Commit 2021-01-19 18:42 21b0b012

View on Github →

feat(analysis/normed_space,topology/metric_space): distance between diagonal vectors (#5803) Add formulas for (e|nn|)dist between λ _, a and λ _, b as well as ∥(λ _, a)∥ and nnnorm (λ _, a).

Estimated changes

Modified src/analysis/normed_space/basic.lean

added theorem pi_nnnorm_const

added theorem pi_norm_const

Modified src/data/finset/basic.lean

added theorem finset.nonempty.forall_const

Modified src/data/finset/lattice.lean

added theorem finset.sup_const

Modified src/topology/metric_space/basic.lean

added theorem dist_pi_const

added theorem nndist_pi_const

Modified src/topology/metric_space/emetric_space.lean

added theorem edist_pi_const