mathlib documentation

set_theory.schroeder_bernstein

theorem function.embedding.schroeder_bernstein {α : Type u} {β : Type v} {f : α → β} {g : β → α} :
function.injective ffunction.injective g(∃ (h : α → β), function.bijective h)

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

theorem function.embedding.min_injective {ι : Type u} {β : ι → Type v} :
nonempty ι(∃ (i : ι), nonempty (Π (j : ι), β i β j))

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