Theorems · Theorem · general topology

ContinuousAt.eventually_ne

∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T1Space Y] {g : X → Y}
  {x : X} {y : Y}, ContinuousAt g x → g x ≠ y → ∀ᶠ (z : X) in nhds x, g z ≠ y

Defined in

Mathlib.Topology.Separation.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceT1Space