lt_length

Mathlib.Combinatorics.Enumerative.Composition

URI: https://scilib.ai/kg/mathlib#CompositionAsSet.lt_length

English

For an index i in the first c.length positions, i+1 is less than the boundary count.

Русский

Для i в диапазоне длины, i+1 меньше числа границ.

LaTeX

$$forall i in Fin(c.length), (i+1) < c.boundaries.card$$

Lean4

theorem lt_length (i : Fin c.length) : (i : ℕ) + 1 < c.boundaries.card :=
  lt_tsub_iff_right.mp i.2

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru