English
In a suitable space with an appropriate measure, any σ-compact set of measure zero is meagre (a countable union of nowhere dense sets). More generally, every Fσ set of measure zero is meagre.
Русский
В подходящем пространстве с подходящей мерой множество σ-компактное и нулевой меры является мелким (состоящим из счётного объединения nowhere dense множеств). Более общо — каждый Fσ-множество нулевой меры мелкое.
LaTeX
$$$\bigl( \text{IsSigmaCompact}(s) \land \mu(s) = 0 \bigr) \Rightarrow \text{Meagre}(s)$$$
Lean4
/-- A σ-compact measure zero subset is meagre.
(More generally, every Fσ set of measure zero is meagre.) -/
theorem of_isSigmaCompact_null [T2Space X] (h₁s : IsSigmaCompact s) (h₂s : μ s = 0) : IsMeagre s :=
by
rcases h₁s with ⟨K, hcompact, hcover⟩
have h (n : ℕ) : IsNowhereDense (K n) :=
by
have : μ (K n) = 0 := measure_mono_null (hcover ▸ subset_iUnion K n) h₂s
exact .of_isClosed_null (hcompact n).isClosed this
rw [isMeagre_iff_countable_union_isNowhereDense]
exact ⟨range K, fun t ⟨n, hn⟩ ↦ hn ▸ h n, countable_range K, hcover.symm.subset⟩
