English
Let X be a topological space. A subset s ⊆ X is residual iff there exists a countable collection S of open dense sets such that the intersection ⋂₀ S is contained in s.
Русский
Пусть X — топологическое пространство. Множество s ⊆ X является резидуальным тогда и только тогда, когда существует счётная коллекция S из открытых плотных множеств such that ⋂₀ S ⊆ s.
LaTeX
$$$s \in \mathrm{residual}(X) \iff \exists S : \mathrm{Set}(\mathrm{Set}(X)),\; (\forall t \in S, \mathrm{IsOpen}~t) \land (\forall t \in S, \mathrm{Dense}~t) \land S.\mathrm{Countable} \land \bigcap_{t \in S} t \subseteq s$$$
Lean4
/-- A set is residual iff it includes a countable intersection of dense open sets. -/
theorem mem_residual_iff {s : Set X} :
s ∈ residual X ↔ ∃ S : Set (Set X), (∀ t ∈ S, IsOpen t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ⋂₀ S ⊆ s :=
mem_countableGenerate_iff.trans <| by simp_rw [subset_def, mem_setOf, forall_and, and_assoc]
