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 α)