Commit 2024-03-20 02:43 4c8f5f4b

View on Github →

feat(Separation): define R0 spaces (#10621) Generalize coclosedCompact_eq_cocompact and relativelyCompact.

Estimated changes

Modified Mathlib/Topology/Compactification/OnePoint.lean

Modified Mathlib/Topology/Compactness/Compact.lean

added theorem Filter.compl_mem_coclosedCompact

added theorem Filter.mem_coclosedCompact_iff

Modified Mathlib/Topology/Inseparable.lean

added theorem Specializes.fst

added theorem Specializes.snd

Modified Mathlib/Topology/Separation.lean

modified theorem Bornology.relativelyCompact.isBounded_iff

modified def Bornology.relativelyCompact

modified theorem Bornology.relativelyCompact_eq_inCompact

modified theorem Filter.coclosedCompact_eq_cocompact

modified theorem Filter.coclosedCompact_le_cofinite

added theorem Inducing.r0Space

added theorem Set.Finite.isCompact_closure

modified theorem Specializes.symm

added theorem isCompact_closure_singleton

Modified Mathlib/Topology/Support.lean