InfiniteDimensionalOrder — Mathlib

English

An order γ is infinite dimensional if its LTSeries relation has arbitrarily long chains; i.e., possible to have LTSeries of unbounded length.

Русский

Порядок γ бесконечно размерен, если он имеет LTSeries длины неограниченно большой.

LaTeX

$$$$ \\text{InfiniteDimensionalOrder}(\\gamma) := \\operatorname{SetRel.InfiniteDimensional}\\{(a,b)\\in \\gamma\\times\\gamma \\mid a

Lean4

/-- A type is infinite dimensional if it has `LTSeries` of at least arbitrary length -/
abbrev InfiniteDimensionalOrder (γ : Type*) [Preorder γ] :=
  SetRel.InfiniteDimensional {(a, b) : γ × γ | a < b}

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