Cantor_Bernstein_Schroeder_Theorem
Provedbijectionscardinalsinjectionsproofwikiset-theory
If there exist injections from A to B and from B to A, then A and B are in bijection (equivalent).
Preamble
import Mathlib.Logic.Equiv.Defs import Mathlib.Logic.Function.Basic
Formal statement
theorem Cantor_Bernstein_Schroeder_Theorem {α : Type _} {β : Type _} (f : α → β) (g : β → α) (hf : Function.Injective f) (hg : Function.Injective g) : Nonempty (α ≃ β) := by sorrySource