Topology & Zorn's Lemma v10.1.0

Verified to be compatible with Coq versions 8.12.2, 8.13.2, 8.14.1, 8.15.0, 8.16.1, 8.17.1, 8.18+rc1.

Breaking changes:

• 23e752a, definition of ProductTopology2_basis changed to use EnsembleProduct. The lemma continuous_2arg_compose is removed, because it was an exact duplicate of continuous_composition_2arg.
• a60c821, the lemma ZornsLemma.FiniteTypes.finite_couple is moved to ZornsLemma.Finite_sets.finite_couple.

Other notable changes or additions:

• f784257, The unit circle in ℝ² is homeomorphic to the unit interval with ends identified.
• bd08c83, Refine the proof that every compact Hausdorff space is normal. Now without using the axiom of choice.

Git Log of changes: v10.0.1...v10.1.0

Topology & Zorn’s Lemma v10.0.1

This is the last release compatible with Coq v8.10.2 and v8.11.2. There has again been lots of clean-up which simplify the code and many minor facts have been added.

Verified to be compatible with Coq versions 8.10.2, 8.11.2, 8.12.2, 8.13.2, 8.14.1, 8.15.0.

Breaking changes:

• ac6d7cc, countable_union was renamed to countable_indexed_union.
• 9cd19e0 changed the statement of metric_space_open_ball_open.
• aff5164 removes countable_ens in favour of countable_type_ensemble. These statements were duplicates of eachother.
• f705646 changes the def. of continuous_2arg.
• 6c4682b rename MetricTopology_metrizable to MetricTopology_metrized.
• 8c534ad generalize the statement of induced_function_correct, but this makes it harder to apply
• d6d78d9 added a hint for unfolding open_neighborhood. This can break proof-scripts, because they might be solved earlier than before.

Git Log of changes: v9.0.0...v10.0.1

P.S.: There is no v10.0.0 release, because commit d6d78d9 broke a proof, which wasn't fixed in this tag.
The main reason for dropping support for v8.10 and v8.11 is, that they are missing some trigonometry facts in the stdlib, which are only available in v8.12.

Topology & Zorn's Lemma v9.0.0

This is the first release since the repos of Topology and ZornsLemma have been merged. There have been many breaking changes: moving stuff between files, renaming lemmas or changing the statements of lemmas. But also lots of additions. Major ones are quotient spaces and the sum topology.

We reformatted most proofs, to use a style using bullets and braces.

Verified to be compatible with Coq versions 8.10.2, 8.11.2, 8.12.2, 8.13.2.

Topology release for Coq 8.12

This is a maintenance release compatible with Coq 8.11 and 8.12, and Zorn's lemma version 8.11.0. It fixes various deprecations and adds support for building with Dune.