cantor_surjective — Mathlib

English

There is no surjection from a set α to its power set Set α.

Русский

Не существует сюръективного отображения из множества α в множество подмножеств P(α).

LaTeX

$$$\forall \alpha, \lnot \exists f: \alpha \to \mathcal{P}(\alpha).$$$

Lean4

/-- **Cantor's diagonal argument** implies that there are no surjective functions from `α`
to `Set α`. -/
theorem cantor_surjective {α} (f : α → Set α) : ¬Surjective f
  | h =>
    let ⟨D, e⟩ := h {a | ¬f a a}
    @iff_not_self (D ∈ f D) <| iff_of_eq <| congr_arg (D ∈ ·) e

Похожие утверждения