Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-23 17:01 28e4bdfc

View on Github →

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

Estimated changes

added theorem complete_space_congr