length_le_length_longestOf — Mathlib

English

If r is finite-dimensional, then for any RelSeries x, x.length ≤ (RelSeries.longestOf r).length.

Русский

Если r имеет конечную размерность, то для любой RelSeries x выполняется x.length ≤ (RelSeries.longestOf r).length.

LaTeX

$$$\\forall x : RelSeries\\ r,\ x.length \\le (RelSeries.longestOf r).length$$$

Lean4

theorem length_le_length_longestOf [r.FiniteDimensional] (x : RelSeries r) :
    x.length ≤ (RelSeries.longestOf r).length :=
  SetRel.FiniteDimensional.exists_longest_relSeries.choose_spec _

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