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)
232theorem law_of_existence {x : ℝ} (hx : 0 < x) : Exists x ↔ x = 1 := by
proof body
Term-mode proof.
233 simp only [Exists, J_eq_zero_iff hx, and_iff_right hx]
234
235/-- Unity is the unique existent. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (8)
Lean names referenced from this declaration's body.
-
Exists
in IndisputableMonolith.Foundation.CostAxioms
decl_use
-
J_eq_zero_iff
in IndisputableMonolith.Foundation.CostAxioms
decl_use
-
Exists
in IndisputableMonolith.Foundation.LawOfExistence
decl_use
-
law_of_existence
in IndisputableMonolith.Foundation.LawOfExistence
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use