Mathlib Changelog
Changelog
About
Github
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