English
If a family of sets {f i} is pairwise disjoint, and each f i is contained in the Dynkin system, then the union across i in a countable index β also belongs to the Dynkin system.
Русский
Если семейство попарно непересекающихся множеств {f_i} содержится в Dynkin-системе, то их объединение по счётному индексу принадлежит системе.
LaTeX
$$$\forall β [Countable β], \; \text{If } \text{Pairwise}(Disjoint\ on\ f) \land \forall i, d.Has(f_i) \Rightarrow d.Has(\bigcup_{i} f_i)$$$
Lean4
theorem has_iUnion {β} [Countable β] {f : β → Set α} (hd : Pairwise (Disjoint on f)) (h : ∀ i, d.Has (f i)) :
d.Has (⋃ i, f i) := by
cases nonempty_encodable β
rw [← Encodable.iUnion_decode₂]
exact d.has_iUnion_nat (Encodable.iUnion_decode₂_disjoint_on hd) fun n => Encodable.iUnion_decode₂_cases d.has_empty h
