No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
57theorem add_contains_add {x y : ℝ} {I J : Interval}
58 (hx : I.contains x) (hy : J.contains y) : (I + J).contains (x + y) := by
proof body
Term-mode proof.
59 constructor
60 · simp only [add_lo, Rat.cast_add]
61 exact add_le_add hx.1 hy.1
62 · simp only [add_hi, Rat.cast_add]
63 exact add_le_add hx.2 hy.2
64
65/-- Negation of intervals: -[a,b] = [-b, -a] -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (11)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
contains
in IndisputableMonolith.Ethics.StakeGraph
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
add_hi
in IndisputableMonolith.Numerics.Interval.Basic
decl_use
-
add_lo
in IndisputableMonolith.Numerics.Interval.Basic
decl_use
-
contains
in IndisputableMonolith.Numerics.Interval.Basic
decl_use
-
Interval
in IndisputableMonolith.Numerics.Interval.Basic
decl_use
-
Interval
in IndisputableMonolith.Recognition.Certification
decl_use