lo_gt_implies_contains_gt
plain-language theorem explainer
The theorem shows that if a rational b lies strictly below the lower endpoint of a closed rational interval I, then every real x contained in I satisfies b < x. Interval-arithmetic routines for bounding transcendental functions invoke this to propagate strict inequalities from rational endpoints. The proof is a one-line term that applies lt_of_lt_of_le after casting the rational inequality to the reals.
Claim. Let $I$ be a closed interval with rational endpoints. If a rational $b$ satisfies $b < I.lo$ and a real $x$ satisfies $x$ in $I$, then $b < x$.
background
The module supplies verified interval arithmetic for computing bounds on transcendental functions, using rational endpoints that Lean can compute exactly. The Interval structure consists of rational lower and upper bounds together with a proof that the lower bound does not exceed the upper bound. Containment of a real number $x$ in $I$ holds precisely when the cast of the lower bound is at most $x$ and $x$ is at most the cast of the upper bound.
proof idea
The term-mode proof applies lt_of_lt_of_le to the cast of the hypothesis b < I.lo (via exact_mod_cast) together with the left conjunct of the containment hypothesis.
why it matters
This lemma is invoked by prove_lower_bound in the Numerics.Interval.Tactic module to establish strict lower bounds from containment. It supports the verified numerical infrastructure used to confirm Recognition Science constants such as the inverse fine-structure constant inside the interval (137.030, 137.039).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.