varsToConstants — Mathlib

English

When applying constantsToVars to a variable coming from the left side of the sum, it preserves the left index and moves the constant to the left side as a variable.

Русский

При применении constantsToVars к переменной слева от суммы оно сохраняет левый индекс и переводит константу в левую часть как переменную.

LaTeX

$$$(\\mathrm{var}(\\mathrm{Sum.inl}\,a)).constantsToVars = \\mathrm{var}(\\mathrm{Sum.inl}\,a)$$$

Lean4

/-- Sends a term with extra variables to a term with constants. -/
@[simp]
def varsToConstants : L.Term (γ ⊕ α) → L[[γ]].Term α
  | var (Sum.inr a) => var a
  | var (Sum.inl c) => Constants.term (Sum.inr c)
  | func f ts => func (Sum.inl f) fun i => (ts i).varsToConstants

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