Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-13 07:40 f1f40840

View on Github →

feat(topology/algebra/ordered/basic): basis for the neighbourhoods of top/bot (#8283)

Estimated changes

added theorem nhds_bot_basis
added theorem nhds_top_basis
added theorem ennreal.nhds_top_basis
added theorem nnreal.nhds_zero
added theorem nnreal.nhds_zero_basis