cauchySeq_const — Mathlib

English

A constant function from a nonempty index set into α is a Cauchy sequence.

Русский

Константная функция из непустого множества индексов в α является Коши-последовательностью.

LaTeX

$$$\\forall x\\inα,\\ \\text{CauchySeq}(\\lambda\\_\\n\\_:β, x).$$$

Lean4

theorem cauchySeq_const [SemilatticeSup β] [Nonempty β] (x : α) : CauchySeq fun _ : β => x :=
  tendsto_const_nhds.cauchySeq

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