hi_lt_implies_contains_lt
plain-language theorem explainer
The theorem shows that if the upper endpoint of a closed rational interval I lies strictly below a rational b, then every real x inside I also lies strictly below b. Interval-arithmetic code that certifies upper bounds on real functions invokes the result to transfer strict inequalities from endpoints to contained points. The proof is a one-line application of lt_of_le_of_lt to the upper conjunct of the containment predicate after casting the rational inequality.
Claim. Let $I$ be a closed interval with rational endpoints. If $I$ has upper endpoint strictly less than a rational $b$ and $x$ is a real number satisfying the containment predicate for $I$, then $x < b$.
background
The module supplies verified interval arithmetic that uses rational endpoints to bound real-valued expressions. An Interval is the structure consisting of rational lower and upper endpoints together with the proof that the lower is at most the upper. The predicate contains I x asserts that the real cast of the lower endpoint is at most x and x is at most the real cast of the upper endpoint.
proof idea
The proof applies the lemma lt_of_le_of_lt directly to the second conjunct of the containment hypothesis (x ≤ I.hi) and the cast of the given strict inequality I.hi < b.
why it matters
The result is invoked by prove_upper_bound in Numerics.Interval.Tactic to establish strict upper bounds on points inside intervals. It supports rigorous numerical verification inside the Recognition Science framework by ensuring interval bounds remain sound when strict inequalities are required. The module provides the foundation for computing bounds on transcendental functions with rational endpoints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.