Commit 2021-04-08 06:49 9c2a3e7e

View on Github →

refactor(analysis/normed_space/add_torsor): generalize to semi_normed_space (#7016) This part of a series of PR to include the theory of semi_normed_space in mathlib.

Estimated changes

Modified src/analysis/normed_space/add_torsor.lean

modified theorem affine_map.continuous_linear_iff

modified def affine_map.of_map_midpoint

modified theorem isometric.dist_point_reflection_self

modified theorem isometric.point_reflection_fixed_iff

modified theorem lipschitz_with.vadd

modified theorem lipschitz_with.vsub

added def pseudo_metric_space_of_normed_group_of_add_torsor