extend_some — Mathlib

English

Let c be an ordered finite partition of n and i an index in Fin(c.length). Extending c by i coincides with the middle extension, i.e., c.extend i = c.extendMiddle i.

Русский

Пусть c — упорядоченная конечная разби́вка множества с размерностью n, и i — индекс в Fin(c.length). Расширение c на позицию i совпадает с средним расширением: c.extend i = c.extendMiddle i.

LaTeX

$$$c.\mathrm{extend}(i) = c.\mathrm{extendMiddle}(i)$$$

Lean4

@[simp]
theorem extend_some (c : OrderedFinpartition n) (i : Fin c.length) : c.extend i = c.extendMiddle i :=
  rfl

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