neg_contains_neg

formal source

  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}
  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