nhdsLT_le_nhdsNE

Mathlib.Topology.Order.LeftRight

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

English

In a preorder space, the left neighborhood of a is contained in the right-neighborhood away from a, i.e., 𝓝[<] a ≤ 𝓝[≠] a.

Русский

Для частично упорядоченного пространства 𝓝[<] a ⊆ 𝓝[≠] a.

LaTeX

$$nhdsWithin_mono a fun _ => ne_of_lt$$

Lean4

theorem nhdsLT_le_nhdsNE (a : α) : 𝓝[<] a ≤ 𝓝[≠] a :=
  nhdsWithin_mono a fun _ => ne_of_lt

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

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

Разделы

Аффилиация

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