add_contains_add

formal source

  54@[simp] theorem add_lo (I J : Interval) : (I + J).lo = I.lo + J.lo := rfl
  55@[simp] theorem add_hi (I J : Interval) : (I + J).hi = I.hi + J.hi := rfl
  56
  57theorem add_contains_add {x y : ℝ} {I J : Interval}
  58    (hx : I.contains x) (hy : J.contains y) : (I + J).contains (x + y) := by
  59  constructor
  60  · simp only [add_lo, Rat.cast_add]
  61    exact add_le_add hx.1 hy.1
  62  · simp only [add_hi, Rat.cast_add]
  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