Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-18 16:59 100975e9

View on Github →

feat(geometry/euclidean/inversion) new file (#14692)

Define euclidean_geometry.inversion.
Prove Ptolemy's inequality.

Estimated changes

Modified src/analysis/inner_product_space/basic.lean

added theorem dist_div_norm_sq_smul

Created src/geometry/euclidean/inversion.lean

added theorem euclidean_geometry.dist_center_inversion

added theorem euclidean_geometry.dist_inversion_center

added theorem euclidean_geometry.dist_inversion_inversion

added def euclidean_geometry.inversion

added theorem euclidean_geometry.inversion_bijective

added theorem euclidean_geometry.inversion_dist_center

added theorem euclidean_geometry.inversion_injective

added theorem euclidean_geometry.inversion_inversion

added theorem euclidean_geometry.inversion_involutive

added theorem euclidean_geometry.inversion_of_mem_sphere

added theorem euclidean_geometry.inversion_self

added theorem euclidean_geometry.inversion_surjective

added theorem euclidean_geometry.inversion_vsub_center

added theorem euclidean_geometry.mul_dist_le_mul_dist_add_mul_dist