eventually_ne_nhds

Mathlib.Topology.Separation.Basic

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

English

If a ≠ b then eventually in nhds a, x ≠ b.

Русский

Если a ≠ b, то в окрестностях a почти везде x ≠ b.

LaTeX

$$$\;\; \text{Ne}(a,b) \Rightarrow ∀ᶠ x \in \mathcal{N}(a), x \neq b$$$

Lean4

theorem eventually_ne_nhds [T1Space X] {a b : X} (h : a ≠ b) : ∀ᶠ x in 𝓝 a, x ≠ b :=
  IsOpen.eventually_mem isOpen_ne h

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

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

Разделы

Аффилиация

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