Commit 2025-04-07 09:08 7874e38f

View on Github →

chore(Geometry/Euclidean/SignedDist): rename signedDist to signedInfDist (#23646) This is to allow for a signedDist function on points. Since signedDist is very new, I hope we don't need to add deprecations.

Estimated changes

Modified Mathlib/Geometry/Euclidean/SignedDist.lean

deleted theorem Affine.Simplex.abs_signedDist_eq_dist_of_mem_affineSpan_range

added theorem Affine.Simplex.abs_signedInfDist_eq_dist_of_mem_affineSpan_range

deleted theorem Affine.Simplex.signedDist_affineCombination

deleted theorem Affine.Simplex.signedDist_apply_of_ne

deleted theorem Affine.Simplex.signedDist_apply_self

added theorem Affine.Simplex.signedInfDist_affineCombination

added theorem Affine.Simplex.signedInfDist_apply_of_ne

added theorem Affine.Simplex.signedInfDist_apply_self

deleted theorem AffineSubspace.abs_signedDist_eq_dist_of_mem_affineSpan_insert

added theorem AffineSubspace.abs_signedInfDist_eq_dist_of_mem_affineSpan_insert

deleted theorem AffineSubspace.signedDist_apply

deleted theorem AffineSubspace.signedDist_apply_of_mem

deleted theorem AffineSubspace.signedDist_apply_self

deleted theorem AffineSubspace.signedDist_eq_const_of_left_mem

deleted theorem AffineSubspace.signedDist_linear

deleted theorem AffineSubspace.signedDist_linear_apply

added theorem AffineSubspace.signedInfDist_apply

added theorem AffineSubspace.signedInfDist_apply_of_mem

added theorem AffineSubspace.signedInfDist_apply_self

added theorem AffineSubspace.signedInfDist_eq_const_of_mem

added theorem AffineSubspace.signedInfDist_linear

added theorem AffineSubspace.signedInfDist_linear_apply