bijective_iff_existsUnique — Mathlib

English

For a bijection f: α → β, for every b ∈ β there exists a unique a ∈ α with f(a) = b.

Русский

Пусть f: α → β биективна. Тогда для каждого b ∈ β существует единственный a ∈ α такой, что f(a) = b.

LaTeX

$$$\operatorname{Bijective}(f) \Rightarrow \forall b:\beta, \exists! a:\alpha, f(a)=b.$$$

Lean4

theorem bijective_iff_existsUnique (f : α → β) : Bijective f ↔ ∀ b : β, ∃! a : α, f a = b :=
  ⟨fun hf b ↦
    let ⟨a, ha⟩ := hf.surjective b
    ⟨a, ha, fun _ ha' ↦ hf.injective (ha'.trans ha.symm)⟩,
    fun he ↦ ⟨fun {_a a'} h ↦ (he (f a')).unique h rfl, fun b ↦ (he b).exists⟩⟩

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