lt_sizeUpTo_index_succ

Mathlib.Combinatorics.Enumerative.Composition

URI: https://scilib.ai/kg/mathlib#Composition.lt_sizeUpTo_index_succ

English

For any j ∈ Fin n, sizeUpTo(index j) ≤ j (as natural numbers).

Русский

Для любого j ∈ Fin n, sizeUpTo(index j) ≤ j (по натуральным числам).

LaTeX

$$$c.sizeUpTo(c.index(j)) \\le j$$$

Lean4

theorem lt_sizeUpTo_index_succ (j : Fin n) : (j : ℕ) < c.sizeUpTo (c.index j).succ :=
  (Nat.find_spec (c.index_exists j.2)).1

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

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

Разделы

Аффилиация

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