Theorem CompleteSpace.fst_of_prod

Modification history

2023-10-15 21:38
Mathlib/Topology/UniformSpace/Cauchy.lean
feat: drop more `CompleteSpace` assumptions (#7691) …
Added CompleteSpace.fst_of_prodView on Github →