Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-26 12:12 9b09f906

View on Github →

feat(ennreal): some lemmas about ennreal (#4262) Also some lemmas about norms in (e)nnreal.

Estimated changes

Modified src/analysis/normed_space/basic.lean

modified def nnnorm

added theorem real.ennnorm_eq_of_real

added theorem real.nnnorm_coe_eq_self

added theorem real.nnnorm_of_nonneg

added theorem real.norm_of_nonneg

Modified src/data/real/ennreal.lean

added theorem ennreal.mul_lt_top_iff

added theorem ennreal.of_real_le_of_le_to_real

Modified src/measure_theory/borel_space.lean

Modified src/topology/instances/ennreal.lean

modified theorem ennreal.continuous_coe

added theorem ennreal.continuous_coe_iff