Commit 2019-09-03 13:42 a199f856

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