Commit 2022-10-23 13:05 3798ca1d

View on Github →

feat(topology/metric_space/basic): Distance between constant functions (#16958) The distance between λ _, a and λ _, b is at most the distance between a and b. Also rename pi_norm_le_iff to pi_norm_le_iff_of_nonneg.

Estimated changes

Modified src/analysis/asymptotics/asymptotics.lean

Modified src/analysis/matrix.lean

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

modified theorem norm_le_pi_norm'

added theorem pi_nnnorm_const_le'

modified theorem pi_nnnorm_le_iff'

added theorem pi_norm_const_le'

deleted theorem pi_norm_le_iff'

added theorem pi_norm_le_iff_of_nonempty'

added theorem pi_norm_le_iff_of_nonneg'

Modified src/analysis/normed_space/finite_dimension.lean

Modified src/analysis/normed_space/multilinear.lean

Modified src/analysis/normed_space/star/matrix.lean

Modified src/measure_theory/covering/besicovitch_vector_space.lean

Modified src/topology/metric_space/basic.lean

added theorem dist_pi_const_le

added theorem dist_pi_le_iff'

added theorem nndist_pi_const_le

Modified src/topology/metric_space/emetric_space.lean

modified theorem edist_pi_const

added theorem edist_pi_const_le