nhdsWithin_empty

Mathlib.Topology.ContinuousOn

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

English

The neighborhood within the empty set is the bottom filter.

Русский

Окрестности внутри пустого множества равны нижнему фильтру.

LaTeX

$$$ 𝓝[\emptyset] a = \bot $$$

Lean4

@[simp]
theorem nhdsWithin_empty (a : α) : 𝓝[∅] a = ⊥ := by rw [nhdsWithin, principal_empty, inf_bot_eq]

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

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

Разделы

Аффилиация

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