lim_eq_iff_le_nhds

Mathlib.Topology.Separation.Hausdorff

URI: https://scilib.ai/kg/mathlib#Ultrafilter.lim_eq_iff_le_nhds

English

The limUnder at nhds x of the identity map equals x.

Русский

limUnder при nhds x для тождественной карты дает x.

LaTeX

$$$\\operatorname{limUnder}(\\mathcal{N}(x))\\mathrm{id} = x$$$

Lean4

theorem lim_eq_iff_le_nhds [CompactSpace X] {x : X} {F : Ultrafilter X} : F.lim = x ↔ ↑F ≤ 𝓝 x :=
  ⟨fun h => h ▸ F.le_nhds_lim, lim_eq⟩

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

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

Разделы

Аффилиация

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