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)
77theorem neg_contains_neg {x : ℝ} {I : Interval} (hx : I.contains x) : (-I).contains (-x) := by
proof body
Term-mode proof.
78 constructor
79 · simp only [neg_lo, Rat.cast_neg]
80 exact neg_le_neg hx.2
81 · simp only [neg_hi, Rat.cast_neg]
82 exact neg_le_neg hx.1
83
84/-- Subtraction of intervals: [a,b] - [c,d] = [a-d, b-c] -/
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
-
contains
in IndisputableMonolith.Numerics.Interval.Basic
decl_use
-
Interval
in IndisputableMonolith.Numerics.Interval.Basic
decl_use
-
neg_hi
in IndisputableMonolith.Numerics.Interval.Basic
decl_use
-
neg_lo
in IndisputableMonolith.Numerics.Interval.Basic
decl_use
-
Interval
in IndisputableMonolith.Recognition.Certification
decl_use