unique — Mathlib

English

If there exists a unique x with p x, then any two p y that satisfy p also must be equal; i.e., the witness is unique.

Русский

Если существует единственный x с p(x), то любые два y с p(y) равны между собой; то есть единственный доказатель существования.

LaTeX

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

Lean4

theorem unique {p : α → Prop} (h : ∃! x, p x) {y₁ y₂ : α} (py₁ : p y₁) (py₂ : p y₂) : y₁ = y₂ :=
  let ⟨_, _, hy⟩ := h;
  (hy _ py₁).trans (hy _ py₂).symm

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