Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-29 14:50 65bdbabc

View on Github →

chore(topology/instances/ennreal): simplify some statements&proofs (#1750) API changes:

  • nhds_top: use ⨅a ≠ ∞ instead of ⨅a:{a:ennreal // a ≠ ⊤}
  • nhds_zero, nhds_of_ne_top : similarly to nhds_top
  • tendsto_nhds: get rid of the intermediate set n.

Estimated changes

modified theorem ennreal.nhds_of_ne_top
modified theorem ennreal.nhds_top
modified theorem ennreal.nhds_zero