card_biUnion_lt_iff_forall_of_isRegular

English

For a regular cardinal c and hs: #s < c, the statement #(⋃ a ∈ s, t a ha) < c is equivalent to ∀ a ∈ s, #(t a ha) < c.

Русский

Для регулярного кардинала c и hs: #s < c, #(⋃ a∈s, t a ha) < c эквивалентно ∀ a∈s, #(t a ha) < c.

LaTeX

$$$IsRegular(c) \land \#s < c \Rightarrow \#(\bigcup_{a \in s} t(a, ha)) < c \Leftrightarrow \forall a \in s, \#(t(a, ha)) < c$$$

Lean4

theorem card_biUnion_lt_iff_forall_of_isRegular {α β : Type u} {s : Set α} {t : ∀ a ∈ s, Set β} {c : Cardinal}
    (hc : c.IsRegular) (hs : #s < c) : #(⋃ a ∈ s, t a ‹_›) < c ↔ ∀ a (ha : a ∈ s), #(t a ha) < c := by
  rw [biUnion_eq_iUnion, card_iUnion_lt_iff_forall_of_isRegular hc hs, SetCoe.forall']

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