limUnder_nhdsWithin_id

Mathlib.Topology.Separation.Hausdorff

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

English

The limUnder at nhdsWithin x s of the identity is x.

Русский

limUnder при nhdsWithin x s для id равен x.

LaTeX

$$$\\operatorname{limUnder}(\\mathcal{N}_{}\\!_{x,s},\\mathrm{id}) = x$$$

Lean4

@[simp]
theorem limUnder_nhdsWithin_id {x : X} {s : Set X} (h : x ∈ closure s) : @limUnder _ _ _ ⟨x⟩ (𝓝[s] x) id = x :=
  lim_nhdsWithin h

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

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

Разделы

Аффилиация

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