Theorems · Theorem · general topology

MapClusterPt.prodMap

∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {α : Type u_5} {β : Type u_6}
  {f : α → X} {g : β → Y} {la : Filter α} {lb : Filter β} {x : X} {y : Y},
  MapClusterPt x la f → MapClusterPt y lb g → MapClusterPt (x, y) (la ×ˢ lb) (Prod.map f g)

Defined in

Mathlib.Topology.Constructions

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace