closure_residualEq — Mathlib

English

For a locally closed set s, the closure of s equals s up to a meager set; i.e., closure(s) and s are equal modulo a meager set.

Русский

Для локально замкнутого множества s множестово closure(s) совпадает с s с точностью до множества, мега- малочисленного.

LaTeX

$$$$ \overline{s} =_{\mathrm{meager}} s. $$$$

Lean4

theorem closure_residualEq {s : Set α} (hs : IsLocallyClosed s) : closure s =ᵇ s :=
  by
  rw [Filter.eventuallyEq_set]
  filter_upwards [coborder_mem_residual hs] with x hx
  nth_rewrite 2 [← closure_inter_coborder (s := s)]
  simp [hx]

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