Commit 2023-04-17 06:32 e29b9ea5

View on Github →

feat: port Analysis.Normed.Group.AddTorsor (#3063)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Normed/Group/AddTorsor.lean

added theorem Continuous.vsub

added theorem Filter.Tendsto.lineMap

added theorem Filter.Tendsto.midpoint

added theorem Filter.Tendsto.vsub

added def IsometryEquiv.constVSub

added def IsometryEquiv.vaddConst

added theorem LipschitzWith.vadd

added theorem LipschitzWith.vsub

added theorem continuous_vsub

added theorem dist_eq_norm_vsub'

added theorem dist_eq_norm_vsub

added theorem dist_vadd_cancel_left

added theorem dist_vadd_cancel_right

added theorem dist_vadd_left

added theorem dist_vadd_right

added theorem dist_vadd_vadd_le

added theorem dist_vsub_cancel_left

added theorem dist_vsub_cancel_right

added theorem dist_vsub_vsub_le

added theorem edist_vadd_vadd_le

added theorem edist_vsub_vsub_le

added def metricSpaceOfNormedAddCommGroupOfAddTorsor

added theorem nndist_vadd_vadd_le

added theorem nndist_vsub_vsub_le

added def pseudoMetricSpaceOfNormedAddCommGroupOfAddTorsor

added theorem uniformContinuous_vadd

added theorem uniformContinuous_vsub