Theorems · Theorem · general topology

Filter.Tendsto.prodMk_nhds

∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {γ : Type u_5} {x : X} {y : Y}
  {f : Filter γ} {mx : γ → X} {my : γ → Y},
  Filter.Tendsto mx f (nhds x) → Filter.Tendsto my f (nhds y) → Filter.Tendsto (fun c => (mx c, my c)) f (nhds (x, y))

Defined in

Mathlib.Topology.Constructions.SumProd

Cited by

46 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace