eventually_ne — Mathlib

English

For a ≠ b, every neighborhood of a relative to s eventually excludes b: ∀ᶠ x ∈ 𝓝[s] a, x ≠ b.

Русский

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

LaTeX

$$$\text{Ne}(a,b) \Rightarrow ∀ᶠ x \in 𝓝[s]a, x \neq b$$$

Lean4

theorem eventually_ne [TopologicalSpace Y] [T1Space Y] {g : X → Y} {x : X} {y : Y} (hg1 : ContinuousAt g x)
    (hg2 : g x ≠ y) : ∀ᶠ z in 𝓝 x, g z ≠ y :=
  hg1.tendsto.eventually_ne hg2

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