Theorem exists_compact_closed_between

Modification history

2024-01-18 09:44

Mathlib/Topology/Separation.lean

feat: construct Haar measure in locally compact non-Hausdorff groups (#9746) …

Modified exists_compact_closed_between View on Github →

2023-10-31 17:03

Mathlib/Topology/Separation.lean

feat: new class `ClosableCompactSubsetOpenSpace` of topological spaces (#7860) …

Added exists_compact_closed_between View on Github →