isMeagre_iUnion — Mathlib

English

A countable union of meagre sets is meagre.

Русский

Счётное объединение множеств мезгрей остаётся мезгрей.

LaTeX

$$[Countable ι] (∀ i, IsMeagre (f i)) → IsMeagre (⋃ i, f i)$$

Lean4

/-- A countable union of meagre sets is meagre. -/
theorem isMeagre_iUnion [Countable ι] {f : ι → Set X} (hs : ∀ i, IsMeagre (f i)) : IsMeagre (⋃ i, f i) :=
  by
  rw [IsMeagre, compl_iUnion]
  exact countable_iInter_mem.mpr hs

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