CauSeq — Mathlib

English

CauSeq β abv is the type of β-valued sequences that are Cauchy with respect to abv.

Русский

CauSeq β abv — это множество последовательностей значений β, которые являются последовательностями Коши по отношению к abv.

LaTeX

$$$\\CauSeq(\\beta,abv) = \\{ f:\\\\mathbb{N} \\to \\beta \\mid IsCauSeq abv f \\}$$$

Lean4

/-- `CauSeq β abv` is the type of `β`-valued Cauchy sequences, with respect to the absolute value
function `abv`. -/
def CauSeq {α : Type*} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (β : Type*) [Ring β] (abv : β → α) : Type _ :=
  { f : ℕ → β // IsCauSeq abv f }

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