coe_embedding

Mathlib.Combinatorics.Enumerative.Composition

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

English

The value of the embedding at (i,j) equals the sum sizeUpTo(i) plus j.

Русский

Значение вложения в позиции (i,j) равно sizeUpTo(i) + j.

LaTeX

$$$(c.embedding\\, i\\, j) = c.sizeUpTo(i) + j$$$

Lean4

@[simp]
theorem coe_embedding (i : Fin c.length) (j : Fin (c.blocksFun i)) : (c.embedding i j : ℕ) = c.sizeUpTo i + j :=
  rfl

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

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

Разделы

Аффилиация

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