contains_point

formal source

  31  hi := q
  32  valid := le_refl q
  33
  34theorem contains_point (q : ℚ) : (point q).contains (q : ℝ) :=
  35  ⟨le_refl _, le_refl _⟩
  36
  37/-- Interval from explicit bounds -/
  38def mk' (lo hi : ℚ) (h : lo ≤ hi := by decide) : Interval where
  39  lo := lo
  40  hi := hi
  41  valid := h
  42
  43/-! ## Interval Arithmetic Operations -/
  44
  45/-- Addition of intervals: [a,b] + [c,d] = [a+c, b+d] -/
  46def add (I J : Interval) : Interval where
  47  lo := I.lo + J.lo
  48  hi := I.hi + J.hi
  49  valid := add_le_add I.valid J.valid
  50
  51instance : Add Interval where
  52  add := add
  53
  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