theorem
proved
hi_le_implies_contains_le
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Numerics.Interval.Basic on GitHub at line 177.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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