cauSeqConj — Mathlib

English

Definition: cauSeqConj(f) is the CauSeq whose nth term is the conjugate of f(n) and which uses isCauSeq_conj as its justification.

Русский

Определение: cauSeqConj(f) есть CauSeq, чьим n-ым членом является сопряжённое к f(n) с обоснованием isCauSeq_conj.

LaTeX

$$$\\mathrm{cauSeqConj}(f) = \\langle\\_, \\mathrm{isCauSeq\\_conj} f\\rangle$$$

Lean4

/-- The complex conjugate of a complex Cauchy sequence, as a complex Cauchy sequence. -/
noncomputable def cauSeqConj (f : CauSeq ℂ (‖·‖)) : CauSeq ℂ (‖·‖) :=
  ⟨_, isCauSeq_conj f⟩

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