map_unique — Mathlib

English

For z ∈ x, there exists a unique w with pair z w ∈ map f x.

Русский

Для данного z ∈ x существует единственный элемент w, такой что pair z w ∈ map f x.

LaTeX

$$$\\exists! w, z \\in x \\land w \\text{ satisfies } z \\in x \\Rightarrow z \\text{ is paired with } w$$$

Lean4

theorem map_unique {f : ZFSet.{u} → ZFSet.{u}} [Definable₁ f] {x z : ZFSet.{u}} (zx : z ∈ x) :
    ∃! w, pair z w ∈ map f x :=
  ⟨f z, image.mk _ _ zx, fun y yx => by
    let ⟨w, _, we⟩ := mem_image.1 yx
    let ⟨wz, fy⟩ := pair_injective we
    rw [← fy, wz]⟩

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