mathlib documentation

set_theory.schroeder_bernstein

theorem function.embedding.schroeder_bernstein {α : Type u} {β : Type v} {f : α → β} {g : β → α} (hf : function.injective f) (hg : function.injective g) :

∃ (h : α → β), function.bijective h

theorem function.embedding.antisymm {α : Type u} {β : Type v} :

(α ↪ β) → (β ↪ α) → nonempty (α ≃ β)

theorem function.embedding.min_injective {ι : Type u} {β : ι → Type v} (I : nonempty ι) :

∃ (i : ι), nonempty (Π (j : ι), β i ↪ β j)

theorem function.embedding.total {α : Type u} {β : Type v} :

nonempty (α ↪ β) ∨ nonempty (β ↪ α)