intro — Mathlib

English

If p is a predicate on a, and w ∈ a satisfies p(w) with the property that every y with p(y) equals w, then there exists a unique x with p(x).

Русский

Если p — предикат на α, и существуют w such that p(w) и ∀y (p(y) → y = w), то существует единственный x с p(x).

LaTeX

$$$$p(w) \\wedge (\\forall y\\, (p(y) \\rightarrow y = w)) \\Rightarrow \\exists! x\\, p(x).$$$$

Lean4

theorem intro {p : α → Prop} (w : α) (h₁ : p w) (h₂ : ∀ y, p y → y = w) : ∃! x, p x :=
  ⟨w, h₁, h₂⟩

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