lt_length'

Mathlib.Combinatorics.Enumerative.Composition

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

English

A more direct bound: every i in Fin c.length satisfies i < c.boundaries.card.

Русский

Каждый i в Fin c.length удовлетворяет i < c.boundaries.card.

LaTeX

$$∀ i : Fin(c.length), (i : ℕ) < c.boundaries.card$$

Lean4

theorem lt_length' (i : Fin c.length) : (i : ℕ) < c.boundaries.card :=
  lt_of_le_of_lt (Nat.le_succ i) (c.lt_length i)

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

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

Разделы

Аффилиация

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