cantor_injective — Mathlib

English

There is no injective function from the power set P(α) into α.

Русский

Не существует инъективной функции из множества подмножеств α в α.

LaTeX

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

Lean4

/-- **Cantor's diagonal argument** implies that there are no injective functions from `Set α`
to `α`. -/
theorem cantor_injective {α : Type*} (f : Set α → α) : ¬Injective f
  | i =>
    cantor_surjective (fun a ↦ {b | ∀ U, a = f U → U b}) <|
      RightInverse.surjective (fun U ↦ Set.ext fun _ ↦ ⟨fun h ↦ h U rfl, fun h _ e ↦ i e ▸ h⟩)

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