pith. machine review for the scientific record. sign in
theorem proved term proof

exists_iff_unity

show as:
view Lean formalization →

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)

  84theorem exists_iff_unity {x : ℝ} (hx : 0 < x) : Exists x ↔ x = 1 :=

proof body

Term-mode proof.

  85  ⟨fun ⟨_, hdef⟩ => (defect_zero_iff_one hx).mp hdef,
  86   fun h => ⟨hx, (defect_zero_iff_one hx).mpr h⟩⟩
  87
  88/-- **Unity is Unique Existent**: ∀ x, Exists x ⟺ x = 1. -/

used by (1)

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

depends on (7)

Lean names referenced from this declaration's body.