Commit 2021-07-17 16:55 3782c193
View on Github →feat(topology/algebra/ordered): add nhds_top_basis_Ici
and nhds_bot_basis_Iic
(#8349)
Also add ennreal.nhds_zero_basis_Iic
and ennreal.supr_div
.
feat(topology/algebra/ordered): add nhds_top_basis_Ici
and nhds_bot_basis_Iic
(#8349)
Also add ennreal.nhds_zero_basis_Iic
and ennreal.supr_div
.