English
For any CauSeq f of complex numbers, lim f equals Re-part limit plus i times Im-part limit: lim f = (lim cauSeqRe f) + (lim cauSeqIm f) ⋅ i.
Русский
Для любой CauSeq f комплексных чисел предел x равен сумме предела вещественной части и i раза предела мнимой части: lim f = lim cauSeqRe f + i · lim cauSeqIm f.
LaTeX
$$$\\lim f = \\big(\\lim (cauSeqRe f)\\big) + \\big(\\lim (cauSeqIm f)\\big) \\cdot i$$$
Lean4
theorem lim_eq_lim_im_add_lim_re (f : CauSeq ℂ (‖·‖)) : lim f = ↑(lim (cauSeqRe f)) + ↑(lim (cauSeqIm f)) * I :=
lim_eq_of_equiv_const <|
letI : IsAbsoluteValue (‖·‖ : ℂ → ℝ) := inferInstance
calc
f ≈ _ := equiv_limAux f
_ = CauSeq.const (‖·‖) (↑(lim (cauSeqRe f)) + ↑(lim (cauSeqIm f)) * I) :=
CauSeq.ext fun _ ↦ Complex.ext (by simp [limAux, cauSeqRe, ofReal]) (by simp [limAux, cauSeqIm, ofReal])
