card_omega0_opow

Mathlib.SetTheory.Cardinal.Ordinal

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

← MathLib Explorer

English

For any a with a ≠ 0, card(ω^a) = max(ω0, a.card).

Русский

Для любого a ≠ 0, card(ω^a) = max(ω0, a.card).

LaTeX

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

Lean4

theorem card_omega0_opow {a : Ordinal} (h : a ≠ 0) : card (ω ^ a) = max ℵ₀ a.card := by
  rw [card_opow_eq_of_omega0_le_left le_rfl h.bot_lt, card_omega0]

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

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

Разделы

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

Аффилиация

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