cauSeqNorm — Mathlib

English

Definition: cauSeqNorm(f) is the CauSeq in ℝ corresponding to the norm of a complex CauSeq.

Русский

Определение: cauSeqNorm(f) — CauSeq в ℝ, соответствующий норме комплексной CauSeq.

LaTeX

$$$\\mathrm{cauSeqNorm}(f) = \\langle\\_, \\mathrm{isCauSeq\\_norm} f.2\\rangle$$$

Lean4

/-- The norm of a complex Cauchy sequence, as a real Cauchy sequence. -/
noncomputable def cauSeqNorm (f : CauSeq ℂ (‖·‖)) : CauSeq ℝ abs :=
  ⟨_, isCauSeq_norm f.2⟩

Похожие утверждения