ordered): add `nhds_top_basis_Ici` and `nhds_bot_basis_Iic` (#8349)

Commit

4 years ago

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`.

Author

urkud

Parents

8139d7eb

mathlib3 3782c193 - feat(topology/algebra/ordered): add `nhds_top_basis_Ici` and `nhds_bot_basis_Iic` (#8349)

mathlib3
3782c193 - feat(topology/algebra/ordered): add `nhds_top_basis_Ici` and `nhds_bot_basis_Iic` (#8349)