card_typein_toType_lt

Mathlib.SetTheory.Ordinal.Basic

URI: https://scilib.ai/kg/mathlib#Cardinal.card_typein_toType_lt

← MathLib Explorer

English

For c and x ∈ c.ord.toType, card(typein(α := c.ord.toType) (<) x) < c.

Русский

Пусть c — кардинал и x ∈ c.ord.toType; тогда card(typein(α := c.ord.toType) (<) x) < c.

LaTeX

$$$ \operatorname{card}(\operatorname{typein}(\alpha := c.ord.toType)(<) x) < c $$$

Lean4

theorem card_typein_toType_lt (c : Cardinal) (x : c.ord.toType) : card (typein (α := c.ord.toType) (· < ·) x) < c :=
  by
  rw [← lt_ord]
  apply typein_lt_self

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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