not_small_ordinal — Mathlib

English

The type of ordinals in universe u is not Small in universe max u v; equivalently, there is no small set of ordinals that contains all ordinals in that universe.

Русский

Тип ординалов в вселенной u не является малым в вселенной max(u,v); эквивалентно: не существует малого множества ординалов, содержащего все ординалы в этой вселенной.

LaTeX

$$$\\neg Small.{u} Ordinal.{max u v}$$$

Lean4

/-- The type of ordinals in universe `u` is not `Small.{u}`. This is the type-theoretic analog of
the Burali-Forti paradox. -/
theorem not_small_ordinal : ¬Small.{u} Ordinal.{max u v} := fun h =>
  @not_injective_of_ordinal _ h _ fun _a _b => Ordinal.lift_inj.{v, u}.1

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