Commit 2023-10-31 17:03 79577733

View on Github →

feat: new class ClosableCompactSubsetOpenSpace of topological spaces (#7860) Useful to uniformize proofs for T2 spaces and regular spaces, notably to discuss regular measures in topological groups.

Estimated changes

Modified Mathlib/Algebra/Support.lean

added theorem Function.range_eq_image_or_of_mulSupport_subset

Modified Mathlib/Topology/Compactness/LocallyCompact.lean

Modified Mathlib/Topology/Constructions.lean

added theorem mem_nhdsWithin_prod_iff

Modified Mathlib/Topology/Separation.lean

added theorem IsCompact.closure_subset_of_isOpen

added theorem exists_compact_closed_between

Modified Mathlib/Topology/Support.lean

added theorem HasCompactMulSupport.intro'

added theorem isCompact_range_of_mulSupport_subset_isCompact

Modified Mathlib/Topology/UniformSpace/Compact.lean

added theorem IsCompact.mem_uniformity_of_prod