Commit 2026-07-28 15:02 fb2c2f59

View on Github →

feat: tag lemmas with compactness and closedness (#39371)

Estimated changes

Modified Mathlib/Topology/Basic.lean

modified theorem isClosed_empty

modified theorem isClosed_univ

Modified Mathlib/Topology/Closure.lean

modified theorem IsClosed.closure_eq

Modified Mathlib/Topology/Compactness/Compact.lean

modified theorem Set.Finite.isCompact

Modified Mathlib/Topology/MetricSpace/ProperSpace.lean

Modified Mathlib/Topology/Order/Compact.lean

Modified Mathlib/Topology/Order/OrderClosed.lean

Modified Mathlib/Topology/Separation/Basic.lean

Modified Mathlib/Topology/Separation/Hausdorff.lean

Created MathlibTest/Compactness.lean