FiniteDimensionalOrder — Mathlib

English

A type γ with a preorder is finite dimensional if the relation {(a,b) in γ×γ | a < b} is finite dimensional in the SetRel sense.

Русский

Тип γ с предортированием конечнодименционален, если отношение {(a,b) : γ×γ | a < b} имеет конечную размерность в смысле SetRel.

LaTeX

$$$$ \\operatorname{FiniteDimensionalOrder}(\\gamma) := \\operatorname{FiniteDimensional}\\{(a,b) \\in \\gamma \\times \\gamma \\mid a < b\\}. $$$$

Lean4

/-- A type is finite dimensional if its `LTSeries` has bounded length. -/
abbrev FiniteDimensionalOrder (γ : Type*) [Preorder γ] :=
  SetRel.FiniteDimensional {(a, b) : γ × γ | a < b}

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