hasCardinalLT_iff_cardinal_mk_lt

Mathlib.SetTheory.Cardinal.HasCardinalLT

URI: https://scilib.ai/kg/mathlib#hasCardinalLT_iff_cardinal_mk_lt

English

If a type X has a bound κ, then X is small.

Русский

Если у множества X есть ограничение Кардинала κ, то X является малым (в смысле множества мировых уровней).

LaTeX

$$Small.{v} X$$

Lean4

theorem hasCardinalLT_iff_cardinal_mk_lt (X : Type u) (κ : Cardinal.{u}) : HasCardinalLT X κ ↔ Cardinal.mk X < κ := by
  simp [HasCardinalLT]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru