Skip to content

Topology & Zorn's Lemma v10.1.0

Latest
Latest
Compare
Choose a tag to compare
@Columbus240 Columbus240 released this 18 Aug 08:34
· 116 commits to master since this release
v10.1.0
384098e
This commit was signed with the committer’s verified signature.
Columbus240
GPG key ID: 1C1CCDFE31AC7CC0
Learn about vigilant mode.

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

Assets 2
Loading