Commit 2024-06-20 19:07 19f8cc69

View on Github →

chore: move some lemmas to Analysis.Normed.Group.Uniform (#13945) From #13713.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Normed/Field/Basic.lean

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

Modified Mathlib/Analysis/Normed/Group/BallSphere.lean

Modified Mathlib/Analysis/Normed/Group/Basic.lean

deleted theorem AntilipschitzWith.le_mul_nnnorm'

deleted theorem AntilipschitzWith.le_mul_norm'

deleted theorem AntilipschitzWith.le_mul_norm_div

deleted theorem AntilipschitzWith.mul_div_lipschitzWith

deleted theorem AntilipschitzWith.mul_lipschitzWith

deleted theorem Isometry.nnnorm_map_of_map_one

deleted theorem Isometry.norm_map_of_map_one

deleted theorem LipschitzOnWith.norm_div_le_of_le

deleted theorem LipschitzWith.div

deleted theorem LipschitzWith.mul'

deleted theorem LipschitzWith.nnorm_le_mul'

deleted theorem LipschitzWith.norm_div_le_of_le

deleted theorem LipschitzWith.norm_le_mul'

deleted theorem MonoidHomClass.antilipschitz_of_bound

deleted theorem MonoidHomClass.continuous_of_bound

deleted theorem MonoidHomClass.isometry_iff_norm

deleted theorem MonoidHomClass.lipschitz_of_bound

deleted theorem MonoidHomClass.lipschitz_of_bound_nnnorm

deleted theorem MonoidHomClass.uniformContinuous_of_bound

deleted theorem OneHomClass.bound_of_antilipschitz

deleted theorem abs_dist_sub_le_dist_mul_mul

deleted theorem antilipschitzWith_inv_iff

deleted theorem cauchySeq_prod_of_eventually_eq

deleted theorem dist_div_div_le

deleted theorem dist_div_div_le_of_le

deleted theorem dist_div_eq_dist_mul_left

deleted theorem dist_div_eq_dist_mul_right

deleted theorem dist_mul_mul_le

deleted theorem dist_mul_mul_le_of_le

deleted theorem dist_mul_self_left

deleted theorem dist_mul_self_right

deleted theorem dist_self_div_left

deleted theorem dist_self_div_right

deleted theorem dist_self_mul_left

deleted theorem dist_self_mul_right

deleted theorem edist_mul_mul_le

deleted theorem lipschitzOnWith_iff_norm_div_le

deleted theorem lipschitzOnWith_inv_iff

deleted theorem lipschitzWith_iff_norm_div_le

deleted theorem lipschitzWith_inv_iff

deleted theorem lipschitzWith_one_nnnorm'

deleted theorem lipschitzWith_one_norm'

deleted theorem locallyLipschitz_inv_iff

deleted theorem nndist_mul_mul_le

deleted theorem uniformContinuous_nnnorm'

deleted theorem uniformContinuous_norm'

Modified Mathlib/Analysis/Normed/Group/Completeness.lean

Modified Mathlib/Analysis/Normed/Group/Completion.lean

Modified Mathlib/Analysis/Normed/Group/Hom.lean

Modified Mathlib/Analysis/Normed/Group/InfiniteSum.lean

Modified Mathlib/Analysis/Normed/Group/Lemmas.lean

Modified Mathlib/Analysis/Normed/Group/Pointwise.lean

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

added theorem AntilipschitzWith.le_mul_nnnorm'

added theorem AntilipschitzWith.le_mul_norm'

added theorem AntilipschitzWith.le_mul_norm_div

added theorem AntilipschitzWith.mul_div_lipschitzWith

added theorem AntilipschitzWith.mul_lipschitzWith

added theorem Isometry.nnnorm_map_of_map_one

added theorem Isometry.norm_map_of_map_one

added theorem LipschitzOnWith.norm_div_le_of_le

added theorem LipschitzWith.div

added theorem LipschitzWith.mul'

added theorem LipschitzWith.nnorm_le_mul'

added theorem LipschitzWith.norm_div_le_of_le

added theorem LipschitzWith.norm_le_mul'

added theorem MonoidHomClass.antilipschitz_of_bound

added theorem MonoidHomClass.continuous_of_bound

added theorem MonoidHomClass.isometry_iff_norm

added theorem MonoidHomClass.lipschitz_of_bound

added theorem MonoidHomClass.lipschitz_of_bound_nnnorm

added theorem MonoidHomClass.uniformContinuous_of_bound

added theorem OneHomClass.bound_of_antilipschitz

added theorem abs_dist_sub_le_dist_mul_mul

added theorem antilipschitzWith_inv_iff

added theorem cauchySeq_prod_of_eventually_eq

added theorem dist_div_div_le

added theorem dist_div_div_le_of_le

added theorem dist_div_eq_dist_mul_left

added theorem dist_div_eq_dist_mul_right

added theorem dist_mul_mul_le

added theorem dist_mul_mul_le_of_le

added theorem dist_mul_self_left

added theorem dist_mul_self_right

added theorem dist_self_div_left

added theorem dist_self_div_right

added theorem dist_self_mul_left

added theorem dist_self_mul_right

added theorem edist_mul_mul_le

added theorem lipschitzOnWith_iff_norm_div_le

added theorem lipschitzOnWith_inv_iff

added theorem lipschitzWith_iff_norm_div_le

added theorem lipschitzWith_inv_iff

added theorem lipschitzWith_one_nnnorm'

added theorem lipschitzWith_one_norm'

added theorem locallyLipschitz_inv_iff

added theorem nndist_mul_mul_le

added theorem uniformContinuous_nnnorm'

added theorem uniformContinuous_norm'

Modified Mathlib/Analysis/Normed/Order/Lattice.lean

Modified Mathlib/Analysis/NormedSpace/LinearIsometry.lean