theorem
proved
hi_le_implies_contains_le
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
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