Theorem completeSpace_prod_of_nonempty

Modification history

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