card_opow_omega0

Mathlib.SetTheory.Cardinal.Ordinal

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

← MathLib Explorer

English

If a > 1, then card(a^ω) = max(ℵ0, a.card).

Русский

Если a > 1, то card(a^ω) = max(ℵ0, a.card).

LaTeX

$$card(a^\omega) = \max(\aleph_0, a.card)$$

Lean4

theorem card_opow_omega0 {a : Ordinal} (h : 1 < a) : card (a ^ ω) = max ℵ₀ a.card := by
  rw [card_opow_eq_of_omega0_le_right h le_rfl, card_omega0, max_comm]

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

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

Разделы

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

Аффилиация

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