constantsVarsEquivLeft — Mathlib

English

There is a bijection between terms with constants and terms with extra variables, implemented via a left-side equivalence that relabels variables accordingly.

Русский

Существет биекция между термами с константами и термами с дополнительными переменными, реализованная через левую эквивалентность, переименовывающую переменные соответствующим образом.

LaTeX

$$$L[[\\gamma]].Term(\\alpha\\oplus \\beta) \\simeq L.Term((\\gamma\\oplus \\alpha) \\oplus \\beta)$$$

Lean4

/-- A bijection between terms with constants and terms with extra variables. -/
def constantsVarsEquivLeft : L[[γ]].Term (α ⊕ β) ≃ L.Term ((γ ⊕ α) ⊕ β) :=
  constantsVarsEquiv.trans (relabelEquiv (Equiv.sumAssoc _ _ _)).symm

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