biUnion_iff — Mathlib

English

If s is countable, then the biUnion over a ∈ s of t(a,ha) is countable iff each t(a,ha) is countable.

Русский

Если s счетно, то биобъединение по a∈s множества t(a,ha) счетно тогда и только тогда, когда каждое t(a,ha) счетно.

LaTeX

$$$\\operatorname{Countable}(s) \\Rightarrow (\\bigcup_{a \\in s} t(a, a\\in s)).Countable \\iff \\forall a\\in s, (t(a, a\\in s)).Countable$$$

Lean4

theorem biUnion_iff {s : Set α} {t : ∀ a ∈ s, Set β} (hs : s.Countable) :
    (⋃ a ∈ s, t a ‹_›).Countable ↔ ∀ a (ha : a ∈ s), (t a ha).Countable :=
  by
  have := hs.to_subtype
  rw [biUnion_eq_iUnion, countable_iUnion_iff, SetCoe.forall']

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