English
Let f be a complex-valued CauSeq (a Cauchy sequence) with respect to the usual complex norm. Then the limit of the sequence of norms equals the norm of the limit: lim (cauSeqNorm f) = ‖lim f‖, i.e., the norm converges along the sequence to the norm of its limit.
Русский
Пусть f — последовательность в комплексных числах, являющаяся последовательностью Коши по обычной норме. Тогда предел последовательности норм равен норме предела: lim (cauSeqNorm f) = ‖lim f‖.
LaTeX
$$$\\displaystyle \\lim (\\|f\\|) = \\|\\lim f\\|$$$
Lean4
theorem lim_norm (f : CauSeq ℂ (‖·‖)) : lim (cauSeqNorm f) = ‖lim f‖ :=
lim_eq_of_equiv_const fun ε ε0 ↦
let ⟨i, hi⟩ := equiv_lim f ε ε0
⟨i, fun j hj => lt_of_le_of_lt (abs_norm_sub_norm_le _ _) (hi j hj)⟩
