Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-17 03:34 08a070b4

View on Github →

chore(topology/instances/ennreal): golf a proof (#9767)

Estimated changes

Modified src/topology/basic.lean

added theorem continuous_of_const

added theorem filter.eventually_eq.continuous_at

Modified src/topology/instances/ennreal.lean