mathlib

28e4bdfc - feat(topology): an `is_complete` set is a `complete_space` (#2037)

feat(topology): an `is_complete` set is a `complete_space` (#2037) * feat(*): misc simple lemmas * +1 lemma * Rename `inclusion_range` to `range_inclusion` Co-Authored-By: Johan Commelin <johan@commelin.net> * feat(topology): an `is_complete` set is a `complete_space` Also simplify a proof in `topology/metric_space/closeds`. * Use in `finite_dimension` Co-authored-by: Johan Commelin <johan@commelin.net>