Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_complete_Union_separated

Modification history

2022-02-17 07:43
src/topology/uniform_space/cauchy.lean
feat(topology/metric_space/gluing): metric space structure on sigma types (#11965) …
Added is_complete_Union_separatedView on Github →