Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-03 13:42 a199f856

View on Github →

feat(topology/uniform_space): Abstract completions (#1374)

  • feat(topology/uniform_space): Abstract completions Define abstract completions, study their properties and derived constructions. Use this study in the concrete completion files, and for comparing completions constructed at different level of generality, especially for real numbers. This comes from the perfectoid spaces project.
  • Apply suggestions from code review by Johan Co-Authored-By: Johan Commelin johan@commelin.net
  • Fix build. When I created the PR, github complained it couldn't automatically merge, and I was not careful enough when I merged...
  • chore(topology/uniform_space): rename completion_pkg
  • fix(compare_reals): create namespace
  • Fix build

Estimated changes

added structure abstract_completion