schroeder_bernstein — Mathlib

English

If there exist injections f: α → β and g: β → α, then there exists a bijection h: α → β.

Русский

Если существуют инъекции f: α → β и g: β → α, то существует биекция h: α → β.

LaTeX

$$$\exists h: \alpha \to \beta, \mathrm{Bijective}(h)$$$

Lean4

/-- **The Schröder-Bernstein Theorem**:
Given injections `α → β` and `β → α`, we can get a bijection `α → β`. -/
theorem schroeder_bernstein {f : α → β} {g : β → α} (hf : Function.Injective f) (hg : Function.Injective g) :
    ∃ h : α → β, Bijective h :=
  by
  obtain ⟨f, hf, _⟩ := schroeder_bernstein_of_rel hf hg (fun x y ↦ True) (by simp) (by simp)
  exact ⟨f, hf⟩

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