withLength — Mathlib

English

If the order is InfiniteDimensional, there exists an LTSeries of any prescribed length n.

Русский

Если порядок бесконечно размерен, существует LTSeries любой заданной длины n.

LaTeX

$$$$ \\text{withLength} [InfiniteDimensionalOrder(\\alpha)](n) : LTSeries(\\alpha). $$$$

Lean4

/-- A `<`-series with length `n` if the relation is infinite dimensional -/
protected noncomputable def withLength [InfiniteDimensionalOrder α] (n : ℕ) : LTSeries α :=
  RelSeries.withLength _ n

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