Theorems · Theorem · general topology

tendsto_inf_principal_nhds_iff_of_forall_eq

∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {x : X} {f : α → X} {l : Filter α} {s : Set α},
  (∀ a ∉ s, f a = x) → (Filter.Tendsto f (l ⊓ Filter.principal s) (nhds x) ↔ Filter.Tendsto f l (nhds x))

Suppose that f sends the complement to s to a single point x, and l is some filter. Then f tends to x along l restricted to s if and only if it tends to x along l.

Defined in

Mathlib.Topology.Neighborhoods

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpace