Theorems · Theorem · general topology

tendsto_pi_nhds

∀ {Y : Type v} {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] {f : Y → (i : ι) → A i}
  {g : (i : ι) → A i} {u : Filter Y},
  Filter.Tendsto f u (nhds g) ↔ ∀ (x : ι), Filter.Tendsto (fun i => f i x) u (nhds (g x))

Defined in

Mathlib.Topology.Constructions

Cited by

58 results in Mathlib

Foundations

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

Assumes

TopologicalSpace