`neg`

definition

show as: view math explainer →

module: IndisputableMonolith.Numerics.Interval.Basic
domain: Numerics
line: 66 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Numerics.Interval.Basic on GitHub at line 66.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  63    exact add_le_add hx.2 hy.2
  64
  65/-- Negation of intervals: -[a,b] = [-b, -a] -/
  66def neg (I : Interval) : Interval where
  67  lo := -I.hi
  68  hi := -I.lo
  69  valid := neg_le_neg I.valid
  70
  71instance : Neg Interval where
  72  neg := neg
  73
  74@[simp] theorem neg_lo (I : Interval) : (-I).lo = -I.hi := rfl
  75@[simp] theorem neg_hi (I : Interval) : (-I).hi = -I.lo := rfl
  76
  77theorem neg_contains_neg {x : ℝ} {I : Interval} (hx : I.contains x) : (-I).contains (-x) := by
  78  constructor
  79  · simp only [neg_lo, Rat.cast_neg]
  80    exact neg_le_neg hx.2
  81  · simp only [neg_hi, Rat.cast_neg]
  82    exact neg_le_neg hx.1
  83
  84/-- Subtraction of intervals: [a,b] - [c,d] = [a-d, b-c] -/
  85def sub (I J : Interval) : Interval where
  86  lo := I.lo - J.hi
  87  hi := I.hi - J.lo
  88  valid := by linarith [I.valid, J.valid]
  89
  90instance : Sub Interval where
  91  sub := sub
  92
  93@[simp] theorem sub_lo (I J : Interval) : (I - J).lo = I.lo - J.hi := rfl
  94@[simp] theorem sub_hi (I J : Interval) : (I - J).hi = I.hi - J.lo := rfl
  95
  96theorem sub_contains_sub {x y : ℝ} {I J : Interval}

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.