nhdsGT_le_nhdsNE

Mathlib.Topology.Order.LeftRight

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

English

Similarly, 𝓝[>] a ≤ 𝓝[≠] a for any a in a preorder space.

Русский

Аналогично, 𝓝[>] a ≤ 𝓝[≠] a для любого a.

LaTeX

$$nhdsWithin_mono a fun _ => ne_of_gt$$

Lean4

theorem nhdsGT_le_nhdsNE (a : α) : 𝓝[>] a ≤ 𝓝[≠] a :=
  nhdsWithin_mono a fun _ => ne_of_gt

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

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

Разделы

Аффилиация

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