Mathlib Map

Theorems · Theorem · general topology

Cauchy.prod

∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : UniformSpace β] {f : Filter α} {g : Filter β},
  Cauchy f → Cauchy g → Cauchy (f ×ˢ g)
Defined in
Mathlib.Topology.UniformSpace.Cauchy
Cited by
4 results in Mathlib
Foundations
Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
UniformSpaceUniformSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CompleteSpace.fst_of_prod · cited by 2CompleteSpace.fst_of_prodCauchySeq.prodMk · cited by 2CauchySeq.prodMkCompleteSpace.snd_of_prod · cited by 1CompleteSpace.snd_of_prodCauchySeq.prodMap · cited by 0CauchySeq.prodMapFilter · cited by 8121FilterUniformSpace · cited by 2040UniformSpaceSProd.sprod · cited by 1750SProd.sprodFilter.NeBot · cited by 853Filter.NeBotCauchy · cited by 115CauchyFilter.map_fst_prod · cited by 5Filter.map_fst_prodFilter.map_snd_prod · cited by 5Filter.map_snd_prodCauchy.prodCITED BYCITES

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by4

Results whose statement or proof uses this declaration.