Normed groups are uniform groups

This file proves lipschitzness of normed group operations and shows that normed groups are uniform groups.

instance NormedGroup.to_isIsometricSMul_right {E : Type u_2} [SeminormedGroup E] : IsIsometricSMul Eᵐᵒᵖ E

instance NormedAddGroup.to_isIsometricVAdd_right {E : Type u_2} [SeminormedAddGroup E] : IsIsometricVAdd Eᵃᵒᵖ E

theorem Isometry.norm_map_of_map_one {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] {f : E → F} (hi : Isometry f) (h₁ : f 1 = 1) (x : E) : ‖f x‖ = ‖x‖

theorem Isometry.norm_map_of_map_zero {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : E → F} (hi : Isometry f) (h₁ : f 0 = 0) (x : E) : ‖f x‖ = ‖x‖

@[simp]

theorem norm_map' {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [IsometryClass 𝓕 E F] [OneHomClass 𝓕 E F] (f : 𝓕) (x : E) : ‖f x‖ = ‖x‖

@[simp]

theorem norm_map {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [IsometryClass 𝓕 E F] [ZeroHomClass 𝓕 E F] (f : 𝓕) (x : E) : ‖f x‖ = ‖x‖

@[simp]

theorem nnnorm_map' {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [IsometryClass 𝓕 E F] [OneHomClass 𝓕 E F] (f : 𝓕) (x : E) : ‖f x‖₊ = ‖x‖₊

@[simp]

theorem nnnorm_map {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [IsometryClass 𝓕 E F] [ZeroHomClass 𝓕 E F] (f : 𝓕) (x : E) : ‖f x‖₊ = ‖x‖₊

@[simp]

theorem dist_mul_self_right {E : Type u_2} [SeminormedGroup E] (a b : E) : dist b (a * b) = ‖a‖

@[simp]

theorem dist_add_self_right {E : Type u_2} [SeminormedAddGroup E] (a b : E) : dist b (a + b) = ‖a‖

@[simp]

theorem dist_mul_self_left {E : Type u_2} [SeminormedGroup E] (a b : E) : dist (a * b) b = ‖a‖

@[simp]

theorem dist_add_self_left {E : Type u_2} [SeminormedAddGroup E] (a b : E) : dist (a + b) b = ‖a‖

@[simp]

theorem dist_div_eq_dist_mul_left {E : Type u_2} [SeminormedGroup E] (a b c : E) : dist (a / b) c = dist a (c * b)

@[simp]

theorem dist_sub_eq_dist_add_left {E : Type u_2} [SeminormedAddGroup E] (a b c : E) : dist (a - b) c = dist a (c + b)

@[simp]

theorem dist_div_eq_dist_mul_right {E : Type u_2} [SeminormedGroup E] (a b c : E) : dist a (b / c) = dist (a * c) b

@[simp]

theorem dist_sub_eq_dist_add_right {E : Type u_2} [SeminormedAddGroup E] (a b c : E) : dist a (b - c) = dist (a + c) b

theorem MonoidHomClass.lipschitz_of_bound {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [MonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ) (h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖) : LipschitzWith C.toNNReal ⇑f

A homomorphism f of seminormed groups is Lipschitz, if there exists a constant C such that for all x, one has ‖f x‖ ≤ C * ‖x‖. The analogous condition for a linear map of (semi)normed spaces is in Mathlib/Analysis/Normed/Operator/Basic.lean.

theorem AddMonoidHomClass.lipschitz_of_bound {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ) (h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖) : LipschitzWith C.toNNReal ⇑f

A homomorphism f of seminormed groups is Lipschitz, if there exists a constant C such that for all x, one has ‖f x‖ ≤ C * ‖x‖. The analogous condition for a linear map of (semi)normed spaces is in Mathlib/Analysis/Normed/Operator/Basic.lean.

theorem lipschitzOnWith_iff_norm_div_le {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] {s : Set E} {f : E → F} {C : NNReal} : LipschitzOnWith C f s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x / f y‖ ≤ ↑C * ‖x / y‖

theorem lipschitzOnWith_iff_norm_sub_le {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] {s : Set E} {f : E → F} {C : NNReal} : LipschitzOnWith C f s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x - f y‖ ≤ ↑C * ‖x - y‖

theorem LipschitzOnWith.norm_div_le {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] {s : Set E} {f : E → F} {C : NNReal} : LipschitzOnWith C f s → ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x / f y‖ ≤ ↑C * ‖x / y‖

Alias of the forward direction of lipschitzOnWith_iff_norm_div_le.

theorem LipschitzOnWith.norm_sub_le {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] {s : Set E} {f : E → F} {C : NNReal} : LipschitzOnWith C f s → ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x - f y‖ ≤ ↑C * ‖x - y‖

theorem LipschitzOnWith.norm_div_le_of_le {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] {s : Set E} {a b : E} {r : ℝ} {f : E → F} {C : NNReal} (h : LipschitzOnWith C f s) (ha : a ∈ s) (hb : b ∈ s) (hr : ‖a / b‖ ≤ r) : ‖f a / f b‖ ≤ ↑C * r

theorem LipschitzOnWith.norm_sub_le_of_le {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] {s : Set E} {a b : E} {r : ℝ} {f : E → F} {C : NNReal} (h : LipschitzOnWith C f s) (ha : a ∈ s) (hb : b ∈ s) (hr : ‖a - b‖ ≤ r) : ‖f a - f b‖ ≤ ↑C * r

theorem lipschitzWith_iff_norm_div_le {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] {f : E → F} {C : NNReal} : LipschitzWith C f ↔ ∀ (x y : E), ‖f x / f y‖ ≤ ↑C * ‖x / y‖

theorem lipschitzWith_iff_norm_sub_le {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : E → F} {C : NNReal} : LipschitzWith C f ↔ ∀ (x y : E), ‖f x - f y‖ ≤ ↑C * ‖x - y‖

theorem LipschitzWith.norm_div_le {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] {f : E → F} {C : NNReal} : LipschitzWith C f → ∀ (x y : E), ‖f x / f y‖ ≤ ↑C * ‖x / y‖

Alias of the forward direction of lipschitzWith_iff_norm_div_le.

theorem LipschitzWith.norm_sub_le {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : E → F} {C : NNReal} : LipschitzWith C f → ∀ (x y : E), ‖f x - f y‖ ≤ ↑C * ‖x - y‖

theorem LipschitzWith.norm_div_le_of_le {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] {a b : E} {r : ℝ} {f : E → F} {C : NNReal} (h : LipschitzWith C f) (hr : ‖a / b‖ ≤ r) : ‖f a / f b‖ ≤ ↑C * r

theorem LipschitzWith.norm_sub_le_of_le {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] {a b : E} {r : ℝ} {f : E → F} {C : NNReal} (h : LipschitzWith C f) (hr : ‖a - b‖ ≤ r) : ‖f a - f b‖ ≤ ↑C * r

theorem MonoidHomClass.continuous_of_bound {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [MonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ) (h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖) : Continuous ⇑f

A homomorphism f of seminormed groups is continuous, if there exists a constant C such that for all x, one has ‖f x‖ ≤ C * ‖x‖.

theorem AddMonoidHomClass.continuous_of_bound {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ) (h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖) : Continuous ⇑f

A homomorphism f of seminormed groups is continuous, if there exists a constant C such that for all x, one has ‖f x‖ ≤ C * ‖x‖.

theorem MonoidHomClass.uniformContinuous_of_bound {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [MonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ) (h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖) : UniformContinuous ⇑f

theorem AddMonoidHomClass.uniformContinuous_of_bound {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ) (h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖) : UniformContinuous ⇑f

theorem MonoidHomClass.isometry_iff_norm {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [MonoidHomClass 𝓕 E F] (f : 𝓕) : Isometry ⇑f ↔ ∀ (x : E), ‖f x‖ = ‖x‖

theorem AddMonoidHomClass.isometry_iff_norm {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) : Isometry ⇑f ↔ ∀ (x : E), ‖f x‖ = ‖x‖

theorem MonoidHomClass.isometry_of_norm {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [MonoidHomClass 𝓕 E F] (f : 𝓕) : (∀ (x : E), ‖f x‖ = ‖x‖) → Isometry ⇑f

Alias of the reverse direction of MonoidHomClass.isometry_iff_norm.

theorem AddMonoidHomClass.isometry_of_norm {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) : (∀ (x : E), ‖f x‖ = ‖x‖) → Isometry ⇑f

theorem MonoidHomClass.lipschitz_of_bound_nnnorm {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [MonoidHomClass 𝓕 E F] (f : 𝓕) (C : NNReal) (h : ∀ (x : E), ‖f x‖₊ ≤ C * ‖x‖₊) : LipschitzWith C ⇑f

theorem AddMonoidHomClass.lipschitz_of_bound_nnnorm {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) (C : NNReal) (h : ∀ (x : E), ‖f x‖₊ ≤ C * ‖x‖₊) : LipschitzWith C ⇑f

theorem MonoidHomClass.antilipschitz_of_bound {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [MonoidHomClass 𝓕 E F] (f : 𝓕) {K : NNReal} (h : ∀ (x : E), ‖x‖ ≤ ↑K * ‖f x‖) : AntilipschitzWith K ⇑f

theorem AddMonoidHomClass.antilipschitz_of_bound {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) {K : NNReal} (h : ∀ (x : E), ‖x‖ ≤ ↑K * ‖f x‖) : AntilipschitzWith K ⇑f

theorem LipschitzWith.norm_le_mul' {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] {f : E → F} {K : NNReal} (h : LipschitzWith K f) (hf : f 1 = 1) (x : E) : ‖f x‖ ≤ ↑K * ‖x‖

theorem LipschitzWith.norm_le_mul {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : E → F} {K : NNReal} (h : LipschitzWith K f) (hf : f 0 = 0) (x : E) : ‖f x‖ ≤ ↑K * ‖x‖

theorem LipschitzWith.nnorm_le_mul' {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] {f : E → F} {K : NNReal} (h : LipschitzWith K f) (hf : f 1 = 1) (x : E) : ‖f x‖₊ ≤ K * ‖x‖₊

theorem LipschitzWith.nnorm_le_mul {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : E → F} {K : NNReal} (h : LipschitzWith K f) (hf : f 0 = 0) (x : E) : ‖f x‖₊ ≤ K * ‖x‖₊

theorem AntilipschitzWith.le_mul_norm' {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] {f : E → F} {K : NNReal} (h : AntilipschitzWith K f) (hf : f 1 = 1) (x : E) : ‖x‖ ≤ ↑K * ‖f x‖

theorem AntilipschitzWith.le_mul_norm {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : E → F} {K : NNReal} (h : AntilipschitzWith K f) (hf : f 0 = 0) (x : E) : ‖x‖ ≤ ↑K * ‖f x‖

theorem antilipschitzWith_iff_exists_mul_le_norm' {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [MonoidHomClass 𝓕 E F] {f : 𝓕} : (∃ (K : NNReal), AntilipschitzWith K ⇑f) ↔ ∃ c > 0, ∀ (x : E), c * ‖x‖ ≤ ‖f x‖

theorem antilipschitzWith_iff_exists_mul_le_norm {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] {f : 𝓕} : (∃ (K : NNReal), AntilipschitzWith K ⇑f) ↔ ∃ c > 0, ∀ (x : E), c * ‖x‖ ≤ ‖f x‖

theorem AntilipschitzWith.le_mul_nnnorm' {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] {f : E → F} {K : NNReal} (h : AntilipschitzWith K f) (hf : f 1 = 1) (x : E) : ‖x‖₊ ≤ K * ‖f x‖₊

theorem AntilipschitzWith.le_mul_nnnorm {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : E → F} {K : NNReal} (h : AntilipschitzWith K f) (hf : f 0 = 0) (x : E) : ‖x‖₊ ≤ K * ‖f x‖₊

theorem OneHomClass.bound_of_antilipschitz {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [OneHomClass 𝓕 E F] (f : 𝓕) {K : NNReal} (h : AntilipschitzWith K ⇑f) (x : E) : ‖x‖ ≤ ↑K * ‖f x‖

theorem ZeroHomClass.bound_of_antilipschitz {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [ZeroHomClass 𝓕 E F] (f : 𝓕) {K : NNReal} (h : AntilipschitzWith K ⇑f) (x : E) : ‖x‖ ≤ ↑K * ‖f x‖

theorem Isometry.nnnorm_map_of_map_one {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] {f : E → F} (hi : Isometry f) (h₁ : f 1 = 1) (x : E) : ‖f x‖₊ = ‖x‖₊

theorem Isometry.nnnorm_map_of_map_zero {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : E → F} (hi : Isometry f) (h₁ : f 0 = 0) (x : E) : ‖f x‖₊ = ‖x‖₊

theorem lipschitzWith_one_norm' {E : Type u_2} [SeminormedGroup E] : LipschitzWith 1 norm

theorem lipschitzWith_one_norm {E : Type u_2} [SeminormedAddGroup E] : LipschitzWith 1 norm

theorem lipschitzWith_one_nnnorm' {E : Type u_2} [SeminormedGroup E] : LipschitzWith 1 nnnorm

theorem lipschitzWith_one_nnnorm {E : Type u_2} [SeminormedAddGroup E] : LipschitzWith 1 nnnorm

theorem uniformContinuous_norm' {E : Type u_2} [SeminormedGroup E] : UniformContinuous norm

theorem uniformContinuous_norm {E : Type u_2} [SeminormedAddGroup E] : UniformContinuous norm

theorem uniformContinuous_nnnorm' {E : Type u_2} [SeminormedGroup E] : UniformContinuous fun (a : E) => ‖a‖₊

theorem uniformContinuous_nnnorm {E : Type u_2} [SeminormedAddGroup E] : UniformContinuous fun (a : E) => ‖a‖₊

instance NormedGroup.to_isIsometricSMul_left {E : Type u_2} [SeminormedCommGroup E] : IsIsometricSMul E E

instance NormedAddGroup.to_isIsometricVAdd_left {E : Type u_2} [SeminormedAddCommGroup E] : IsIsometricVAdd E E

@[simp]

theorem dist_self_mul_right {E : Type u_2} [SeminormedCommGroup E] (a b : E) : dist a (a * b) = ‖b‖

@[simp]

theorem dist_self_add_right {E : Type u_2} [SeminormedAddCommGroup E] (a b : E) : dist a (a + b) = ‖b‖

@[simp]

theorem dist_self_mul_left {E : Type u_2} [SeminormedCommGroup E] (a b : E) : dist (a * b) a = ‖b‖

@[simp]

theorem dist_self_add_left {E : Type u_2} [SeminormedAddCommGroup E] (a b : E) : dist (a + b) a = ‖b‖

@[simp]

theorem dist_self_div_right {E : Type u_2} [SeminormedCommGroup E] (a b : E) : dist a (a / b) = ‖b‖

@[simp]

theorem dist_self_sub_right {E : Type u_2} [SeminormedAddCommGroup E] (a b : E) : dist a (a - b) = ‖b‖

@[simp]

theorem dist_self_div_left {E : Type u_2} [SeminormedCommGroup E] (a b : E) : dist (a / b) a = ‖b‖

@[simp]

theorem dist_self_sub_left {E : Type u_2} [SeminormedAddCommGroup E] (a b : E) : dist (a - b) a = ‖b‖

theorem dist_mul_mul_le {E : Type u_2} [SeminormedCommGroup E] (a₁ a₂ b₁ b₂ : E) : dist (a₁ * a₂) (b₁ * b₂) ≤ dist a₁ b₁ + dist a₂ b₂

theorem dist_add_add_le {E : Type u_2} [SeminormedAddCommGroup E] (a₁ a₂ b₁ b₂ : E) : dist (a₁ + a₂) (b₁ + b₂) ≤ dist a₁ b₁ + dist a₂ b₂

theorem dist_mul_mul_le_of_le {E : Type u_2} [SeminormedCommGroup E] {a₁ a₂ b₁ b₂ : E} {r₁ r₂ : ℝ} (h₁ : dist a₁ b₁ ≤ r₁) (h₂ : dist a₂ b₂ ≤ r₂) : dist (a₁ * a₂) (b₁ * b₂) ≤ r₁ + r₂

theorem dist_add_add_le_of_le {E : Type u_2} [SeminormedAddCommGroup E] {a₁ a₂ b₁ b₂ : E} {r₁ r₂ : ℝ} (h₁ : dist a₁ b₁ ≤ r₁) (h₂ : dist a₂ b₂ ≤ r₂) : dist (a₁ + a₂) (b₁ + b₂) ≤ r₁ + r₂

theorem dist_div_div_le {E : Type u_2} [SeminormedCommGroup E] (a₁ a₂ b₁ b₂ : E) : dist (a₁ / a₂) (b₁ / b₂) ≤ dist a₁ b₁ + dist a₂ b₂

theorem dist_sub_sub_le {E : Type u_2} [SeminormedAddCommGroup E] (a₁ a₂ b₁ b₂ : E) : dist (a₁ - a₂) (b₁ - b₂) ≤ dist a₁ b₁ + dist a₂ b₂

theorem dist_div_div_le_of_le {E : Type u_2} [SeminormedCommGroup E] {a₁ a₂ b₁ b₂ : E} {r₁ r₂ : ℝ} (h₁ : dist a₁ b₁ ≤ r₁) (h₂ : dist a₂ b₂ ≤ r₂) : dist (a₁ / a₂) (b₁ / b₂) ≤ r₁ + r₂

theorem dist_sub_sub_le_of_le {E : Type u_2} [SeminormedAddCommGroup E] {a₁ a₂ b₁ b₂ : E} {r₁ r₂ : ℝ} (h₁ : dist a₁ b₁ ≤ r₁) (h₂ : dist a₂ b₂ ≤ r₂) : dist (a₁ - a₂) (b₁ - b₂) ≤ r₁ + r₂

theorem abs_dist_sub_le_dist_mul_mul {E : Type u_2} [SeminormedCommGroup E] (a₁ a₂ b₁ b₂ : E) : |dist a₁ b₁ - dist a₂ b₂| ≤ dist (a₁ * a₂) (b₁ * b₂)

theorem abs_dist_sub_le_dist_add_add {E : Type u_2} [SeminormedAddCommGroup E] (a₁ a₂ b₁ b₂ : E) : |dist a₁ b₁ - dist a₂ b₂| ≤ dist (a₁ + a₂) (b₁ + b₂)

theorem nndist_mul_mul_le {E : Type u_2} [SeminormedCommGroup E] (a₁ a₂ b₁ b₂ : E) : nndist (a₁ * a₂) (b₁ * b₂) ≤ nndist a₁ b₁ + nndist a₂ b₂

theorem nndist_add_add_le {E : Type u_2} [SeminormedAddCommGroup E] (a₁ a₂ b₁ b₂ : E) : nndist (a₁ + a₂) (b₁ + b₂) ≤ nndist a₁ b₁ + nndist a₂ b₂

theorem edist_mul_mul_le {E : Type u_2} [SeminormedCommGroup E] (a₁ a₂ b₁ b₂ : E) : edist (a₁ * a₂) (b₁ * b₂) ≤ edist a₁ b₁ + edist a₂ b₂

theorem edist_add_add_le {E : Type u_2} [SeminormedAddCommGroup E] (a₁ a₂ b₁ b₂ : E) : edist (a₁ + a₂) (b₁ + b₂) ≤ edist a₁ b₁ + edist a₂ b₂

@[simp]

theorem lipschitzWith_inv_iff {α : Type u_4} {E : Type u_5} [SeminormedCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} : LipschitzWith K f⁻¹ ↔ LipschitzWith K f

@[simp]

theorem lipschitzWith_neg_iff {α : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} : LipschitzWith K (-f) ↔ LipschitzWith K f

@[simp]

theorem antilipschitzWith_inv_iff {α : Type u_4} {E : Type u_5} [SeminormedCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} : AntilipschitzWith K f⁻¹ ↔ AntilipschitzWith K f

@[simp]

theorem antilipschitzWith_neg_iff {α : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} : AntilipschitzWith K (-f) ↔ AntilipschitzWith K f

@[simp]

theorem lipschitzOnWith_inv_iff {α : Type u_4} {E : Type u_5} [SeminormedCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} {s : Set α} : LipschitzOnWith K f⁻¹ s ↔ LipschitzOnWith K f s

@[simp]

theorem lipschitzOnWith_neg_iff {α : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} {s : Set α} : LipschitzOnWith K (-f) s ↔ LipschitzOnWith K f s

@[simp]

theorem locallyLipschitz_inv_iff {α : Type u_4} {E : Type u_5} [SeminormedCommGroup E] [PseudoEMetricSpace α] {f : α → E} : LocallyLipschitz f⁻¹ ↔ LocallyLipschitz f

@[simp]

theorem locallyLipschitz_neg_iff {α : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {f : α → E} : LocallyLipschitz (-f) ↔ LocallyLipschitz f

@[simp]

theorem locallyLipschitzOn_inv_iff {α : Type u_4} {E : Type u_5} [SeminormedCommGroup E] [PseudoEMetricSpace α] {f : α → E} {s : Set α} : LocallyLipschitzOn s f⁻¹ ↔ LocallyLipschitzOn s f

@[simp]

theorem locallyLipschitzOn_neg_iff {α : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {f : α → E} {s : Set α} : LocallyLipschitzOn s (-f) ↔ LocallyLipschitzOn s f

theorem LipschitzWith.of_inv {α : Type u_4} {E : Type u_5} [SeminormedCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} : LipschitzWith K f⁻¹ → LipschitzWith K f

Alias of the forward direction of lipschitzWith_inv_iff.

theorem LipschitzWith.inv {α : Type u_4} {E : Type u_5} [SeminormedCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} : LipschitzWith K f → LipschitzWith K f⁻¹

Alias of the reverse direction of lipschitzWith_inv_iff.

theorem LipschitzWith.of_neg {α : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} : LipschitzWith K (-f) → LipschitzWith K f

theorem LipschitzWith.neg {α : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} : LipschitzWith K f → LipschitzWith K (-f)

theorem AntilipschitzWith.inv {α : Type u_4} {E : Type u_5} [SeminormedCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} : AntilipschitzWith K f → AntilipschitzWith K f⁻¹

Alias of the reverse direction of antilipschitzWith_inv_iff.

theorem AntilipschitzWith.of_inv {α : Type u_4} {E : Type u_5} [SeminormedCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} : AntilipschitzWith K f⁻¹ → AntilipschitzWith K f

Alias of the forward direction of antilipschitzWith_inv_iff.

theorem AntilipschitzWith.neg {α : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} : AntilipschitzWith K f → AntilipschitzWith K (-f)

theorem AntilipschitzWith.of_neg {α : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} : AntilipschitzWith K (-f) → AntilipschitzWith K f

theorem LipschitzOnWith.of_inv {α : Type u_4} {E : Type u_5} [SeminormedCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} {s : Set α} : LipschitzOnWith K f⁻¹ s → LipschitzOnWith K f s

Alias of the forward direction of lipschitzOnWith_inv_iff.

theorem LipschitzOnWith.inv {α : Type u_4} {E : Type u_5} [SeminormedCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} {s : Set α} : LipschitzOnWith K f s → LipschitzOnWith K f⁻¹ s

Alias of the reverse direction of lipschitzOnWith_inv_iff.

theorem LipschitzOnWith.neg {α : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} {s : Set α} : LipschitzOnWith K f s → LipschitzOnWith K (-f) s

theorem LipschitzOnWith.of_neg {α : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} {s : Set α} : LipschitzOnWith K (-f) s → LipschitzOnWith K f s

theorem LocallyLipschitz.of_inv {α : Type u_4} {E : Type u_5} [SeminormedCommGroup E] [PseudoEMetricSpace α] {f : α → E} : LocallyLipschitz f⁻¹ → LocallyLipschitz f

Alias of the forward direction of locallyLipschitz_inv_iff.

theorem LocallyLipschitz.inv {α : Type u_4} {E : Type u_5} [SeminormedCommGroup E] [PseudoEMetricSpace α] {f : α → E} : LocallyLipschitz f → LocallyLipschitz f⁻¹

Alias of the reverse direction of locallyLipschitz_inv_iff.

theorem LocallyLipschitz.neg {α : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {f : α → E} : LocallyLipschitz f → LocallyLipschitz (-f)

theorem LocallyLipschitz.of_neg {α : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {f : α → E} : LocallyLipschitz (-f) → LocallyLipschitz f

theorem LocallyLipschitzOn.inv {α : Type u_4} {E : Type u_5} [SeminormedCommGroup E] [PseudoEMetricSpace α] {f : α → E} {s : Set α} : LocallyLipschitzOn s f → LocallyLipschitzOn s f⁻¹

Alias of the reverse direction of locallyLipschitzOn_inv_iff.

theorem LocallyLipschitzOn.of_inv {α : Type u_4} {E : Type u_5} [SeminormedCommGroup E] [PseudoEMetricSpace α] {f : α → E} {s : Set α} : LocallyLipschitzOn s f⁻¹ → LocallyLipschitzOn s f

Alias of the forward direction of locallyLipschitzOn_inv_iff.

theorem LocallyLipschitzOn.of_neg {α : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {f : α → E} {s : Set α} : LocallyLipschitzOn s (-f) → LocallyLipschitzOn s f

theorem LocallyLipschitzOn.neg {α : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {f : α → E} {s : Set α} : LocallyLipschitzOn s f → LocallyLipschitzOn s (-f)

theorem LipschitzOnWith.mul {α : Type u_4} {E : Type u_5} [SeminormedCommGroup E] [PseudoEMetricSpace α] {Kf Kg : NNReal} {f g : α → E} {s : Set α} (hf : LipschitzOnWith Kf f s) (hg : LipschitzOnWith Kg g s) : LipschitzOnWith (Kf + Kg) (fun (x : α) => f x * g x) s

theorem LipschitzOnWith.add {α : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {Kf Kg : NNReal} {f g : α → E} {s : Set α} (hf : LipschitzOnWith Kf f s) (hg : LipschitzOnWith Kg g s) : LipschitzOnWith (Kf + Kg) (fun (x : α) => f x + g x) s

theorem LipschitzWith.mul {α : Type u_4} {E : Type u_5} [SeminormedCommGroup E] [PseudoEMetricSpace α] {Kf Kg : NNReal} {f g : α → E} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) : LipschitzWith (Kf + Kg) fun (x : α) => f x * g x

theorem LipschitzWith.add {α : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {Kf Kg : NNReal} {f g : α → E} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) : LipschitzWith (Kf + Kg) fun (x : α) => f x + g x

theorem LocallyLipschitzOn.mul {α : Type u_4} {E : Type u_5} [SeminormedCommGroup E] [PseudoEMetricSpace α] {f g : α → E} {s : Set α} (hf : LocallyLipschitzOn s f) (hg : LocallyLipschitzOn s g) : LocallyLipschitzOn s fun (x : α) => f x * g x

theorem LocallyLipschitzOn.add {α : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {f g : α → E} {s : Set α} (hf : LocallyLipschitzOn s f) (hg : LocallyLipschitzOn s g) : LocallyLipschitzOn s fun (x : α) => f x + g x

theorem LocallyLipschitz.mul {α : Type u_4} {E : Type u_5} [SeminormedCommGroup E] [PseudoEMetricSpace α] {f g : α → E} (hf : LocallyLipschitz f) (hg : LocallyLipschitz g) : LocallyLipschitz fun (x : α) => f x * g x

theorem LocallyLipschitz.add {α : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {f g : α → E} (hf : LocallyLipschitz f) (hg : LocallyLipschitz g) : LocallyLipschitz fun (x : α) => f x + g x

theorem LipschitzOnWith.div {α : Type u_4} {E : Type u_5} [SeminormedCommGroup E] [PseudoEMetricSpace α] {Kf Kg : NNReal} {f g : α → E} {s : Set α} (hf : LipschitzOnWith Kf f s) (hg : LipschitzOnWith Kg g s) : LipschitzOnWith (Kf + Kg) (fun (x : α) => f x / g x) s

theorem LipschitzOnWith.sub {α : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {Kf Kg : NNReal} {f g : α → E} {s : Set α} (hf : LipschitzOnWith Kf f s) (hg : LipschitzOnWith Kg g s) : LipschitzOnWith (Kf + Kg) (fun (x : α) => f x - g x) s

theorem LipschitzWith.div {α : Type u_4} {E : Type u_5} [SeminormedCommGroup E] [PseudoEMetricSpace α] {Kf Kg : NNReal} {f g : α → E} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) : LipschitzWith (Kf + Kg) fun (x : α) => f x / g x

theorem LipschitzWith.sub {α : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {Kf Kg : NNReal} {f g : α → E} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) : LipschitzWith (Kf + Kg) fun (x : α) => f x - g x

theorem LocallyLipschitzOn.div {α : Type u_4} {E : Type u_5} [SeminormedCommGroup E] [PseudoEMetricSpace α] {f g : α → E} {s : Set α} (hf : LocallyLipschitzOn s f) (hg : LocallyLipschitzOn s g) : LocallyLipschitzOn s fun (x : α) => f x / g x

theorem LocallyLipschitzOn.sub {α : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {f g : α → E} {s : Set α} (hf : LocallyLipschitzOn s f) (hg : LocallyLipschitzOn s g) : LocallyLipschitzOn s fun (x : α) => f x - g x

theorem LocallyLipschitz.div {α : Type u_4} {E : Type u_5} [SeminormedCommGroup E] [PseudoEMetricSpace α] {f g : α → E} (hf : LocallyLipschitz f) (hg : LocallyLipschitz g) : LocallyLipschitz fun (x : α) => f x / g x

theorem LocallyLipschitz.sub {α : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {f g : α → E} (hf : LocallyLipschitz f) (hg : LocallyLipschitz g) : LocallyLipschitz fun (x : α) => f x - g x

theorem AntilipschitzWith.mul_lipschitzWith {α : Type u_4} {E : Type u_5} [SeminormedCommGroup E] [PseudoEMetricSpace α] {Kf Kg : NNReal} {f g : α → E} (hf : AntilipschitzWith Kf f) (hg : LipschitzWith Kg g) (hK : Kg < Kf⁻¹) : AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ fun (x : α) => f x * g x

theorem AntilipschitzWith.add_lipschitzWith {α : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {Kf Kg : NNReal} {f g : α → E} (hf : AntilipschitzWith Kf f) (hg : LipschitzWith Kg g) (hK : Kg < Kf⁻¹) : AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ fun (x : α) => f x + g x

theorem AntilipschitzWith.mul_div_lipschitzWith {α : Type u_4} {E : Type u_5} [SeminormedCommGroup E] [PseudoEMetricSpace α] {Kf Kg : NNReal} {f g : α → E} (hf : AntilipschitzWith Kf f) (hg : LipschitzWith Kg (g / f)) (hK : Kg < Kf⁻¹) : AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ g

theorem AntilipschitzWith.add_sub_lipschitzWith {α : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {Kf Kg : NNReal} {f g : α → E} (hf : AntilipschitzWith Kf f) (hg : LipschitzWith Kg (g - f)) (hK : Kg < Kf⁻¹) : AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ g

theorem AntilipschitzWith.le_mul_norm_div {F : Type u_3} [SeminormedCommGroup F] {E : Type u_5} [SeminormedCommGroup E] {K : NNReal} {f : E → F} (hf : AntilipschitzWith K f) (x y : E) : ‖x / y‖ ≤ ↑K * ‖f x / f y‖

theorem AntilipschitzWith.le_mul_norm_sub {F : Type u_3} [SeminormedAddCommGroup F] {E : Type u_5} [SeminormedAddCommGroup E] {K : NNReal} {f : E → F} (hf : AntilipschitzWith K f) (x y : E) : ‖x - y‖ ≤ ↑K * ‖f x - f y‖

@[instance 100]

instance SeminormedCommGroup.to_lipschitzMul {E : Type u_2} [SeminormedCommGroup E] : LipschitzMul E

@[instance 100]

instance SeminormedAddCommGroup.to_lipschitzAdd {E : Type u_2} [SeminormedAddCommGroup E] : LipschitzAdd E

@[instance 100]

instance SeminormedCommGroup.to_isUniformGroup {E : Type u_2} [SeminormedCommGroup E] : IsUniformGroup E

A seminormed group is a uniform group, i.e., multiplication and division are uniformly continuous.

@[instance 100]

instance SeminormedAddCommGroup.to_isUniformAddGroup {E : Type u_2} [SeminormedAddCommGroup E] : IsUniformAddGroup E

A seminormed group is a uniform additive group, i.e., addition and subtraction are uniformly continuous.

@[instance 100]

instance SeminormedCommGroup.toIsTopologicalGroup {E : Type u_2} [SeminormedCommGroup E] : IsTopologicalGroup E

@[instance 100]

instance SeminormedAddCommGroup.toIsTopologicalAddGroup {E : Type u_2} [SeminormedAddCommGroup E] : IsTopologicalAddGroup E

SeparationQuotient

instance SeparationQuotient.instMulNorm {E : Type u_2} [SeminormedCommGroup E] : Norm (SeparationQuotient E)

instance SeparationQuotient.instNorm {E : Type u_2} [SeminormedAddCommGroup E] : Norm (SeparationQuotient E)

@[simp]

theorem SeparationQuotient.norm_mk' {E : Type u_2} [SeminormedCommGroup E] (p : E) : ‖mk p‖ = ‖p‖

@[simp]

theorem SeparationQuotient.norm_mk {E : Type u_2} [SeminormedAddCommGroup E] (p : E) : ‖mk p‖ = ‖p‖

instance SeparationQuotient.instNormedCommGroup {E : Type u_2} [SeminormedCommGroup E] : NormedCommGroup (SeparationQuotient E)

instance SeparationQuotient.instNormedAddCommGroup {E : Type u_2} [SeminormedAddCommGroup E] : NormedAddCommGroup (SeparationQuotient E)

theorem SeparationQuotient.mk_eq_one_iff {E : Type u_2} [SeminormedCommGroup E] {p : E} : mk p = 1 ↔ ‖p‖ = 0

theorem SeparationQuotient.mk_eq_zero_iff {E : Type u_2} [SeminormedAddCommGroup E] {p : E} : mk p = 0 ↔ ‖p‖ = 0

@[simp]

theorem SeparationQuotient.nnnorm_mk' {E : Type u_2} [SeminormedCommGroup E] (p : E) : ‖mk p‖₊ = ‖p‖₊

@[simp]

theorem SeparationQuotient.nnnorm_mk {E : Type u_2} [SeminormedAddCommGroup E] (p : E) : ‖mk p‖₊ = ‖p‖₊

theorem cauchySeq_prod_of_eventually_eq {E : Type u_2} [SeminormedCommGroup E] {u v : ℕ → E} {N : ℕ} (huv : ∀ n ≥ N, u n = v n) (hv : CauchySeq fun (n : ℕ) => ∏ k ∈ Finset.range (n + 1), v k) : CauchySeq fun (n : ℕ) => ∏ k ∈ Finset.range (n + 1), u k

theorem cauchySeq_sum_of_eventually_eq {E : Type u_2} [SeminormedAddCommGroup E] {u v : ℕ → E} {N : ℕ} (huv : ∀ n ≥ N, u n = v n) (hv : CauchySeq fun (n : ℕ) => ∑ k ∈ Finset.range (n + 1), v k) : CauchySeq fun (n : ℕ) => ∑ k ∈ Finset.range (n + 1), u k

theorem CauchySeq.mul_norm_bddAbove {G : Type u_4} [SeminormedGroup G] {u : ℕ → G} (hu : CauchySeq u) : BddAbove (Set.range fun (n : ℕ) => ‖u n‖)

theorem CauchySeq.norm_bddAbove {G : Type u_4} [SeminormedAddGroup G] {u : ℕ → G} (hu : CauchySeq u) : BddAbove (Set.range fun (n : ℕ) => ‖u n‖)