residual_of_dense_Gδ — Mathlib

English

Dense Gδ sets are residual.

Русский

Плотные Gδ-множества являются резидуальными.

LaTeX

$$$IsGδ(s)\\land Dense(s)\\Rightarrow s\\in residual(X)$$$

Lean4

/-- Dense Gδ sets are residual. -/
theorem residual_of_dense_Gδ {s : Set X} (ho : IsGδ s) (hd : Dense s) : s ∈ residual X :=
  by
  rcases ho with ⟨T, To, Tct, rfl⟩
  exact (countable_sInter_mem Tct).mpr fun t tT => residual_of_dense_open (To t tT) (hd.mono (sInter_subset_of_mem tT))

Похожие утверждения