def inverse {α : Type u_1} {β : Type u_2} [Inhabited α] (f : α → β) : β → α

Equations

• inverse f y = if h : ∃ (x : α), f x = y then Classical.choose h else default

theorem inverse_spec {α : Type u_1} {β : Type u_2} [Inhabited α] {f : α → β} (y : β) (h : ∃ (x : α), f x = y) : f (inverse f y) = y

theorem Cantor {α : Type u_3} (f : α → Set α) : ¬Function.Surjective f