Commit 2024-05-06 15:07 57511d5f

View on Github →

feat(CompactOpen): add instances (#12667)

Estimated changes

Modified Mathlib/Topology/CompactOpen.lean

added theorem ContinuousMap.inseparable_coe

added theorem ContinuousMap.specializes_coe

Modified Mathlib/Topology/Separation.lean

added theorem IsCompact.exists_isOpen_closure_subset

added theorem IsCompact.lift'_closure_nhdsSet

added theorem RegularSpace.of_lift'_closure_le