Theorems · Theorem · general topology

Topology.IsClosedEmbedding.tendsto_nhds_iff

∀ {X : Type u_1} {Y : Type u_2} {ι : Type u_4} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {g : ι → X} {l : Filter ι} {x : X},
  Topology.IsClosedEmbedding f → (Filter.Tendsto g l (nhds x) ↔ Filter.Tendsto (f ∘ g) l (nhds (f x)))

Defined in

Mathlib.Topology.Maps.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace