isCauSeq_conj — Mathlib

English

The complex conjugate of a complex CauSeq is again a complex CauSeq: cauSeqConj(f) is a CauSeq in ℂ.

Русский

Сопряжённая комплексной CauSeq снова является CauSeq в ℂ.

LaTeX

$$$\\mathrm{isCauSeq\\_conj}(f):\\ IsCauSeq(\\\\|\\\\cdot\\\\|) (\\\\lambda n.\\\\overline{f(n)})$$$

Lean4

theorem isCauSeq_conj (f : CauSeq ℂ (‖·‖)) : IsCauSeq (‖·‖) fun n ↦ conj (f n) := fun ε ε0 ↦
  let ⟨i, hi⟩ := f.2 ε ε0
  ⟨i, fun j hj => by simp_rw [← RingHom.map_sub, norm_conj]; exact hi j hj⟩

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