Commit 2022-06-09 18:12 7b4680fe

View on Github →

feat(analysis/inner_product_space/pi_L2): Distance formula in the euclidean space (#14642) A few missing results about pi_Lp 2 and euclidean_space.

Estimated changes

Modified src/analysis/inner_product_space/pi_L2.lean

added theorem euclidean_space.dist_eq

added theorem euclidean_space.edist_eq

added theorem euclidean_space.nndist_eq

Modified src/analysis/normed_space/pi_Lp.lean

added theorem pi_Lp.dist_eq_of_L2

added theorem pi_Lp.edist_eq_of_L2

added theorem pi_Lp.nndist_eq_of_L2