search

coq-community / topology

General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]
Other
46 stars 10 forks source link

Rework `Completeness` and `Completion` #44

Closed Columbus240 closed 1 year ago

Columbus240 commented 1 year ago

Before this PR, the definition of complete and many statements in Completeness and Completion explicitly mention the MetricTopology. This makes it hard to use these results with arbitrary metrizable topologies which might not be defined via their metric. For example RTop.

This PR uses the assumption metrizes X d instead, whenever possible.

The statement of completion_exists has been adapted as well, and the proof has been split into separate lemmas. The lemma d_restriction_metric has been moved to MetricSpaces.

stop-cran commented 1 year ago

Great work!

Columbus240 commented 1 year ago

Thanks!