English
Raises all Fin-indexed variables of a term that are at least m by n', producing a term with variables in Fin(n+n').
Русский
Поднимает все переменные типа Fin, начиная с позиции m, на значение n', получая терм с переменными Fin(n+n').
LaTeX
$$$\\mathrm{liftAt}: {n : \\mathbb{N}} \\to {n' : \\mathbb{N}} \\to L\\Term(\\alpha \\oplus \\mathrm{Fin}\n n) \\to L\\Term(\\alpha \\oplus \\mathrm{Fin}(n+n'))$ defined by relabeling with a map $\\mathrm{Sum.map}\\mathrm{id}\\, (\\mathrm{Fin.castAdd}\\ n'\\cdot)\\,\\text{(etc.)}$$$
Lean4
/-- Raises all of the `Fin`-indexed variables of a term greater than or equal to `m` by `n'`. -/
def liftAt {n : ℕ} (n' m : ℕ) : L.Term (α ⊕ (Fin n)) → L.Term (α ⊕ (Fin (n + n'))) :=
relabel (Sum.map id fun i => if ↑i < m then Fin.castAdd n' i else Fin.addNat i n')
