lo_ge_implies_contains_ge

formal source

 169  lt_of_le_of_lt hx.2 (by exact_mod_cast h)
 170
 171/-- If b ≤ I.lo, then all x in I satisfy b ≤ x -/
 172theorem lo_ge_implies_contains_ge {I : Interval} {b : ℚ} (h : b ≤ I.lo) {x : ℝ}
 173    (hx : I.contains x) : (b : ℝ) ≤ x :=
 174  le_trans (by exact_mod_cast h) hx.1
 175
 176/-- If I.hi ≤ b, then all x in I satisfy x ≤ b -/
 177theorem hi_le_implies_contains_le {I : Interval} {b : ℚ} (h : I.hi ≤ b) {x : ℝ}
 178    (hx : I.contains x) : x ≤ (b : ℝ) :=
 179  le_trans hx.2 (by exact_mod_cast h)
 180
 181end Interval
 182
 183end IndisputableMonolith.Numerics