Theorems · Theorem · general topology

Filter.Tendsto.eventually_ne

∀ {Y : Type u_2} {X : Type u_3} [inst : TopologicalSpace Y] [T1Space Y] {g : X → Y} {l : Filter X} {b₁ b₂ : Y},
  Filter.Tendsto g l (nhds b₁) → b₁ ≠ b₂ → ∀ᶠ (z : X) in l, g z ≠ b₂

Defined in

Mathlib.Topology.Separation.Basic

Cited by

11 results in Mathlib

Foundations

Depth 61 from the axioms · uses propext, Quot.sound

Assumes

TopologicalSpaceT1Space