Commit 2024-02-09 13:35 22ba268f

View on Github →

chore: rename declarations containing nNReal to nnreal (#10372)

Estimated changes

Modified Mathlib/Analysis/NormedSpace/Basic.lean

deleted theorem nnnorm_algebraMap_nNReal

added theorem nnnorm_algebraMap_nnreal

deleted theorem norm_algebraMap_nNReal

added theorem norm_algebraMap_nnreal

Modified Mathlib/Topology/ContinuousFunction/Ideals.lean

Modified Mathlib/Topology/MetricSpace/PartitionOfUnity.lean

deleted theorem EMetric.exists_continuous_nNReal_forall_closedBall_subset

added theorem EMetric.exists_continuous_nnreal_forall_closedBall_subset

deleted theorem Metric.exists_continuous_nNReal_forall_closedBall_subset

added theorem Metric.exists_continuous_nnreal_forall_closedBall_subset