`sub`

definition

show as: view math explainer →

module: IndisputableMonolith.Numerics.Interval.Basic
domain: Numerics
line: 85 · 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 85.

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

  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}
  97    (hx : I.contains x) (hy : J.contains y) : (I - J).contains (x - y) := by
  98  constructor
  99  · simp only [sub_lo, Rat.cast_sub]
 100    exact sub_le_sub hx.1 hy.2
 101  · simp only [sub_hi, Rat.cast_sub]
 102    exact sub_le_sub hx.2 hy.1
 103
 104/-- Multiplication for positive intervals -/
 105def mulPos (I J : Interval) (hI : 0 < I.lo) (hJ : 0 < J.lo) : Interval where
 106  lo := I.lo * J.lo
 107  hi := I.hi * J.hi
 108  valid := by
 109    apply mul_le_mul I.valid J.valid
 110    · exact le_of_lt hJ
 111    · linarith [I.valid]
 112
 113theorem mulPos_contains_mul {x y : ℝ} {I J : Interval}
 114    (hIpos : 0 < I.lo) (hJpos : 0 < J.lo)
 115    (hx : I.contains x) (hy : J.contains y) : (mulPos I J hIpos hJpos).contains (x * y) := by

papers checked against this theorem

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