monotone_nhds

Mathlib.Topology.Filter

URI: https://scilib.ai/kg/mathlib#Filter.monotone_nhds

English

The neighborhood operator is monotone: if l1 ≤ l2 then 𝓝 l1 ≤ 𝓝 l2.

Русский

Окрестности монотонируются: если l1 ≤ l2, то 𝓝 l1 ≤ 𝓝 l2.

LaTeX

$$$\text{Monotone}(\mathcal{N}) \;\Rightarrow\; l_1 \le l_2 \implies \mathcal{N}(l_1) \le \mathcal{N}(l_2).$$$

Lean4

theorem monotone_nhds : Monotone (𝓝 : Filter α → Filter (Filter α)) :=
  Monotone.of_map_inf Filter.nhds_inf

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

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

Разделы

Аффилиация

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