card_iUnion_lt_iff_forall_of_isRegular

English

For a regular cardinal c and hι: #ι < c, the statement #(⋃ i, t_i) < c holds iff ∀ i, #(t_i) < c.

Русский

Для регулярного кардинала c и hι: #ι < c, верно #(⋃ i, t_i) < c тогда и только тогда, когда ∀ i, #(t_i) < c.

LaTeX

$$$IsRegular(c) \land \#ι < c \Rightarrow \Big( #(\bigcup_i t_i) < c \;\Leftrightarrow\; \forall i, #(t_i) < c \Big)$$$

Lean4

@[simp]
theorem card_iUnion_lt_iff_forall_of_isRegular {ι : Type u} {α : Type u} {t : ι → Set α} {c : Cardinal}
    (hc : c.IsRegular) (hι : #ι < c) : #(⋃ i, t i) < c ↔ ∀ i, #(t i) < c :=
  by
  refine ⟨card_lt_of_card_iUnion_lt, fun h ↦ ?_⟩
  apply lt_of_le_of_lt (Cardinal.mk_sUnion_le _)
  apply Cardinal.mul_lt_of_lt hc.aleph0_le (lt_of_le_of_lt Cardinal.mk_range_le hι)
  apply Cardinal.iSup_lt_of_isRegular hc (lt_of_le_of_lt Cardinal.mk_range_le hι)
  simpa

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