Misc development - Githubissues

coq-community / topology

General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]

Other

46 stars 10 forks source link

Misc development #33

Closed Columbus240 closed 3 years ago

Columbus240 commented 3 years ago

I made some changes to the library, some of them are minor breaking changes.

Breaking changes for users of the library:

Rename product2_map_continuous to product2_map_continous_at
Show that metric_nonneg is admissible and remove it from the metric structure.

Additions:

Lemmas for closed Empty_set and closed Full_set
Characterize continuity via closed sets
Describe how Im commutes with IndexedUnion and FamilyUnion
Prove that bool and unit are finite types
Prove that Rmin and Rmax are continuous, via Rabs

Minor changes:

Moving a lemma from RTopology.v to Families.v
Reorder imports in WellOrders.v
Extract the lemma that id is a homeomorphism from another proof.