not_small_cardinal — Mathlib

English

The type of cardinals is not Small in universe u (Burali-Forti paradox).

Русский

Тип кардиналов во вселенной u не является Small (парadox Бурали-Форти).

LaTeX

$$$\lnot Small Cardinal$$$

Lean4

/-- The type of cardinals in universe `u` is not `Small.{u}`. This is a version of the Burali-Forti
paradox. -/
theorem _root_.not_small_cardinal : ¬Small.{u} Cardinal.{max u v} :=
  by
  intro h
  have := small_lift.{_, v} Cardinal.{max u v}
  rw [← small_univ_iff, ← bddAbove_iff_small] at this
  exact not_bddAbove_univ this

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