theorem proved term proof

`law_of_existence`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  80theorem law_of_existence (x : ℝ) : Exists x ↔ DefectCollapse x :=

Term-mode proof.

  81  ⟨fun ⟨hpos, hdef⟩ => ⟨hpos, hdef⟩, fun ⟨hpos, hdef⟩ => ⟨hpos, hdef⟩⟩
  82
  83/-- **Existence Characterization**: x exists ⟺ x = 1. -/

From the project-wide theorem graph. These declarations reference this one in their body.

law_of_existence in IndisputableMonolith.Foundation.CostAxioms decl_use
unity_is_unique_existent in IndisputableMonolith.Foundation.CostAxioms decl_use

Lean names referenced from this declaration's body.