doc-next-gen

Mathlib.Analysis.Normed.Group.Uniform

Module docstring

{"# Normed groups are uniform groups

This file proves lipschitzness of normed group operations and shows that normed groups are uniform groups. ","### SeparationQuotient "}

NormedGroup.to_isIsometricSMul_right instance
: IsIsometricSMul Eᵐᵒᵖ E
Full source 
@[to_additive]
instance NormedGroup.to_isIsometricSMul_right : IsIsometricSMul Eᵐᵒᵖ E :=
  ⟨fun a => Isometry.of_dist_eq fun b c => by simp [dist_eq_norm_div]⟩
Isometric Right Action by the Multiplicative Opposite in Normed Groups
Informal description
For any normed group $E$, the multiplicative opposite $E^\text{op}$ acts isometrically on $E$ by right multiplication. That is, for any $a \in E^\text{op}$, the map $x \mapsto x \cdot a$ is an isometry from $E$ to itself.
Isometry.norm_map_of_map_one theorem
{f : E → F} (hi : Isometry f) (h₁ : f 1 = 1) (x : E) : ‖f x‖ = ‖x‖
Full source 
@[to_additive]
theorem Isometry.norm_map_of_map_one {f : E → F} (hi : Isometry f) (h₁ : f 1 = 1) (x : E) :
    ‖f x‖ = ‖x‖ := by rw [← dist_one_right, ← h₁, hi.dist_eq, dist_one_right]
Isometry Preserves Norm When Fixing Identity
Informal description
Let $E$ and $F$ be seminormed groups, and let $f : E \to F$ be an isometry such that $f(1) = 1$. Then for any $x \in E$, the norm of $f(x)$ equals the norm of $x$, i.e., $\|f(x)\| = \|x\|$.
dist_mul_self_right theorem
(a b : E) : dist b (a * b) = ‖a‖
Full source 
@[to_additive (attr := simp)]
theorem dist_mul_self_right (a b : E) : dist b (a * b) = ‖a‖ := by
  rw [← dist_one_left, ← dist_mul_right 1 a b, one_mul]
Distance Identity: $\text{dist}(b, a \cdot b) = \|a\|$ in Seminormed Groups
Informal description
For any elements $a$ and $b$ in a seminormed group $E$, the distance between $b$ and $a * b$ is equal to the norm of $a$, i.e., $\text{dist}(b, a \cdot b) = \|a\|$.
dist_mul_self_left theorem
(a b : E) : dist (a * b) b = ‖a‖
Full source 
@[to_additive (attr := simp)]
theorem dist_mul_self_left (a b : E) : dist (a * b) b = ‖a‖ := by
  rw [dist_comm, dist_mul_self_right]
Distance Identity: $\text{dist}(a \cdot b, b) = \|a\|$ in Seminormed Groups
Informal description
For any elements $a$ and $b$ in a seminormed group $E$, the distance between $a \cdot b$ and $b$ is equal to the norm of $a$, i.e., $\text{dist}(a \cdot b, b) = \|a\|$.
dist_div_eq_dist_mul_left theorem
(a b c : E) : dist (a / b) c = dist a (c * b)
Full source 
@[to_additive (attr := simp)]
theorem dist_div_eq_dist_mul_left (a b c : E) : dist (a / b) c = dist a (c * b) := by
  rw [← dist_mul_right _ _ b, div_mul_cancel]
Distance Identity: $\text{dist}(a / b, c) = \text{dist}(a, c * b)$ in Seminormed Groups
Informal description
For any elements $a, b, c$ in a seminormed group $E$, the distance between $a / b$ and $c$ is equal to the distance between $a$ and $c * b$, i.e., $\text{dist}(a / b, c) = \text{dist}(a, c * b)$.
dist_div_eq_dist_mul_right theorem
(a b c : E) : dist a (b / c) = dist (a * c) b
Full source 
@[to_additive (attr := simp)]
theorem dist_div_eq_dist_mul_right (a b c : E) : dist a (b / c) = dist (a * c) b := by
  rw [← dist_mul_right _ _ c, div_mul_cancel]
Distance Identity: $d(a, b/c) = d(a \cdot c, b)$ in Seminormed Groups
Informal description
For any elements $a, b, c$ in a seminormed group $E$, the distance between $a$ and $b/c$ equals the distance between $a \cdot c$ and $b$, i.e., \[ d(a, b/c) = d(a \cdot c, b). \]
MonoidHomClass.lipschitz_of_bound theorem
[MonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ) (h : ∀ x, ‖f x‖ ≤ C * ‖x‖) : LipschitzWith (Real.toNNReal C) f
Full source 
/-- 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/NormedSpace/OperatorNorm.lean`. -/
@[to_additive "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/NormedSpace/OperatorNorm.lean`."]
theorem MonoidHomClass.lipschitz_of_bound [MonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ)
    (h : ∀ x, ‖f x‖ ≤ C * ‖x‖) : LipschitzWith (Real.toNNReal C) f :=
  LipschitzWith.of_dist_le' fun x y => by simpa only [dist_eq_norm_div, map_div] using h (x / y)
Lipschitz Continuity of Monoid Homomorphisms with Norm Bounds
Informal description
Let $E$ and $F$ be seminormed groups and let $f \colon E \to F$ be a monoid homomorphism. If there exists a constant $C \in \mathbb{R}$ such that for all $x \in E$, $\|f(x)\| \leq C \cdot \|x\|$, then $f$ is Lipschitz continuous with constant $\text{Real.toNNReal}(C)$.
lipschitzOnWith_iff_norm_div_le theorem
{f : E → F} {C : ℝ≥0} : LipschitzOnWith C f s ↔ ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → ‖f x / f y‖ ≤ C * ‖x / y‖
Full source 
@[to_additive]
theorem lipschitzOnWith_iff_norm_div_le {f : E → F} {C : ℝ≥0} :
    LipschitzOnWithLipschitzOnWith C f s ↔ ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → ‖f x / f y‖ ≤ C * ‖x / y‖ := by
  simp only [lipschitzOnWith_iff_dist_le_mul, dist_eq_norm_div]
Lipschitz Condition on Seminormed Groups via Quotient Norms
Informal description
For a function $f : E \to F$ between seminormed groups and a non-negative real number $C$, the function $f$ is Lipschitz continuous on a set $s \subseteq E$ with constant $C$ if and only if for all $x, y \in s$, the norm of the quotient $\|f(x) / f(y)\|$ is bounded by $C$ times the norm of the quotient $\|x / y\|$, i.e., $\|f(x) / f(y)\| \leq C \cdot \|x / y\|$.
LipschitzOnWith.norm_div_le_of_le theorem
{f : E → F} {C : ℝ≥0} (h : LipschitzOnWith C f s) (ha : a ∈ s) (hb : b ∈ s) (hr : ‖a / b‖ ≤ r) : ‖f a / f b‖ ≤ C * r
Full source 
@[to_additive]
theorem LipschitzOnWith.norm_div_le_of_le {f : E → F} {C : ℝ≥0} (h : LipschitzOnWith C f s)
    (ha : a ∈ s) (hb : b ∈ s) (hr : ‖a / b‖ ≤ r) : ‖f a / f b‖ ≤ C * r :=
  (h.norm_div_le ha hb).trans <| by gcongr
Norm Bound for Lipschitz Functions on Seminormed Groups
Informal description
Let $E$ and $F$ be seminormed groups, $f : E \to F$ a function, $C \geq 0$ a real number, and $s \subseteq E$ a subset. If $f$ is Lipschitz continuous on $s$ with constant $C$, then for any $a, b \in s$ with $\|a / b\| \leq r$, we have $\|f(a) / f(b)\| \leq C \cdot r$.
lipschitzWith_iff_norm_div_le theorem
{f : E → F} {C : ℝ≥0} : LipschitzWith C f ↔ ∀ x y, ‖f x / f y‖ ≤ C * ‖x / y‖
Full source 
@[to_additive]
theorem lipschitzWith_iff_norm_div_le {f : E → F} {C : ℝ≥0} :
    LipschitzWithLipschitzWith C f ↔ ∀ x y, ‖f x / f y‖ ≤ C * ‖x / y‖ := by
  simp only [lipschitzWith_iff_dist_le_mul, dist_eq_norm_div]
Lipschitz Condition via Norm of Quotients in Seminormed Groups
Informal description
For a function $f \colon E \to F$ between seminormed groups and a non-negative real constant $C$, the function $f$ is Lipschitz with constant $C$ if and only if for all $x, y \in E$, the norm of the quotient $\|f(x) / f(y)\|$ is bounded by $C$ times the norm of the quotient $\|x / y\|$, i.e., $\|f(x) / f(y)\| \leq C \|x / y\|$.
LipschitzWith.norm_div_le_of_le theorem
{f : E → F} {C : ℝ≥0} (h : LipschitzWith C f) (hr : ‖a / b‖ ≤ r) : ‖f a / f b‖ ≤ C * r
Full source 
@[to_additive]
theorem LipschitzWith.norm_div_le_of_le {f : E → F} {C : ℝ≥0} (h : LipschitzWith C f)
    (hr : ‖a / b‖ ≤ r) : ‖f a / f b‖ ≤ C * r :=
  (h.norm_div_le _ _).trans <| by gcongr
Lipschitz Condition Implies Norm Bound on Quotients in Seminormed Groups
Informal description
Let $E$ and $F$ be seminormed groups, and let $f \colon E \to F$ be a Lipschitz function with constant $C \geq 0$. For any elements $a, b \in E$ such that $\|a / b\| \leq r$, we have $\|f(a) / f(b)\| \leq C \cdot r$.
MonoidHomClass.continuous_of_bound theorem
[MonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ) (h : ∀ x, ‖f x‖ ≤ C * ‖x‖) : Continuous f
Full source 
/-- 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‖`. -/
@[to_additive "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.continuous_of_bound [MonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ)
    (h : ∀ x, ‖f x‖ ≤ C * ‖x‖) : Continuous f :=
  (MonoidHomClass.lipschitz_of_bound f C h).continuous
Continuity of Monoid Homomorphisms with Norm Bounds
Informal description
Let $E$ and $F$ be seminormed groups and let $f \colon E \to F$ be a monoid homomorphism. If there exists a constant $C \in \mathbb{R}$ such that for all $x \in E$, $\|f(x)\| \leq C \|x\|$, then $f$ is continuous.
MonoidHomClass.uniformContinuous_of_bound theorem
[MonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ) (h : ∀ x, ‖f x‖ ≤ C * ‖x‖) : UniformContinuous f
Full source 
@[to_additive]
theorem MonoidHomClass.uniformContinuous_of_bound [MonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ)
    (h : ∀ x, ‖f x‖ ≤ C * ‖x‖) : UniformContinuous f :=
  (MonoidHomClass.lipschitz_of_bound f C h).uniformContinuous
Uniform Continuity of Monoid Homomorphisms with Norm Bounds
Informal description
Let $E$ and $F$ be seminormed groups, and let $f \colon E \to F$ be a monoid homomorphism. If there exists a constant $C \in \mathbb{R}$ such that for all $x \in E$, $\|f(x)\| \leq C \cdot \|x\|$, then $f$ is uniformly continuous.
MonoidHomClass.isometry_iff_norm theorem
[MonoidHomClass 𝓕 E F] (f : 𝓕) : Isometry f ↔ ∀ x, ‖f x‖ = ‖x‖
Full source 
@[to_additive]
theorem MonoidHomClass.isometry_iff_norm [MonoidHomClass 𝓕 E F] (f : 𝓕) :
    IsometryIsometry f ↔ ∀ x, ‖f x‖ = ‖x‖ := by
  simp only [isometry_iff_dist_eq, dist_eq_norm_div, ← map_div]
  refine ⟨fun h x => ?_, fun h x y => h _⟩
  simpa using h x 1
Isometry Criterion for Monoid Homomorphisms: $\|f(x)\| = \|x\|$
Informal description
Let $E$ and $F$ be seminormed groups, and let $\mathcal{F}$ be a type of homomorphisms from $E$ to $F$ that preserve the monoid structure. For any homomorphism $f \in \mathcal{F}$, $f$ is an isometry if and only if for every element $x \in E$, the norm of $f(x)$ equals the norm of $x$, i.e., $\|f(x)\| = \|x\|$.
MonoidHomClass.lipschitz_of_bound_nnnorm theorem
[MonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ≥0) (h : ∀ x, ‖f x‖₊ ≤ C * ‖x‖₊) : LipschitzWith C f
Full source 
@[to_additive]
theorem MonoidHomClass.lipschitz_of_bound_nnnorm [MonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ≥0)
    (h : ∀ x, ‖f x‖₊ ≤ C * ‖x‖₊) : LipschitzWith C f :=
  @Real.toNNReal_coe C ▸ MonoidHomClass.lipschitz_of_bound f C h
Lipschitz Continuity of Monoid Homomorphisms via Non-Negative Norm Bounds
Informal description
Let $E$ and $F$ be seminormed groups, and let $\mathcal{F}$ be a type of monoid homomorphisms from $E$ to $F$. For any monoid homomorphism $f \in \mathcal{F}$ and any nonnegative real number $C$, if for all $x \in E$ the non-negative norm of $f(x)$ satisfies $\|f(x)\|_+ \leq C \cdot \|x\|_+$, then $f$ is Lipschitz continuous with constant $C$.
MonoidHomClass.antilipschitz_of_bound theorem
[MonoidHomClass 𝓕 E F] (f : 𝓕) {K : ℝ≥0} (h : ∀ x, ‖x‖ ≤ K * ‖f x‖) : AntilipschitzWith K f
Full source 
@[to_additive]
theorem MonoidHomClass.antilipschitz_of_bound [MonoidHomClass 𝓕 E F] (f : 𝓕) {K : ℝ≥0}
    (h : ∀ x, ‖x‖ ≤ K * ‖f x‖) : AntilipschitzWith K f :=
  AntilipschitzWith.of_le_mul_dist fun x y => by
    simpa only [dist_eq_norm_div, map_div] using h (x / y)
Antilipschitz Property of Monoid Homomorphisms via Norm Bounds
Informal description
Let $E$ and $F$ be seminormed groups, and let $\mathcal{F}$ be a type of monoid homomorphisms from $E$ to $F$. For any monoid homomorphism $f \in \mathcal{F}$ and any nonnegative real number $K$, if for all $x \in E$ the norm of $x$ satisfies $\|x\| \leq K \cdot \|f(x)\|$, then $f$ is antilipschitz with constant $K$.
LipschitzWith.norm_le_mul' theorem
{f : E → F} {K : ℝ≥0} (h : LipschitzWith K f) (hf : f 1 = 1) (x) : ‖f x‖ ≤ K * ‖x‖
Full source 
@[to_additive LipschitzWith.norm_le_mul]
theorem LipschitzWith.norm_le_mul' {f : E → F} {K : ℝ≥0} (h : LipschitzWith K f) (hf : f 1 = 1)
    (x) : ‖f x‖ ≤ K * ‖x‖ := by simpa only [dist_one_right, hf] using h.dist_le_mul x 1
Norm Bound under Lipschitz Maps Preserving Identity
Informal description
For any function $f \colon E \to F$ between seminormed groups that is Lipschitz with constant $K \geq 0$ and satisfies $f(1) = 1$, the norm of $f(x)$ is bounded by $K$ times the norm of $x$, i.e., $\|f(x)\| \leq K \|x\|$ for all $x \in E$.
LipschitzWith.nnorm_le_mul' theorem
{f : E → F} {K : ℝ≥0} (h : LipschitzWith K f) (hf : f 1 = 1) (x) : ‖f x‖₊ ≤ K * ‖x‖₊
Full source 
@[to_additive LipschitzWith.nnorm_le_mul]
theorem LipschitzWith.nnorm_le_mul' {f : E → F} {K : ℝ≥0} (h : LipschitzWith K f) (hf : f 1 = 1)
    (x) : ‖f x‖₊ ≤ K * ‖x‖₊ :=
  h.norm_le_mul' hf x
Non-negative Norm Bound under Lipschitz Maps Preserving Identity
Informal description
For any function $f \colon E \to F$ between seminormed groups that is Lipschitz with constant $K \geq 0$ and satisfies $f(1) = 1$, the non-negative norm of $f(x)$ is bounded by $K$ times the non-negative norm of $x$, i.e., $\|f(x)\|₊ \leq K \|x\|₊$ for all $x \in E$.
AntilipschitzWith.le_mul_norm' theorem
{f : E → F} {K : ℝ≥0} (h : AntilipschitzWith K f) (hf : f 1 = 1) (x) : ‖x‖ ≤ K * ‖f x‖
Full source 
@[to_additive AntilipschitzWith.le_mul_norm]
theorem AntilipschitzWith.le_mul_norm' {f : E → F} {K : ℝ≥0} (h : AntilipschitzWith K f)
    (hf : f 1 = 1) (x) : ‖x‖ ≤ K * ‖f x‖ := by
  simpa only [dist_one_right, hf] using h.le_mul_dist x 1
Norm Bound under Antilipschitz Maps Preserving Identity
Informal description
For any function $f \colon E \to F$ between seminormed groups that is antilipschitz with constant $K \geq 0$ and satisfies $f(1) = 1$, the norm of any element $x \in E$ is bounded by $K$ times the norm of its image under $f$, i.e., $\|x\| \leq K \|f(x)\|$.
AntilipschitzWith.le_mul_nnnorm' theorem
{f : E → F} {K : ℝ≥0} (h : AntilipschitzWith K f) (hf : f 1 = 1) (x) : ‖x‖₊ ≤ K * ‖f x‖₊
Full source 
@[to_additive AntilipschitzWith.le_mul_nnnorm]
theorem AntilipschitzWith.le_mul_nnnorm' {f : E → F} {K : ℝ≥0} (h : AntilipschitzWith K f)
    (hf : f 1 = 1) (x) : ‖x‖₊ ≤ K * ‖f x‖₊ :=
  h.le_mul_norm' hf x
Non-negative Norm Bound under Antilipschitz Maps Preserving Identity
Informal description
For any function $f \colon E \to F$ between seminormed groups that is antilipschitz with constant $K \geq 0$ and satisfies $f(1) = 1$, the non-negative norm of any element $x \in E$ is bounded by $K$ times the non-negative norm of its image under $f$, i.e., $\|x\|₊ \leq K \|f(x)\|₊$.
OneHomClass.bound_of_antilipschitz theorem
[OneHomClass 𝓕 E F] (f : 𝓕) {K : ℝ≥0} (h : AntilipschitzWith K f) (x) : ‖x‖ ≤ K * ‖f x‖
Full source 
@[to_additive]
theorem OneHomClass.bound_of_antilipschitz [OneHomClass 𝓕 E F] (f : 𝓕) {K : ℝ≥0}
    (h : AntilipschitzWith K f) (x) : ‖x‖ ≤ K * ‖f x‖ :=
  h.le_mul_nnnorm' (map_one f) x
Norm Bound for Identity-Preserving Antilipschitz Homomorphisms
Informal description
Let $E$ and $F$ be seminormed groups, and let $\mathcal{F}$ be a type of homomorphisms from $E$ to $F$ that preserve the identity element (i.e., $f(1) = 1$ for any $f \in \mathcal{F}$). Given a homomorphism $f \in \mathcal{F}$ that is antilipschitz with constant $K \geq 0$, the norm of any element $x \in E$ is bounded by $K$ times the norm of its image under $f$, i.e., $\|x\| \leq K \|f(x)\|$.
Isometry.nnnorm_map_of_map_one theorem
{f : E → F} (hi : Isometry f) (h₁ : f 1 = 1) (x : E) : ‖f x‖₊ = ‖x‖₊
Full source 
@[to_additive]
theorem Isometry.nnnorm_map_of_map_one {f : E → F} (hi : Isometry f) (h₁ : f 1 = 1) (x : E) :
    ‖f x‖₊ = ‖x‖₊ :=
  Subtype.ext <| hi.norm_map_of_map_one h₁ x
Isometry Preserves Non-Negative Norm When Fixing Identity
Informal description
Let $E$ and $F$ be seminormed groups, and let $f : E \to F$ be an isometry such that $f(1) = 1$. Then for any $x \in E$, the non-negative norm of $f(x)$ equals the non-negative norm of $x$, i.e., $\|f(x)\|_+ = \|x\|_+$.
dist_self_mul_right theorem
(a b : E) : dist a (a * b) = ‖b‖
Full source 
@[to_additive (attr := simp)]
theorem dist_self_mul_right (a b : E) : dist a (a * b) = ‖b‖ := by
  rw [← dist_one_left, ← dist_mul_left a 1 b, mul_one]
Distance Identity: $\text{dist}(a, a \cdot b) = \|b\|$ in Seminormed Groups
Informal description
For any elements $a$ and $b$ in a seminormed group $E$, the distance between $a$ and $a \cdot b$ is equal to the norm of $b$, i.e., $\text{dist}(a, a \cdot b) = \|b\|$.
dist_self_mul_left theorem
(a b : E) : dist (a * b) a = ‖b‖
Full source 
@[to_additive (attr := simp)]
theorem dist_self_mul_left (a b : E) : dist (a * b) a = ‖b‖ := by
  rw [dist_comm, dist_self_mul_right]
Distance Identity: $\text{dist}(a \cdot b, a) = \|b\|$ in Seminormed Groups
Informal description
For any elements $a$ and $b$ in a seminormed group $E$, the distance between $a \cdot b$ and $a$ is equal to the norm of $b$, i.e., $\text{dist}(a \cdot b, a) = \|b\|$.
dist_self_div_right theorem
(a b : E) : dist a (a / b) = ‖b‖
Full source 
@[to_additive (attr := simp 1001)] -- Increase priority because `simp` can prove this
theorem dist_self_div_right (a b : E) : dist a (a / b) = ‖b‖ := by
  rw [div_eq_mul_inv, dist_self_mul_right, norm_inv']
Distance Identity: $\text{dist}(a, a / b) = \|b\|$ in Seminormed Groups
Informal description
For any elements $a$ and $b$ in a seminormed group $E$, the distance between $a$ and $a / b$ is equal to the norm of $b$, i.e., $\text{dist}(a, a / b) = \|b\|$.
dist_self_div_left theorem
(a b : E) : dist (a / b) a = ‖b‖
Full source 
@[to_additive (attr := simp 1001)] -- Increase priority because `simp` can prove this
theorem dist_self_div_left (a b : E) : dist (a / b) a = ‖b‖ := by
  rw [dist_comm, dist_self_div_right]
Distance Identity: $\text{dist}(a / b, a) = \|b\|$ in Seminormed Groups
Informal description
For any elements $a$ and $b$ in a seminormed group $E$, the distance between $a / b$ and $a$ is equal to the norm of $b$, i.e., $\text{dist}(a / b, a) = \|b\|$.
dist_mul_mul_le theorem
(a₁ a₂ b₁ b₂ : E) : dist (a₁ * a₂) (b₁ * b₂) ≤ dist a₁ b₁ + dist a₂ b₂
Full source 
@[to_additive]
theorem dist_mul_mul_le (a₁ a₂ b₁ b₂ : E) : dist (a₁ * a₂) (b₁ * b₂) ≤ dist a₁ b₁ + dist a₂ b₂ := by
  simpa only [dist_mul_left, dist_mul_right] using dist_triangle (a₁ * a₂) (b₁ * a₂) (b₁ * b₂)
Triangle Inequality for Products in Seminormed Commutative Groups
Informal description
For any elements $a_1, a_2, b_1, b_2$ in a seminormed commutative group $E$, the distance between the products $a_1 * a_2$ and $b_1 * b_2$ satisfies the inequality: \[ \text{dist}(a_1 a_2, b_1 b_2) \leq \text{dist}(a_1, b_1) + \text{dist}(a_2, b_2). \]
dist_mul_mul_le_of_le theorem
(h₁ : dist a₁ b₁ ≤ r₁) (h₂ : dist a₂ b₂ ≤ r₂) : dist (a₁ * a₂) (b₁ * b₂) ≤ r₁ + r₂
Full source 
@[to_additive]
theorem dist_mul_mul_le_of_le (h₁ : dist a₁ b₁ ≤ r₁) (h₂ : dist a₂ b₂ ≤ r₂) :
    dist (a₁ * a₂) (b₁ * b₂) ≤ r₁ + r₂ :=
  (dist_mul_mul_le a₁ a₂ b₁ b₂).trans <| add_le_add h₁ h₂
Bounded Distance Inequality for Products in Seminormed Commutative Groups
Informal description
For any elements $a_1, a_2, b_1, b_2$ in a seminormed commutative group $E$, if the distances satisfy $\text{dist}(a_1, b_1) \leq r_1$ and $\text{dist}(a_2, b_2) \leq r_2$, then the distance between the products $a_1 a_2$ and $b_1 b_2$ satisfies the inequality: \[ \text{dist}(a_1 a_2, b_1 b_2) \leq r_1 + r_2. \]
dist_div_div_le theorem
(a₁ a₂ b₁ b₂ : E) : dist (a₁ / a₂) (b₁ / b₂) ≤ dist a₁ b₁ + dist a₂ b₂
Full source 
@[to_additive]
theorem dist_div_div_le (a₁ a₂ b₁ b₂ : E) : dist (a₁ / a₂) (b₁ / b₂) ≤ dist a₁ b₁ + dist a₂ b₂ := by
  simpa only [div_eq_mul_inv, dist_inv_inv] using dist_mul_mul_le a₁ a₂⁻¹ b₁ b₂⁻¹
Triangle Inequality for Quotients in Seminormed Commutative Groups
Informal description
For any elements $a_1, a_2, b_1, b_2$ in a seminormed commutative group $E$, the distance between the quotients $a_1 / a_2$ and $b_1 / b_2$ satisfies the inequality: \[ \text{dist}(a_1 / a_2, b_1 / b_2) \leq \text{dist}(a_1, b_1) + \text{dist}(a_2, b_2). \]
dist_div_div_le_of_le theorem
(h₁ : dist a₁ b₁ ≤ r₁) (h₂ : dist a₂ b₂ ≤ r₂) : dist (a₁ / a₂) (b₁ / b₂) ≤ r₁ + r₂
Full source 
@[to_additive]
theorem dist_div_div_le_of_le (h₁ : dist a₁ b₁ ≤ r₁) (h₂ : dist a₂ b₂ ≤ r₂) :
    dist (a₁ / a₂) (b₁ / b₂) ≤ r₁ + r₂ :=
  (dist_div_div_le a₁ a₂ b₁ b₂).trans <| add_le_add h₁ h₂
Bounded Distance Inequality for Quotients in Seminormed Commutative Groups
Informal description
For any elements $a_1, a_2, b_1, b_2$ in a seminormed commutative group $E$, if $\text{dist}(a_1, b_1) \leq r_1$ and $\text{dist}(a_2, b_2) \leq r_2$, then the distance between the quotients $a_1 / a_2$ and $b_1 / b_2$ satisfies the inequality: \[ \text{dist}(a_1 / a_2, b_1 / b_2) \leq r_1 + r_2. \]
abs_dist_sub_le_dist_mul_mul theorem
(a₁ a₂ b₁ b₂ : E) : |dist a₁ b₁ - dist a₂ b₂| ≤ dist (a₁ * a₂) (b₁ * b₂)
Full source 
@[to_additive]
theorem abs_dist_sub_le_dist_mul_mul (a₁ a₂ b₁ b₂ : E) :
    |dist a₁ b₁ - dist a₂ b₂| ≤ dist (a₁ * a₂) (b₁ * b₂) := by
  simpa only [dist_mul_left, dist_mul_right, dist_comm b₂] using
    abs_dist_sub_le (a₁ * a₂) (b₁ * b₂) (b₁ * a₂)
Reverse Triangle Inequality for Products in Seminormed Commutative Groups
Informal description
For any four elements $a_1, a_2, b_1, b_2$ in a seminormed commutative group $E$, the absolute difference between the distances $\text{dist}(a_1, b_1)$ and $\text{dist}(a_2, b_2)$ is bounded by the distance between the products $a_1 \cdot a_2$ and $b_1 \cdot b_2$, i.e., \[ |\text{dist}(a_1, b_1) - \text{dist}(a_2, b_2)| \leq \text{dist}(a_1 \cdot a_2, b_1 \cdot b_2). \]
nndist_mul_mul_le theorem
(a₁ a₂ b₁ b₂ : E) : nndist (a₁ * a₂) (b₁ * b₂) ≤ nndist a₁ b₁ + nndist a₂ b₂
Full source 
@[to_additive]
theorem nndist_mul_mul_le (a₁ a₂ b₁ b₂ : E) :
    nndist (a₁ * a₂) (b₁ * b₂) ≤ nndist a₁ b₁ + nndist a₂ b₂ :=
  NNReal.coe_le_coe.1 <| dist_mul_mul_le a₁ a₂ b₁ b₂
Triangle Inequality for Non-Negative Distance of Products in Seminormed Commutative Groups
Informal description
For any elements $a_1, a_2, b_1, b_2$ in a seminormed commutative group $E$, the non-negative distance between the products $a_1 a_2$ and $b_1 b_2$ satisfies the inequality: \[ \text{nndist}(a_1 a_2, b_1 b_2) \leq \text{nndist}(a_1, b_1) + \text{nndist}(a_2, b_2). \]
edist_mul_mul_le theorem
(a₁ a₂ b₁ b₂ : E) : edist (a₁ * a₂) (b₁ * b₂) ≤ edist a₁ b₁ + edist a₂ b₂
Full source 
@[to_additive]
theorem edist_mul_mul_le (a₁ a₂ b₁ b₂ : E) :
    edist (a₁ * a₂) (b₁ * b₂) ≤ edist a₁ b₁ + edist a₂ b₂ := by
  simp only [edist_nndist]
  norm_cast
  apply nndist_mul_mul_le
Triangle Inequality for Extended Distance of Products in Seminormed Commutative Groups
Informal description
For any elements $a_1, a_2, b_1, b_2$ in a seminormed commutative group $E$, the extended distance between the products $a_1 a_2$ and $b_1 b_2$ satisfies the inequality: \[ \text{edist}(a_1 a_2, b_1 b_2) \leq \text{edist}(a_1, b_1) + \text{edist}(a_2, b_2). \]
antilipschitzWith_inv_iff theorem
: AntilipschitzWith K f⁻¹ ↔ AntilipschitzWith K f
Full source 
@[to_additive (attr := simp)]
lemma antilipschitzWith_inv_iff : AntilipschitzWithAntilipschitzWith K f⁻¹ ↔ AntilipschitzWith K f := by
  simp [AntilipschitzWith]
Antilipschitz Property of Inverse Function: $f^{-1}$ is $K$-antilipschitz iff $f$ is $K$-antilipschitz
Informal description
For any function $f$ and constant $K$, the inverse function $f^{-1}$ is $K$-antilipschitz if and only if $f$ is $K$-antilipschitz.
lipschitzOnWith_inv_iff theorem
: LipschitzOnWith K f⁻¹ s ↔ LipschitzOnWith K f s
Full source 
@[to_additive (attr := simp)]
lemma lipschitzOnWith_inv_iff : LipschitzOnWithLipschitzOnWith K f⁻¹ s ↔ LipschitzOnWith K f s := by
  simp [LipschitzOnWith]
Lipschitz Condition for Inverse Function on a Set: $f^{-1}$ is $K$-Lipschitz on $s$ iff $f$ is $K$-Lipschitz on $s$
Informal description
For a function $f$ and a set $s$, the inverse function $f^{-1}$ is $K$-Lipschitz on $s$ if and only if $f$ is $K$-Lipschitz on $s$.
LipschitzOnWith.mul theorem
(hf : LipschitzOnWith Kf f s) (hg : LipschitzOnWith Kg g s) : LipschitzOnWith (Kf + Kg) (fun x ↦ f x * g x) s
Full source 
@[to_additive]
lemma LipschitzOnWith.mul (hf : LipschitzOnWith Kf f s) (hg : LipschitzOnWith Kg g s) :
    LipschitzOnWith (Kf + Kg) (fun x ↦ f x * g x) s := fun x hx y hy ↦
  calc
    edist (f x * g x) (f y * g y) ≤ edist (f x) (f y) + edist (g x) (g y) :=
      edist_mul_mul_le _ _ _ _
    _ ≤ Kf * edist x y + Kg * edist x y := add_le_add (hf hx hy) (hg hx hy)
    _ = (Kf + Kg) * edist x y := (add_mul _ _ _).symm
Lipschitz Property of Product Function on a Set
Informal description
Let $f$ and $g$ be functions defined on a set $s$ in a seminormed commutative group $E$, with Lipschitz constants $K_f$ and $K_g$ respectively. Then the product function $x \mapsto f(x) * g(x)$ is Lipschitz on $s$ with constant $K_f + K_g$.
LipschitzWith.mul theorem
(hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) : LipschitzWith (Kf + Kg) fun x ↦ f x * g x
Full source 
@[to_additive]
lemma LipschitzWith.mul (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) :
    LipschitzWith (Kf + Kg) fun x ↦ f x * g x := by
  simpa [← lipschitzOnWith_univ] using hf.lipschitzOnWith.mul hg.lipschitzOnWith
Lipschitz Constant of Product Function: $K_f + K_g$
Informal description
Let $f$ and $g$ be Lipschitz functions with constants $K_f$ and $K_g$ respectively. Then the pointwise product function $x \mapsto f(x) * g(x)$ is Lipschitz with constant $K_f + K_g$.
LocallyLipschitzOn.mul theorem
(hf : LocallyLipschitzOn s f) (hg : LocallyLipschitzOn s g) : LocallyLipschitzOn s fun x ↦ f x * g x
Full source 
@[to_additive]
lemma LocallyLipschitzOn.mul (hf : LocallyLipschitzOn s f) (hg : LocallyLipschitzOn s g) :
    LocallyLipschitzOn s fun x ↦ f x * g x := fun x hx ↦ by
  obtain ⟨Kf, t, ht, hKf⟩ := hf hx
  obtain ⟨Kg, u, hu, hKg⟩ := hg hx
  exact ⟨Kf + Kg, t ∩ u, inter_mem ht hu,
    (hKf.mono Set.inter_subset_left).mul (hKg.mono Set.inter_subset_right)⟩
Local Lipschitz Property of Product Function on a Set
Informal description
Let $f$ and $g$ be functions defined on a set $s$ in a seminormed commutative group $E$, such that $f$ and $g$ are locally Lipschitz on $s$. Then the product function $x \mapsto f(x) * g(x)$ is locally Lipschitz on $s$.
LocallyLipschitz.mul theorem
(hf : LocallyLipschitz f) (hg : LocallyLipschitz g) : LocallyLipschitz fun x ↦ f x * g x
Full source 
@[to_additive]
lemma LocallyLipschitz.mul (hf : LocallyLipschitz f) (hg : LocallyLipschitz g) :
    LocallyLipschitz fun x ↦ f x * g x := by
  simpa [← locallyLipschitzOn_univ] using hf.locallyLipschitzOn.mul hg.locallyLipschitzOn
Local Lipschitz Property of Pointwise Product Function
Informal description
Let $f$ and $g$ be locally Lipschitz functions on a seminormed commutative group $E$. Then the pointwise product function $x \mapsto f(x) * g(x)$ is locally Lipschitz.
LipschitzOnWith.div theorem
(hf : LipschitzOnWith Kf f s) (hg : LipschitzOnWith Kg g s) : LipschitzOnWith (Kf + Kg) (fun x ↦ f x / g x) s
Full source 
@[to_additive]
lemma LipschitzOnWith.div (hf : LipschitzOnWith Kf f s) (hg : LipschitzOnWith Kg g s) :
    LipschitzOnWith (Kf + Kg) (fun x ↦ f x / g x) s := by
  simpa only [div_eq_mul_inv] using hf.mul hg.inv
Lipschitz Property of Quotient Function on a Set: $\text{Lip}(f/g) \leq \text{Lip}(f) + \text{Lip}(g)$
Informal description
Let $E$ be a seminormed commutative group, and let $f, g : E \to E$ be functions defined on a subset $s \subseteq E$. If $f$ is Lipschitz on $s$ with constant $K_f$ and $g$ is Lipschitz on $s$ with constant $K_g$, then the function $x \mapsto f(x) / g(x)$ is Lipschitz on $s$ with constant $K_f + K_g$.
LipschitzWith.div theorem
(hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) : LipschitzWith (Kf + Kg) fun x => f x / g x
Full source 
@[to_additive]
theorem LipschitzWith.div (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) :
    LipschitzWith (Kf + Kg) fun x => f x / g x := by
  simpa only [div_eq_mul_inv] using hf.mul hg.inv
Lipschitz Property of Quotient Function: $\text{Lip}(f/g) \leq \text{Lip}(f) + \text{Lip}(g)$
Informal description
Let $E$ be a seminormed commutative group and let $f, g : E \to E$ be Lipschitz functions with constants $K_f$ and $K_g$ respectively. Then the function $x \mapsto f(x) / g(x)$ is Lipschitz with constant $K_f + K_g$.
LocallyLipschitzOn.div theorem
(hf : LocallyLipschitzOn s f) (hg : LocallyLipschitzOn s g) : LocallyLipschitzOn s fun x ↦ f x / g x
Full source 
@[to_additive]
lemma LocallyLipschitzOn.div (hf : LocallyLipschitzOn s f) (hg : LocallyLipschitzOn s g) :
    LocallyLipschitzOn s fun x ↦ f x / g x := by
  simpa only [div_eq_mul_inv] using hf.mul hg.inv
Local Lipschitz Property of Quotient Function on a Set
Informal description
Let $E$ be a seminormed commutative group and $s \subseteq E$ a subset. If $f, g : E \to E$ are locally Lipschitz functions on $s$, then the quotient function $x \mapsto f(x) / g(x)$ is locally Lipschitz on $s$.
LocallyLipschitz.div theorem
(hf : LocallyLipschitz f) (hg : LocallyLipschitz g) : LocallyLipschitz fun x ↦ f x / g x
Full source 
@[to_additive]
lemma LocallyLipschitz.div (hf : LocallyLipschitz f) (hg : LocallyLipschitz g) :
    LocallyLipschitz fun x ↦ f x / g x := by
  simpa only [div_eq_mul_inv] using hf.mul hg.inv
Local Lipschitz Property of Quotient Function
Informal description
Let $E$ be a seminormed commutative group and let $f, g : E \to E$ be locally Lipschitz functions. Then the function $x \mapsto f(x) / g(x)$ is locally Lipschitz.
AntilipschitzWith.mul_lipschitzWith theorem
(hf : AntilipschitzWith Kf f) (hg : LipschitzWith Kg g) (hK : Kg < Kf⁻¹) : AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ fun x => f x * g x
Full source 
@[to_additive]
theorem mul_lipschitzWith (hf : AntilipschitzWith Kf f) (hg : LipschitzWith Kg g) (hK : Kg < Kf⁻¹) :
    AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ fun x => f x * g x := by
  letI : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace hf.edist_ne_top
  refine AntilipschitzWith.of_le_mul_dist fun x y => ?_
  rw [NNReal.coe_inv, ← _root_.div_eq_inv_mul]
  rw [le_div_iff₀ (NNReal.coe_pos.2 <| tsub_pos_iff_lt.2 hK)]
  rw [mul_comm, NNReal.coe_sub hK.le, sub_mul]
  calc
    ↑Kf⁻¹ * dist x y - Kg * dist x y ≤ dist (f x) (f y) - dist (g x) (g y) :=
      sub_le_sub (hf.mul_le_dist x y) (hg.dist_le_mul x y)
    _ ≤ _ := le_trans (le_abs_self _) (abs_dist_sub_le_dist_mul_mul _ _ _ _)
Antilipschitz Property of Product of Antilipschitz and Lipschitz Maps
Informal description
Let $E$ and $F$ be seminormed commutative groups, and let $f : E \to F$ be an antilipschitz map with constant $K_f$. Let $g : E \to F$ be a Lipschitz map with constant $K_g$ such that $K_g < K_f^{-1}$. Then the map $x \mapsto f(x) \cdot g(x)$ is antilipschitz with constant $(K_f^{-1} - K_g)^{-1}$.
AntilipschitzWith.mul_div_lipschitzWith theorem
(hf : AntilipschitzWith Kf f) (hg : LipschitzWith Kg (g / f)) (hK : Kg < Kf⁻¹) : AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ g
Full source 
@[to_additive]
theorem mul_div_lipschitzWith (hf : AntilipschitzWith Kf f) (hg : LipschitzWith Kg (g / f))
    (hK : Kg < Kf⁻¹) : AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ g := by
  simpa only [Pi.div_apply, mul_div_cancel] using hf.mul_lipschitzWith hg hK
Antilipschitz Property of $g$ via $g/f$ Lipschitz: $\text{AntilipschitzWith}((K_f^{-1} - K_g)^{-1}, g)$
Informal description
Let $E$ and $F$ be seminormed commutative groups, and let $f : E \to F$ be an antilipschitz map with constant $K_f$. Let $g : E \to F$ be a map such that the function $x \mapsto g(x) / f(x)$ is Lipschitz with constant $K_g$, where $K_g < K_f^{-1}$. Then $g$ is antilipschitz with constant $(K_f^{-1} - K_g)^{-1}$.
AntilipschitzWith.le_mul_norm_div theorem
{f : E → F} (hf : AntilipschitzWith K f) (x y : E) : ‖x / y‖ ≤ K * ‖f x / f y‖
Full source 
@[to_additive le_mul_norm_sub]
theorem le_mul_norm_div {f : E → F} (hf : AntilipschitzWith K f) (x y : E) :
    ‖x / y‖ ≤ K * ‖f x / f y‖ := by simp [← dist_eq_norm_div, hf.le_mul_dist x y]
Norm Inequality for Antilipschitz Maps on Seminormed Groups: $\|x / y\| \leq K \cdot \|f(x) / f(y)\|$
Informal description
Let $E$ and $F$ be seminormed commutative groups, and let $f : E \to F$ be an antilipschitz map with constant $K$. Then for any $x, y \in E$, the norm of $x / y$ is bounded by $K$ times the norm of $f(x) / f(y)$, i.e., \[ \|x / y\| \leq K \cdot \|f(x) / f(y)\|. \]
SeminormedCommGroup.to_isUniformGroup instance
: IsUniformGroup E
Full source 
/-- A seminormed group is a uniform group, i.e., multiplication and division are uniformly
continuous. -/
@[to_additive "A seminormed group is a uniform additive group, i.e., addition and subtraction are
uniformly continuous."]
instance (priority := 100) SeminormedCommGroup.to_isUniformGroup : IsUniformGroup E :=
  ⟨(LipschitzWith.prod_fst.div LipschitzWith.prod_snd).uniformContinuous⟩
Seminormed Commutative Groups are Uniform Groups
Informal description
Every seminormed commutative group $E$ is a uniform group, meaning that the group operations (multiplication and inversion) are uniformly continuous with respect to the uniformity induced by the norm.
SeminormedCommGroup.toIsTopologicalGroup instance
: IsTopologicalGroup E
Full source 
@[to_additive]
instance (priority := 100) SeminormedCommGroup.toIsTopologicalGroup : IsTopologicalGroup E :=
  inferInstance
Seminormed Commutative Groups are Topological Groups
Informal description
Every seminormed commutative group $E$ is a topological group, meaning that the group operations (multiplication and inversion) are continuous with respect to the topology induced by the norm.
SeparationQuotient.instMulNorm instance
: Norm (SeparationQuotient E)
Full source 
@[to_additive instNorm]
instance instMulNorm : Norm (SeparationQuotient E) where
  norm := lift Norm.norm fun _ _ h => h.norm_eq_norm'
Norm on the Separation Quotient of a Seminormed Commutative Group
Informal description
The separation quotient of a seminormed commutative group $E$ inherits a norm structure, where the norm of an equivalence class is defined as the norm of any representative element.
SeparationQuotient.norm_mk' theorem
(p : E) : ‖mk p‖ = ‖p‖
Full source 
@[to_additive (attr := simp) norm_mk]
theorem norm_mk' (p : E) : ‖mk p‖ = ‖p‖ := rfl
Norm Preservation in Separation Quotient
Informal description
For any element $p$ in a seminormed commutative group $E$, the norm of its image under the separation quotient projection map equals the norm of $p$, i.e., $\|\text{mk}(p)\| = \|p\|$.
SeparationQuotient.mk_eq_one_iff theorem
{p : E} : mk p = 1 ↔ ‖p‖ = 0
Full source 
@[to_additive]
theorem mk_eq_one_iff {p : E} : mkmk p = 1 ↔ ‖p‖ = 0 := by
  rw [← norm_mk', norm_eq_zero']
Characterization of Identity in Separation Quotient via Norm Vanishing
Informal description
For any element $p$ in a seminormed commutative group $E$, the image of $p$ under the separation quotient projection map equals the identity element if and only if the norm of $p$ is zero, i.e., $\text{mk}(p) = 1 \leftrightarrow \|p\| = 0$.
SeparationQuotient.nnnorm_mk' theorem
(p : E) : ‖mk p‖₊ = ‖p‖₊
Full source 
@[to_additive (attr := simp) nnnorm_mk]
theorem nnnorm_mk' (p : E) : ‖mk p‖₊ = ‖p‖₊ := rfl
Preservation of Non-Negative Norm under Separation Quotient Projection
Informal description
For any element $p$ in a seminormed commutative group $E$, the non-negative norm of the image of $p$ under the separation quotient projection map is equal to the non-negative norm of $p$, i.e., $\|\text{mk}(p)\|₊ = \|p\|₊$.
cauchySeq_prod_of_eventually_eq theorem
{u v : ℕ → E} {N : ℕ} (huv : ∀ n ≥ N, u n = v n) (hv : CauchySeq fun n => ∏ k ∈ range (n + 1), v k) : CauchySeq fun n => ∏ k ∈ range (n + 1), u k
Full source 
@[to_additive]
theorem cauchySeq_prod_of_eventually_eq {u v : ℕ → E} {N : ℕ} (huv : ∀ n ≥ N, u n = v n)
    (hv : CauchySeq fun n => ∏ k ∈ range (n + 1), v k) :
    CauchySeq fun n => ∏ k ∈ range (n + 1), u k := by
  let d : ℕ → E := fun n => ∏ k ∈ range (n + 1), u k / v k
  rw [show (fun n => ∏ k ∈ range (n + 1), u k) = d * fun n => ∏ k ∈ range (n + 1), v k
      by ext n; simp [d]]
  suffices ∀ n ≥ N, d n = d N from (tendsto_atTop_of_eventually_const this).cauchySeq.mul hv
  intro n hn
  dsimp [d]
  rw [eventually_constant_prod _ (add_le_add_right hn 1)]
  intro m hm
  simp [huv m (le_of_lt hm)]
Cauchy Property of Partial Products under Eventual Equality
Informal description
Let $E$ be a seminormed commutative group, and let $u, v \colon \mathbb{N} \to E$ be sequences such that $u(n) = v(n)$ for all $n \geq N$, where $N \in \mathbb{N}$. If the sequence of partial products $\prod_{k=0}^n v(k)$ is Cauchy, then the sequence of partial products $\prod_{k=0}^n u(k)$ is also Cauchy.
CauchySeq.mul_norm_bddAbove theorem
{G : Type*} [SeminormedGroup G] {u : ℕ → G} (hu : CauchySeq u) : BddAbove (Set.range (fun n ↦ ‖u n‖))
Full source 
@[to_additive CauchySeq.norm_bddAbove]
lemma CauchySeq.mul_norm_bddAbove {G : Type*} [SeminormedGroup G] {u : ℕ → G}
    (hu : CauchySeq u) : BddAbove (Set.range (fun n ↦ ‖u n‖)) := by
  obtain ⟨C, -, hC⟩ := cauchySeq_bdd hu
  simp_rw [SeminormedGroup.dist_eq] at hC
  have : ∀ n, ‖u n‖ ≤ C + ‖u 0‖ := by
    intro n
    rw [add_comm]
    refine (norm_le_norm_add_norm_div' (u n) (u 0)).trans ?_
    simp [(hC _ _).le]
  rw [bddAbove_def]
  exact ⟨C + ‖u 0‖, by simpa using this⟩
Boundedness of Norms in a Cauchy Sequence in Seminormed Groups
Informal description
Let $G$ be a seminormed group and $u : \mathbb{N} \to G$ be a Cauchy sequence. Then the set of norms $\{\|u(n)\| \mid n \in \mathbb{N}\}$ is bounded above.