Commit 2022-03-25 17:53 5925650f

View on Github →

chore(nnreal): rename lemmas based on real.to_nnreal when they mention of_real (#12937) Many lemma using real.to_nnreal mention of_real in their names. This PR tries to make things more coherent.

Estimated changes

Modified src/analysis/special_functions/pow.lean

Modified src/data/real/sqrt.lean

Modified src/measure_theory/constructions/borel_space.lean

Modified src/topology/instances/ennreal.lean

Modified src/topology/instances/nnreal.lean

added theorem continuous_real_to_nnreal

deleted theorem nnreal.continuous_of_real

deleted theorem nnreal.has_sum_of_real_of_nonneg

added theorem nnreal.has_sum_real_to_nnreal_of_nonneg

deleted theorem nnreal.tendsto_of_real

added theorem nnreal.tendsto_real_to_nnreal