lim_nhdsWithin

Mathlib.Topology.Separation.Hausdorff

URI: https://scilib.ai/kg/mathlib#lim_nhdsWithin

← MathLib Explorer

English

If x ∈ closure(s), then the limit of nhdsWithin x s equals x.

Русский

Если x ∈ замыкание s, то предел nhdsWithin x s равен x.

LaTeX

$$$ x \\in \\overline{s} \\Rightarrow \\lim (\\mathcal{N}(x)\\restriction s) = x$$$

Lean4

@[simp]
theorem lim_nhdsWithin {x : X} {s : Set X} (h : x ∈ closure s) : @lim _ _ ⟨x⟩ (𝓝[s] x) = x :=
  haveI : NeBot (𝓝[s] x) := mem_closure_iff_clusterPt.1 h
  lim_eq inf_le_left

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru