Commit 2020-10-25 21:53 a9d3ce8e

View on Github →

feat(analysis/normed_space/add_torsor): continuity of vadd/vsub (#4751) Prove that vadd/vsub are Lipschitz continuous, hence uniform continuous and continuous.

Estimated changes

Modified src/algebra/add_torsor.lean

added theorem vadd_eq_vadd_iff_neg_add_eq_vsub

added theorem vadd_eq_vadd_iff_sub_eq_vsub

added theorem vsub_sub_vsub_comm

Modified src/analysis/normed_space/add_torsor.lean

added theorem continuous.vadd

added theorem continuous.vsub

added theorem continuous_at.vadd

added theorem continuous_at.vsub

added theorem continuous_vadd

added theorem continuous_vsub

added theorem continuous_within_at.vadd

added theorem continuous_within_at.vsub

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.vadd

added theorem filter.tendsto.vsub

added theorem lipschitz_with.vadd

added theorem lipschitz_with.vsub

modified def metric_space_of_normed_group_of_add_torsor

added theorem nndist_vadd_vadd_le

added theorem nndist_vsub_vsub_le

added theorem uniform_continuous_vadd

added theorem uniform_continuous_vsub

Modified src/analysis/normed_space/basic.lean