card_opow_eq_of_omega0_le_left — Mathlib

English

If ω ≤ a and 0 < b, then (a^b).card = max(a.card, b.card).

Русский

Если ω ≤ a и 0 < b, то (a^b).card = max(a.card, b.card).

LaTeX

$$(a^b).card = \max(a.card, b.card) \quad (ω ≤ a, 0 < b)$$

Lean4

theorem card_opow_eq_of_omega0_le_left {a b : Ordinal} (ha : ω ≤ a) (hb : 0 < b) : (a ^ b).card = max a.card b.card :=
  by
  apply (card_opow_le_of_omega0_le_left ha b).antisymm (max_le _ _) <;> apply card_le_card
  · exact left_le_opow a hb
  · exact right_le_opow b (one_lt_omega0.trans_le ha)

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