Mathlib Map

Theorems · Theorem · general topology

CompleteSpace.fst_of_prod

∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : UniformSpace β] [CompleteSpace (α × β)]
  [h : Nonempty β], CompleteSpace α
Defined in
Mathlib.Topology.UniformSpace.Cauchy
Cited by
2 results in Mathlib
Foundations
Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
UniformSpaceUniformSpaceCompleteSpaceNonempty
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

fst_integral · cited by 3fst_integralcompleteSpace_prod_of_nonempty · cited by 0completeSpace_prod_of_non…Filter · cited by 8121Filternhds · cited by 5554nhdsCompleteSpace · cited by 2532CompleteSpaceUniformSpace · cited by 2040UniformSpaceSProd.sprod · cited by 1750SProd.sprodFilter.map · cited by 819Filter.mapCauchy · cited by 115Cauchynhds_prod_eq · cited by 84nhds_prod_eqFilter.map_mono · cited by 63Filter.map_monoCompleteSpace.complete · cited by 19CompleteSpace.completeFilter.map_fst_prod · cited by 5Filter.map_fst_prodCauchy.prod · cited by 4Cauchy.prodcauchy_pure · cited by 2cauchy_pureCompleteSpace.fst_of_prodCITED BYCITES

Cites13

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

Cited by2

Results whose statement or proof uses this declaration.