coq-community / topology

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

Characterize RTop and its subspaces #35

Open Columbus240 opened 3 years ago

Columbus240 commented 3 years ago

There are multiple ways to characterize RTop and its subspaces (up to homeomorphism) based on order or metric properties. Such theorems could help transport topological properties.

IIRC the following statements are true:

I'm sure there's some way to use the metric structure, but haven't yet looked into a precise statement. Metrically complete and separable are probably important again.

Small conjecture: an order topology is separable/second-countable iff there's a countable dense subset. A subset A of an ordered set X shall be called dense if for all x, y : X with x <= y there exists a : A such that x <= a <= y.