Chain — Mathlib

English

A chain in a preorder α is a monotone function from the natural numbers to α, i.e., a monotone sequence.

Русский

Цепь в частично упорядоченном множестве α — это монотонная функция из натуральных чисел в α, то есть монотонная последовательность.

LaTeX

$$$\\text{Chain}(\\alpha) = \\{ f: \\mathbb{N} \\to \\alpha \\mid f \\text{ is monotone} \\}$$$

Lean4

/-- A chain is a monotone sequence.

See the definition on page 114 of [gunter1992]. -/
def Chain (α : Type u) [Preorder α] :=
  ℕ →o α

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