Commit 2023-05-29 07:37 deff4e17

View on Github →

feat: add SigmaCompactSpace instances (#4458) forward-port of leanprover-community/mathlib#19100. Also adds a new lemma IsClosed.sigmaCompactSpace.

Estimated changes

Modified Mathlib/Topology/Constructions.lean

added theorem ULift.closedEmbedding_down

Modified Mathlib/Topology/SubsetProperties.lean

added theorem IsClosed.sigmaCompactSpace