single_blocksFun — Mathlib

English

If n is positive and c is the composition of n that consists of a single block of size n, then for every index i in the natural indexing of the blocks, the i-th block value equals n.

Русский

Если n положительно и c – композиция n, состоящая из одного блока размером n, то для каждого индекса i в естественной нумерации блоков i-й блок равен n.

LaTeX

$$$\\forall n\\in\\mathbb{N},\\ 0

Lean4

@[simp]
theorem single_blocksFun {n : ℕ} (h : 0 < n) (i : Fin (single n h).length) : (single n h).blocksFun i = n := by
  simp [blocksFun, single]

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