existsUnique_iff_exists — Mathlib

English

If α is a Subsingleton, then (∃! x, p x) is equivalent to ∃ x, p x.

Русский

Если α — подсинглотон, то (существует уникальный x: p(x)) эквивалентно существованию x: p(x).

LaTeX

$$$$ [Subsingleton \\alpha] \\Rightarrow (\\\\exists! x, p(x)) \\Leftrightarrow (\\\\exists x, p(x)). $$$$

Lean4

@[simp]
theorem existsUnique_iff_exists [Subsingleton α] {p : α → Prop} : (∃! x, p x) ↔ ∃ x, p x :=
  ⟨fun h ↦ h.exists, Exists.imp fun x hx ↦ ⟨hx, fun y _ ↦ Subsingleton.elim y x⟩⟩

Похожие утверждения