Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nhds_within_Ici_basis_Ico

Modification history

2022-09-10 01:42
src/topology/algebra/order/basic.lean
feat(counterexamples/sorgenfrey_line): new file (#14820) …
Added nhds_within_Ici_basis_IcoView on Github →