eventually_ne — Mathlib

English

For a nontrivial limit, eventual non-equality holds: if g tends to b1 and b1 ≠ b2, then g never equals b2 eventually.

Русский

Если предел не тождественен, то существует окрестность, где g z ≠ b2 почти всегда.

LaTeX

$$$\text{Tendsto } g\ l\!\to (\mathcal{N} b_1) \land b_1 \neq b_2 \Rightarrow ∀ᶠ z \in l, g(z) \neq b_2$$$

Lean4

theorem eventually_ne {X} [TopologicalSpace Y] [T1Space Y] {g : X → Y} {l : Filter X} {b₁ b₂ : Y}
    (hg : Tendsto g l (𝓝 b₁)) (hb : b₁ ≠ b₂) : ∀ᶠ z in l, g z ≠ b₂ :=
  hg.eventually (isOpen_compl_singleton.eventually_mem hb)

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