card_lt_of_card_iUnion_lt — Mathlib

English

Let t_i be sets, and c a cardinal. If h holds that the union over i of t_i has cardinal less than c, then for every i, t_i has cardinal less than c.

Русский

Пусть t_i — множества; если множество объединения ⋃ i t_i имеет кардинал меньше c, то у каждого i кардинал t_i тоже меньше c.

LaTeX

$$$\#\Big(\bigcup_i t_i\Big) < c \Rightarrow \forall i,\#t_i < c$$$

Lean4

@[simp]
theorem card_lt_of_card_iUnion_lt {ι : Type u} {α : Type u} {t : ι → Set α} {c : Cardinal} (h : #(⋃ i, t i) < c)
    (i : ι) : #(t i) < c :=
  lt_of_le_of_lt (Cardinal.mk_le_mk_of_subset <| subset_iUnion _ _) h

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