Mathlib v3 is deprecated. Go to Mathlib v4

Theorem exists_open_between_and_is_compact_closure

Modification history

2022-08-29 16:05
src/topology/separation.lean
feat(topology): composition of continuous functions is continuous w.r.t. the compact-open topologies (#15721) …
Modified exists_open_between_and_is_compact_closureView on Github →
2022-07-13 00:00
src/topology/separation.lean
refactor(topology/separation): rename `regular_space` to `t3_space` (#15169) …
Modified exists_open_between_and_is_compact_closureView on Github →
2022-01-14 08:37
src/topology/separation.lean
feat(topology/subset_properties): some compactness properties (#11425) …
Added exists_open_between_and_is_compact_closureView on Github →