Commit 2023-04-17 15:15 7a30096d

View on Github →

feat: port Analysis.NormedSpace.AddTorsor (#3477)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/AddTorsor.lean

added def AffineMap.ofMapMidpoint

added theorem AffineSubspace.isClosed_direction_iff

added theorem antilipschitzWith_lineMap

added theorem dist_center_homothety

added theorem dist_homothety_center

added theorem dist_homothety_self

added theorem dist_left_lineMap

added theorem dist_left_midpoint

added theorem dist_lineMap_left

added theorem dist_lineMap_lineMap

added theorem dist_lineMap_right

added theorem dist_midpoint_left

added theorem dist_midpoint_midpoint_le'

added theorem dist_midpoint_midpoint_le

added theorem dist_midpoint_right

added theorem dist_right_lineMap

added theorem dist_right_midpoint

added theorem dist_self_homothety

added theorem eventually_homothety_image_subset_of_finite_subset_interior

added theorem eventually_homothety_mem_of_mem_interior

added theorem lipschitzWith_lineMap

Modified Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean

deleted def AffineEquiv.Simps.symmApply

added def AffineEquiv.Simps.symm_apply