Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-30 14:54 3398efa6

View on Github →

feat(topology/homeomorph): homeo of continuous equivalence from compact to T2 (#11072)

Estimated changes

Modified src/topology/homeomorph.lean

added theorem continuous.continuous_symm_of_equiv_compact_to_t2

added theorem continuous.homeo_of_equiv_compact_to_t2.t1_counterexample

added def continuous.homeo_of_equiv_compact_to_t2

deleted theorem homeomorph.compact_space

deleted theorem homeomorph.t2_space