Commit 2023-05-30 23:20 6e1dbc75

View on Github →

chore: Rename Alenxandroff to Compactification.OnePoint (#4506) We rename Alexandroff to Compactification.OnePoint to avoid future name conflicts (with e.g. Alexandroff topological spaces). See this zulip thread.

Estimated changes

deleted theorem Alexandroff.coe_eq_coe
deleted theorem Alexandroff.coe_injective
deleted theorem Alexandroff.coe_ne_infty
deleted theorem Alexandroff.compl_infty
deleted def Alexandroff.infty
deleted theorem Alexandroff.infty_ne_coe
deleted theorem Alexandroff.isOpenMap_coe
deleted theorem Alexandroff.isOpen_def
deleted theorem Alexandroff.le_nhds_infty
deleted theorem Alexandroff.nhds_coe_eq
deleted theorem Alexandroff.nhds_infty_eq
deleted def Alexandroff.some
deleted def Alexandroff
added theorem OnePoint.coe_eq_coe
added theorem OnePoint.coe_injective
added theorem OnePoint.coe_ne_infty
added theorem OnePoint.compl_infty
added def OnePoint.infty
added theorem OnePoint.infty_ne_coe
added theorem OnePoint.isOpenMap_coe
added theorem OnePoint.isOpen_def
added theorem OnePoint.le_nhds_infty
added theorem OnePoint.nhds_coe_eq
added theorem OnePoint.nhds_infty_eq
added def OnePoint.some
added def OnePoint