Commit 2025-10-29 12:32 737069ed

View on Github →

feat(Topology/Sets): Singleton instances for (Nonempty)Compacts (#31035)

Estimated changes

Modified Mathlib/Topology/Sets/Compacts.lean

added theorem TopologicalSpace.Compacts.map_singleton

added theorem TopologicalSpace.Compacts.mem_singleton

added theorem TopologicalSpace.Compacts.singleton_prod_singleton

added theorem TopologicalSpace.NonemptyCompacts.mem_singleton

added theorem TopologicalSpace.NonemptyCompacts.singleton_prod_singleton

added theorem TopologicalSpace.NonemptyCompacts.toCloseds_singleton

added theorem TopologicalSpace.NonemptyCompacts.toCompacts_singleton