relabelAux — Mathlib

English

relabelAux is a standard relabeling map used to reindex variables when relabeling bounded formulas.

Русский

relabelAux — стандартное отображение перенумерации переменных при перенумерации ограниченных формул.

LaTeX

$$$\text{relabelAux} (g) (k) : α ⊕ (Fin k) → β ⊕ (Fin (n+k))$ is given by Sum.map and Equiv.sumAssoc composition.$$

Lean4

/-- A function to help relabel the variables in bounded formulas. -/
def relabelAux (g : α → β ⊕ (Fin n)) (k : ℕ) : α ⊕ (Fin k) → β ⊕ (Fin (n + k)) :=
  Sum.map id finSumFinEquiv ∘ Equiv.sumAssoc _ _ _ ∘ Sum.map g id

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