card_opow_le_of_omega0_le_left — Mathlib

English

If ho expresses o.card ≤ c and hc expresses ℵ0 ≤ c, then the union over j < o of A(j) has cardinal ≤ c given each fiber ≤ c.

Русский

Если ho задаёт o.card ≤ c и hc задаёт ℵ0 ≤ c, то объединение по j<o множества A(j) имеет кардинал ≤ c при условии, что каждый A(j) имеет кардинал ≤ c.

LaTeX

$$\#(⋃ j < o, A(j)) ≤ c$$

Lean4

theorem card_opow_le_of_omega0_le_left {a : Ordinal} (ha : ω ≤ a) (b : Ordinal) : (a ^ b).card ≤ max a.card b.card :=
  by
  refine limitRecOn b ?_ ?_ ?_
  · simpa using one_lt_omega0.le.trans ha
  · intro b IH
    rw [opow_succ, card_mul, card_succ, Cardinal.mul_eq_max_of_aleph0_le_right, max_comm]
    · grw [IH]
      rw [← max_assoc, max_self]
      grw [← le_self_add]
    · rw [ne_eq, card_eq_zero, opow_eq_zero]
      rintro ⟨rfl, -⟩
      cases omega0_pos.not_ge ha
    · rwa [aleph0_le_card]
  · intro b hb IH
    rw [(isNormal_opow (one_lt_omega0.trans_le ha)).apply_of_isSuccLimit hb]
    apply (card_iSup_Iio_le_card_mul_iSup _).trans
    rw [Cardinal.lift_id, Cardinal.mul_eq_max_of_aleph0_le_right, max_comm]
    · apply max_le _ (le_max_right _ _)
      apply ciSup_le'
      rintro ⟨c, (hcb : c < b)⟩
      grw [IH c hcb, hcb]
    · simpa using hb.ne_bot
    · refine le_ciSup_of_le ?_ ⟨1, one_lt_omega0.trans_le <| omega0_le_of_isSuccLimit hb⟩ ?_
      · exact Cardinal.bddAbove_of_small _
      · simpa

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