No_Bijection_from_Set_to_its_Power_Set
Provedbijectionspower-setproofwiki
Let S be a set. There is no bijection f: S → 𝒫(S).
Preamble
import Mathlib.Data.Set.Basic import Mathlib.Logic.Function.Basic
Formal statement
theorem No_Bijection_from_Set_to_its_Power_Set {α : Type _} (f : α → Set α) : ¬ Function.Bijective f := by sorrySource