English
Let G be a seminormed group and u: N → G a Cauchy sequence. Then the norms of the terms are bounded above; equivalently there exists a real constant C such that for all n, ||u(n)|| ≤ C.
Русский
Пусть G — полугруппа с нормой, и u: N → G — последовательность Коши. Тогда нормы членов последовательности ограничены сверху; то есть существует константа C ∈ ℝ такая, что для всех n выполняется ||u(n)|| ≤ C.
LaTeX
$$$\exists C \in \mathbb{R}, \; \forall n \in \mathbb{N}, \; \|u(n)\| \le C$$$
Lean4
@[to_additive CauchySeq.norm_bddAbove]
theorem 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⟩
