Theorems · Theorem · general topology

not_continuousAt_of_tendsto

∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {l₁ : Filter X}
  {l₂ : Filter Y} {x : X},
  Filter.Tendsto f l₁ l₂ → ∀ [l₁.NeBot], l₁ ≤ nhds x → Disjoint (nhds (f x)) l₂ → ¬ContinuousAt f x

If a function f tends to somewhere other than 𝓝 (f x) at x, then f is not continuous at x

Defined in

Mathlib.Topology.Continuous

Cited by

6 results in Mathlib

Foundations

Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceFilter.NeBot