def sbAux {α : Type u_1} {β : Type u_2} (f : α → β) (g : β → α) : ℕ → Set α

Equations

• sbAux f g 0 = Set.univ \ g '' Set.univ
• sbAux f g n.succ = g '' (f '' sbAux f g n)

def sbSet {α : Type u_1} {β : Type u_2} (f : α → β) (g : β → α) : Set α

Equations

• sbSet f g = ⋃ (n : ℕ), sbAux f g n

def sbFun {α : Type u_1} {β : Type u_2} [Nonempty β] (f : α → β) (g : β → α) (x : α) : β

Equations

• sbFun f g x = if x ∈ sbSet f g then f x else Function.invFun g x

theorem sb_right_inv {α : Type u_1} {β : Type u_2} [Nonempty β] (f : α → β) (g : β → α) {x : α} (hx : x ∉ sbSet f g) : g (Function.invFun g x) = x

theorem sb_injective {α : Type u_1} {β : Type u_2} [Nonempty β] (f : α → β) (g : β → α) (hf : Function.Injective f) : Function.Injective (sbFun f g)

theorem sb_surjective {α : Type u_1} {β : Type u_2} [Nonempty β] (f : α → β) (g : β → α) (hg : Function.Injective g) : Function.Surjective (sbFun f g)

theorem schroeder_bernstein {α : Type u_1} {β : Type u_2} [Nonempty β] {f : α → β} {g : β → α} (hf : Function.Injective f) (hg : Function.Injective g) : ∃ (h : α → β), Function.Bijective h