constantsVarsEquivLeft_apply — Mathlib

English

There is a left-hand variant of the constants-variables equivalence, respecting associativity of sum types.

Русский

Существует вариант левосторонней эквивалентности констант и переменных, сохраняющий ассоциативность суммы.

LaTeX

$$$L[[\\gamma]].Term(\\alpha\\oplus\\beta) \\xrightarrow{\\text{relabel}} L.Term((\\gamma\\oplus \\alpha) \\oplus \\beta)$$$

Lean4

@[simp]
theorem constantsVarsEquivLeft_apply (t : L[[γ]].Term (α ⊕ β)) :
    constantsVarsEquivLeft t = (constantsToVars t).relabel (Equiv.sumAssoc _ _ _).symm :=
  rfl

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