LTSeries — Mathlib

English

LTSeries is the specialization of RelSeries to the relation a < b on a preorder.

Русский

LTSeries есть частный случай RelSeries, где отношение задано как a < b на предпорядке.

LaTeX

$$$$ \\text{LTSeries}(\\alpha) := \\text{RelSeries}\\{(a,b)\\in \\alpha\\times\\alpha \\mid a

Lean4

/-- If `α` is a preorder, a LTSeries is a relation series of the less than relation.
-/
abbrev LTSeries :=
  RelSeries {(a, b) : α × α | a < b}

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