extend — Mathlib

English

Extend(c) with i: Option(Fin c.length) is defined as ExtendLeft if i = None, else ExtendMiddle i.

Русский

Расширение разбиения c с i: Option(Fin c.length) определено как ExtendLeft при i = None, иначе ExtendMiddle i.

LaTeX

$$$\\text{extend}(c,i) = \\begin{cases} c.extendLeft, & i = \\mathrm{None} \\\\ c.extendMiddle i, & i = \\mathrm{Some}(i) \\end{cases}$$$

Lean4

/-- Extend an ordered partition of `n` entries, by adding singleton to the left or appending it
to one of the existing part. -/
def extend (c : OrderedFinpartition n) (i : Option (Fin c.length)) : OrderedFinpartition (n + 1) :=
  match i with
  | none => c.extendLeft
  | some i => c.extendMiddle i

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