Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-04 06:42 58de2a0a

View on Github →

chore(analysis): use nnnorm notation everywhere (#13930) This was done with a series of ad-hoc regular expressions, then cleaned up by hand.

Estimated changes

Modified src/analysis/analytic/composition.lean

Modified src/analysis/analytic/radius_liminf.lean

modified theorem formal_multilinear_series.radius_eq_liminf

Modified src/analysis/calculus/inverse.lean

Modified src/analysis/normed/group/hom.lean

modified def add_monoid_hom.mk_normed_group_hom'

Modified src/analysis/normed_space/banach.lean

Modified src/analysis/normed_space/enorm.lean

modified theorem enorm.map_smul

Modified src/analysis/normed_space/finite_dimension.lean

Modified src/analysis/normed_space/indicator_function.lean

Modified src/analysis/normed_space/linear_isometry.lean

modified theorem linear_isometry.nnnorm_map

modified theorem linear_isometry_equiv.nnnorm_map

Modified src/analysis/normed_space/multilinear.lean

modified theorem continuous_multilinear_map.le_of_op_nnnorm_le

modified theorem continuous_multilinear_map.le_op_nnnorm

Modified src/analysis/normed_space/operator_norm.lean

Modified src/measure_theory/constructions/borel_space.lean

modified theorem measurable.nnnorm

modified theorem measurable_ennnorm

Modified src/measure_theory/constructions/prod.lean

Modified src/measure_theory/function/conditional_expectation.lean

Modified src/measure_theory/function/l1_space.lean

modified theorem measure_theory.lintegral_nnnorm_zero

Modified src/measure_theory/function/l2_space.lean

Modified src/measure_theory/function/lp_space.lean

Modified src/measure_theory/function/simple_func_dense_lp.lean

Modified src/measure_theory/function/strongly_measurable.lean

Modified src/measure_theory/integral/set_to_l1.lean