theorem proved term proof

`hi_le_implies_contains_le`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 177theorem hi_le_implies_contains_le {I : Interval} {b : ℚ} (h : I.hi ≤ b) {x : ℝ}
 178    (hx : I.contains x) : x ≤ (b : ℝ) :=

Term-mode proof.

 179  le_trans hx.2 (by exact_mod_cast h)
 180
 181end Interval
 182
 183end IndisputableMonolith.Numerics

From the project-wide theorem graph. These declarations reference this one in their body.

prove_upper_bound_le in IndisputableMonolith.Numerics.Interval.Tactic decl_use

Lean names referenced from this declaration's body.