Theorem IsCompact.closure_subset_of_isOpen

Modification history

2024-01-29 18:36

Mathlib/Topology/Separation.lean

feat(Topology/Separation): define R₁ spaces, review API (#10085) …

Modified IsCompact.closure_subset_of_isOpen View on Github →

2024-01-18 09:44

Mathlib/Topology/Separation.lean

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

Modified IsCompact.closure_subset_of_isOpen View on Github →

2023-10-31 17:03

Mathlib/Topology/Separation.lean

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

Added IsCompact.closure_subset_of_isOpen View on Github →