isOrdinal_notMem_univ — Mathlib

English

The Burali-Forti paradox: the class of ordinals is not a member of the universe.

Русский

Парадокс Бурали-Форти: класс ординалов не является членом универсума.

LaTeX

$$$ \\text{IsOrdinal} \\notin \\mathrm{Class.univ}. $$$

Lean4

/-- The **Burali-Forti paradox**: ordinals form a proper class. -/
theorem isOrdinal_notMem_univ : IsOrdinal ∉ Class.univ.{u} :=
  by
  rintro ⟨x, hx, -⟩
  suffices IsOrdinal x by
    apply Class.mem_irrefl x
    rwa [Class.coe_mem, hx]
  refine ⟨fun y hy z hz ↦ ?_, fun hyz hzw hwx ↦ ?_⟩ <;> rw [← Class.coe_apply, hx] at *
  exacts [hy.mem hz, hwx.mem_trans hyz hzw]

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