instLocallyFiniteOrder — Mathlib

English

An instance of LocallyFiniteOrder is provided for positive naturals, enabling finite intervals to be defined between elements.

Русский

Для положительных натуральных чисел задан локально конечный порядок, обеспечивающий конечные интервалы между элементами.

LaTeX

$$$ \\text{LocallyFiniteOrder}(\\mathbb{N}^+) $$$

Lean4

instance instLocallyFiniteOrder : LocallyFiniteOrder ℕ+ :=
  Subtype.instLocallyFiniteOrder _

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