lo_ge_implies_contains_ge
plain-language theorem explainer
If a rational b is at most the lower endpoint of a closed interval I with rational bounds, then every real x inside I is at least b. Numerics routines that propagate interval bounds during constant computations cite this to maintain lower estimates. The proof is a one-line term applying transitivity after casting the rational inequality to reals.
Claim. Let $I$ be a closed interval with rational endpoints $lo$ and $hi$. If $b$ is rational with $b ≤ I.lo$ and $x$ is real with $I.lo ≤ x ≤ I.hi$, then $b ≤ x$.
background
The module supplies verified interval arithmetic that uses exact rational endpoints to bound real values of transcendental functions. An Interval is the structure with fields lo : ℚ, hi : ℚ and valid : lo ≤ hi. The contains predicate on a real x holds exactly when lo ≤ x ≤ hi.
proof idea
The proof is a one-line term that applies le_trans to the cast of b ≤ I.lo and the first projection of the contains hypothesis, which supplies I.lo ≤ x.
why it matters
The lemma is called by prove_lower_bound_le in Numerics.Interval.Tactic. It supplies a basic inequality step inside the verified arithmetic layer that supports bound computations for Recognition Science constants, including the alpha inverse band and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.