nhds_nil

Mathlib.Topology.List

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

English

The neighborhood filter at the empty list equals the pure filter of the empty list.

Русский

Окрестности пустого списка равны чистоте (pure) пустого списка.

LaTeX

$$$ \mathcal{N}(\,[\]) = \operatorname{pure}(\,[\]) $$$

Lean4

@[simp]
theorem nhds_nil : 𝓝 ([] : List α) = pure [] := by rw [nhds_list, List.traverse_nil _]

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

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

Разделы

Аффилиация

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