English
A property holds on a residual set if and only if it holds on some dense Gδ set.
Русский
Свойство выполняется на резидуальном множестве тогда и только тогда, когда оно выполняется на некотором плотном Gδ-множестве.
LaTeX
$$$\\\\forall p:\\\\ X \\to \\text{Prop}, \\\\big(\\\\forall^\\\\infty x \\\\text{in residual}(X), p(x)\\\\big) \\\\iff \\\\exists t: \\text{Set}(X), \\, \\mathrm{IsGδ}(t) \land \\, \\operatorname{Dense}(t) \land \\\\forall x \\in t, p(x)$$$
Lean4
/-- A property holds on a residual (comeagre) set if and only if it holds on some dense `Gδ` set. -/
theorem eventually_residual {p : X → Prop} : (∀ᶠ x in residual X, p x) ↔ ∃ t : Set X, IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x :=
by
simp only [Filter.Eventually, mem_residual, subset_def, mem_setOf_eq]
tauto
