lim_conj — Mathlib

English

The limit of the conjugate sequence equals the conjugate of the limit: lim(cauSeqConj f) = conj(lim f).

Русский

Предел сопряжённой CauSeq равен сопряжению предела: lim(cauSeqConj f) = conj(lim f).

LaTeX

$$$\\lim (\\\\mathrm{cauSeqConj} f) = \\overline{\\lim f}$$$

Lean4

theorem lim_conj (f : CauSeq ℂ (‖·‖)) : lim (cauSeqConj f) = conj (lim f) :=
  Complex.ext (by simp [cauSeqConj, (lim_re _).symm, cauSeqRe])
    (by simp [cauSeqConj, (lim_im _).symm, cauSeqIm, (lim_neg _).symm]; rfl)

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