English
If a countable family of closed sets covers a dense Gδ set, then the union of their interiors is dense.
Русский
Если счетное множество замкнутых множеств покрывает плотную Gδ—множество, то объединение их Interiors плотное.
LaTeX
$$$$\\text{If } (IsGδ(s_i))_{i\\in I}, \\ Dense(\\bigcap_i s_i), \\text{ then } Dense(\\\\bigcup_i \\operatorname{interior}(s_i)).$$$$
Lean4
/-- If a countable family of closed sets cover a dense `Gδ` set, then the union of their interiors
is dense. Formulated here with `⋃`. -/
theorem dense_iUnion_interior_of_closed [Countable ι] {s : Set X} (hs : IsGδ s) (hd : Dense s) {f : ι → Set X}
(hc : ∀ i, IsClosed (f i)) (hU : s ⊆ ⋃ i, f i) : Dense (⋃ i, interior (f i)) :=
by
let g i := (frontier (f i))ᶜ
have hgo : ∀ i, IsOpen (g i) := fun i => isClosed_frontier.isOpen_compl
have hgd : Dense (⋂ i, g i) := by
refine dense_iInter_of_isOpen hgo fun i x => ?_
rw [closure_compl, interior_frontier (hc _)]
exact id
refine (hd.inter_of_Gδ hs (.iInter_of_isOpen fun i => (hgo i)) hgd).mono ?_
rintro x ⟨hxs, hxg⟩
rw [mem_iInter] at hxg
rcases mem_iUnion.1 (hU hxs) with ⟨i, hi⟩
exact mem_iUnion.2 ⟨i, self_diff_frontier (f i) ▸ ⟨hi, hxg _⟩⟩
