withLength — Mathlib

English

There exists a RelSeries r with length n (for infinite-dimensional r).

Русский

Существует RelSeries r длины n (при бесконечной размерности r).

LaTeX

$$$\\exists p : RelSeries\\ r, p.length = n$$$

Lean4

/-- A relation series with length `n` if the relation is infinite dimensional -/
protected noncomputable def withLength [r.InfiniteDimensional] (n : ℕ) : RelSeries r :=
  (SetRel.InfiniteDimensional.exists_relSeries_with_length n).choose

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