one_lt_card

Mathlib.SetTheory.Ordinal.Basic

URI: https://scilib.ai/kg/mathlib#Ordinal.one_lt_card

English

For any ordinal o, 1 < o.card ↔ 1 < o.

Русский

Для любого ординала o, 1 < o.card ⇔ 1 < o.

LaTeX

$$$1 < o.card \\iff 1 < o$$$

Lean4

@[simp]
theorem one_lt_card {o} : 1 < card o ↔ 1 < o := by simpa using nat_lt_card (n := 1)

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

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

Разделы

Аффилиация

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