instIsComplete — Mathlib

English

The complex numbers are complete with respect to the usual norm, i.e., every Cauchy sequence converges in ℂ.

Русский

Комплексные числа полны в обычной норме, то есть любая последовательность Коши сходится в ℂ.

LaTeX

$$$CauSeq.IsComplete(\\\\mathbb{C}, \\\\|\\\\cdot\\\\|)$$$

Lean4

instance instIsComplete : CauSeq.IsComplete ℂ (‖·‖) :=
  ⟨fun f ↦ ⟨limAux f, equiv_limAux f⟩⟩

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