Theorems · Theorem · general topology

Filter.Tendsto.prodMap

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_6} {f : α → γ} {g : β → δ} {a : Filter α} {b : Filter β}
  {c : Filter γ} {d : Filter δ},
  Filter.Tendsto f a c → Filter.Tendsto g b d → Filter.Tendsto (Prod.map f g) (a ×ˢ b) (c ×ˢ d)

Defined in

Mathlib.Order.Filter.Prod

Cited by

38 results in Mathlib

Foundations

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