Commit 2022-02-14 07:20 25ebf419

View on Github →

chore(analysis): move some code (#12008) Move the code that doesn't rely on normed_space from analysis.normed_space.add_torsor to analysis.normed.group.add_torsor.

Estimated changes

Created src/analysis/normed/group/add_torsor.lean

added theorem continuous.vsub

added theorem continuous_at.vsub

added theorem continuous_vsub

added theorem continuous_within_at.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 theorem filter.tendsto.line_map

added theorem filter.tendsto.midpoint

added theorem filter.tendsto.vsub

added def isometric.const_vadd

added def isometric.const_vsub

added def isometric.vadd_const

added theorem lipschitz_with.vadd

added theorem lipschitz_with.vsub

added def metric_space_of_normed_group_of_add_torsor

added theorem nndist_vadd_vadd_le

added theorem nndist_vsub_vsub_le

added def pseudo_metric_space_of_normed_group_of_add_torsor

added theorem uniform_continuous_vadd

added theorem uniform_continuous_vsub

added theorem vadd_ball

added theorem vadd_closed_ball

added theorem vadd_sphere

Modified src/analysis/normed_space/add_torsor.lean

deleted theorem continuous.vsub

deleted theorem continuous_at.vsub

deleted theorem continuous_vsub

deleted theorem continuous_within_at.vsub

deleted theorem dist_eq_norm_vsub

deleted theorem dist_vadd_cancel_left

deleted theorem dist_vadd_cancel_right

deleted theorem dist_vadd_left

deleted theorem dist_vadd_right

deleted theorem dist_vadd_vadd_le

deleted theorem dist_vsub_cancel_left

deleted theorem dist_vsub_cancel_right

deleted theorem dist_vsub_vsub_le

deleted theorem edist_vadd_vadd_le

deleted theorem edist_vsub_vsub_le

deleted theorem filter.tendsto.line_map

deleted theorem filter.tendsto.midpoint

deleted theorem filter.tendsto.vsub

deleted def isometric.const_vadd

deleted def isometric.const_vsub

deleted def isometric.vadd_const

deleted theorem lipschitz_with.vadd

deleted theorem lipschitz_with.vsub

deleted def metric_space_of_normed_group_of_add_torsor

deleted theorem nndist_vadd_vadd_le

deleted theorem nndist_vsub_vsub_le

deleted def pseudo_metric_space_of_normed_group_of_add_torsor

deleted theorem uniform_continuous_vadd

deleted theorem uniform_continuous_vsub

deleted theorem vadd_ball

deleted theorem vadd_closed_ball

deleted theorem vadd_sphere