lean_workbook_plus_55105

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove that there is no surjective function from a set $E$ to its power set $P(E)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_55105 (E : Type) : ¬∃ f : E → Set E, Function.Surjective f   :=  by sorry

Source