Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-11-21 11:20
1777cd53
View on Github →
chore(Topology/Sets): use prefix naming for
toCompacts
in
simps
(
#31591
)
Estimated changes
Modified
Mathlib/Topology/Sets/Compacts.lean
deleted
theorem
TopologicalSpace.NonemptyCompacts.toCompacts_singleton