English
A set is meagre iff it is contained in a countable union of nowhere dense sets.
Русский
Множество является мезгрей тогда и только тогда, когда оно содержится в счётном объединении нигде плотных множеств.
LaTeX
$$IsMeagre(s) \iff ∃ S : Set (Set X), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S$$
Lean4
/-- A set is meagre iff it is contained in a countable union of nowhere dense sets. -/
theorem isMeagre_iff_countable_union_isNowhereDense {s : Set X} :
IsMeagre s ↔ ∃ S : Set (Set X), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S :=
by
rw [IsMeagre, mem_residual_iff, compl_bijective.surjective.image_surjective.exists]
simp_rw [← and_assoc, ← forall_and, forall_mem_image, ← isClosed_isNowhereDense_iff_compl, sInter_image, ←
compl_iUnion₂, compl_subset_compl, ← sUnion_eq_biUnion, and_assoc]
refine ⟨fun ⟨S, hS, hc, hsub⟩ ↦ ⟨S, fun s hs ↦ (hS hs).2, ?_, hsub⟩, ?_⟩
· rw [← compl_compl_image S]; exact hc.image _
· intro ⟨S, hS, hc, hsub⟩
use closure '' S
rw [forall_mem_image]
exact
⟨fun s hs ↦ ⟨isClosed_closure, (hS s hs).closure⟩, (hc.image _).image _,
hsub.trans (sUnion_mono_subsets fun s ↦ subset_closure)⟩
