[WIP] Topology, Uniform spaces & Reals

[johoelzl]

this is not finished yet I copied everything from my library_dev development and adapted it to changes like ^. to ., @[simp] lemma in one line, absolute imports...

This pull request adds a construction for the reals. The idea is to develop a topology library inclusive a formalization of uniform spaces and uniform completion.

I need to admit it is not clear if a lot of work is safed by using this approach, proofing that the field properties hold using Cauchy sequences in Isabelle is also quite short. Edit: But then we do not yet have any topological results on the reals in Isabelle at this point.

[gebner]

Sorry for asking this so late, but why does Prop have the Sierpinski topology (instead of the discrete one, for example)? From what I can tell this definition is only used in continuous_abs_rat.

[digama0]

I have to say, I'm worried about the maintainability here. You have a lot of new definitions, and it's not clear to me how much is necessary for the goal, or even exactly what the goal is since obviously you can get to the reals directly with a lot less work.

Why is ℝ defined as a quotient? ℚ should already be separated, so that the setoid construction is trivial.

[avigad]

@digama0 This should give us other useful constructions too, for little extra cost -- including the completion of an arbitrary metric space (and infrastructure to extend functions defined on the dense subsets), and (a generalization of) Lebesgue measure.

[digama0]

I'm fine with this construction because of its side effects, as you say, but we should be clear about what exactly are the goal posts and target uses of this library. This should help with separating the material into appropriately sized chunks and reuse in other areas. Even if there is a completion framework here, if no one knows how to use it other than the author it's useless. I think it is best to merge it now and work on making it more accessible as time goes on.

[johoelzl]

@gebner the Sierpinski topology allows us to express that a predicate is an open set: continuous p <-> open {x | p x}. There is currently no application of this (I think also not in continuous_abs_rat). Somehow it feels natural to use it for Prop and the discrete topology for bool.

@digama0 the Cauchy filters over rat are not separated, even as rat itself is separated. Hence the quotient over the separation relation. Alternatively, we could use the minimal Cauchy filters as completion. I chose the two-step construction, to introduce a general construction of separated uniform spaces. I guess a it would be a good idea to add a general construction of the quotient over Cauchy filters.

I can add some references and a rough idea how the completion process works. I also changed the title to emphasise that it is more about introducing topology than constructing the real numbers.

Currently the theories are very abstract, but in my experience this will be necessary anyway. When we introduce metric spaces we could derive more concrete theorems, but I'm not sure if this is really helpful.

[johoelzl]

I will reopen it when I'm finished with completeness and reorganized the real.lean file.