existsUnique_of_exists_of_unique — Mathlib

English

If there exists x with p x and p is unique on its domain, then there exists a unique x with p x.

Русский

Если существует x с p(x) и p(x) уникальна, значит существует единственный x с p(x).

LaTeX

$$$$ (\\exists x\\, p(x)) \\land (\\\\forall y_1 y_2, p(y_1) \\\\land p(y_2) \\\\rightarrow y_1 = y_2) \\Rightarrow \\exists! x\\, p(x). $$$$

Lean4

theorem existsUnique_of_exists_of_unique {p : α → Prop} (hex : ∃ x, p x) (hunique : ∀ y₁ y₂, p y₁ → p y₂ → y₁ = y₂) :
    ∃! x, p x :=
  Exists.elim hex (fun x px ↦ ExistsUnique.intro x px (fun y (h : p y) ↦ hunique y x h px))

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