English
A set is residual (comeagre) if and only if it contains a dense Gδ set.
Русский
Резидуальное множество (comeagre) эквивалентно содержанию плотного множества Gδ внутри него.
LaTeX
$$$\\text{mem_residual} \\ :\\ s \\in \\text{residual}(X) \\iff \\exists t \\subseteq s, \\mathrm{IsGδ}(t) \\land \\operatorname{Dense}(t)$$$
Lean4
/-- A set is residual (comeagre) if and only if it includes a dense `Gδ` set. -/
theorem mem_residual {s : Set X} : s ∈ residual X ↔ ∃ t ⊆ s, IsGδ t ∧ Dense t :=
by
constructor
· rw [mem_residual_iff]
rintro ⟨S, hSo, hSd, Sct, Ss⟩
refine ⟨_, Ss, ⟨_, fun t ht => hSo _ ht, Sct, rfl⟩, ?_⟩
exact dense_sInter_of_isOpen hSo Sct hSd
rintro ⟨t, ts, ho, hd⟩
exact mem_of_superset (residual_of_dense_Gδ ho hd) ts
