hi_le_implies_contains_le
plain-language theorem explainer
If the upper rational endpoint of interval I is at most b, every real x inside I satisfies x at most b. Numerics code computing rigorous bounds on transcendental functions cites this when propagating upper limits from rational endpoints. The proof is a one-line term that chains transitivity on the right half of containment after casting the rational inequality.
Claim. Let $I$ be a closed interval with rational endpoints. If $I.hi ≤ b$ for rational $b$, then every real $x$ satisfying $I.lo ≤ x ≤ I.hi$ obeys $x ≤ b$.
background
The module supplies verified interval arithmetic that uses exact rational endpoints to bound real values. Interval is the structure with rational lo and hi together with the proof lo ≤ hi. The contains predicate asserts that the real cast of lo is at most x and x is at most the real cast of hi.
proof idea
One-line term proof applying le_trans to the second conjunct of the containment hypothesis (x ≤ I.hi) and the cast of the given I.hi ≤ b.
why it matters
It is called directly by prove_upper_bound_le in Numerics.Interval.Tactic to establish concrete upper bounds. The lemma supports the Numerics layer that supplies exact interval computations for constants such as phi inside the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.