sub_contains_sub
plain-language theorem explainer
The theorem shows that if a real x lies inside interval I and y inside J then x minus y lies inside the difference interval I minus J. Numerics researchers building verified bounds on real functions would cite this when composing subtraction steps in interval arithmetic. The proof is a direct constructor split that reduces both endpoint inequalities to sub_le_sub via the endpoint lemmas sub_lo and sub_hi.
Claim. Let $I$ and $J$ be closed intervals with rational endpoints. If the real number $x$ satisfies $I.lo ≤ x ≤ I.hi$ and $y$ satisfies $J.lo ≤ y ≤ J.hi$, then $x - y$ satisfies $(I - J).lo ≤ x - y ≤ (I - J).hi$, where $(I - J).lo = I.lo - J.hi$ and $(I - J).hi = I.hi - J.lo$.
background
The module supplies verified interval arithmetic that uses rational endpoints to produce rigorous bounds on real-valued expressions. An Interval is the structure consisting of rational lo and hi with the proof obligation lo ≤ hi. The contains predicate for an interval I and real x is the conjunction (I.lo cast to ℝ) ≤ x ∧ x ≤ (I.hi cast to ℝ). Subtraction of intervals is defined by the endpoint rules sub_lo and sub_hi, which set the lower bound of I - J to I.lo - J.hi and the upper bound to I.hi - J.lo.
proof idea
The proof opens with the constructor tactic to split the target containment into its lower-bound and upper-bound conjuncts. Each conjunct is discharged by a simp only [sub_lo, Rat.cast_sub] step followed by exact sub_le_sub applied to the appropriate projections of the input hypotheses hx and hy.
why it matters
This lemma supplies the subtraction case for the interval-arithmetic layer that supports exact bounding of transcendental functions inside the numerics module. It completes one of the basic arithmetic closures required before higher-level operations such as multiplication or function evaluation can be verified. No downstream uses are recorded yet, so the result currently serves as infrastructure rather than a direct input to a parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.