Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ennreal.continuous_coe_iff

Modification history

2020-12-16 07:31
src/topology/instances/ennreal.lean
chore(*): use notation `ℝ≥0` (#5391)
Modified ennreal.continuous_coe_iffView on Github →
2020-09-26 12:12
src/topology/instances/ennreal.lean
feat(ennreal): some lemmas about ennreal (#4262) …
Added ennreal.continuous_coe_iffView on Github →