Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-10-29 20:27
c8dae005
View on Github →
feat: add a uniqueness result for one-point compactification (
#18411
)
Estimated changes
Modified
Mathlib/Topology/Compactification/OnePoint.lean
added
theorem
OnePoint.elim_infty
added
theorem
OnePoint.elim_some
added
theorem
OnePoint.equivOfIsEmbeddingOfRangeEq_apply_coe
added
theorem
OnePoint.equivOfIsEmbeddingOfRangeEq_apply_infty
added
theorem
OnePoint.some_eq_iff