eventually_mem — Mathlib

English

Let X be a topological space and s ⊆ X be open. If x ∈ s, then x lies in a neighborhood contained in s; equivalently, 𝓝 x ⊆ s, i.e. ∀ᶠ y in 𝓝 x, y ∈ s.

Русский

Пусть X — топологическое пространство, s ⊆ X открытое. Тогда при любом x ∈ s существует окрестность x, содержащаяся в s; эквивалентно 𝓝 x ⊆ s, то есть ∀ᶠ y в 𝓝 x, y ∈ s.

LaTeX

$$$\\mathrm{IsOpen}(s) \land x \\in s \\Rightarrow \\nhds x \\subseteq s$$$

Lean4

theorem eventually_mem (hs : IsOpen s) (hx : x ∈ s) : ∀ᶠ x in 𝓝 x, x ∈ s :=
  IsOpen.mem_nhds hs hx

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