constantsVarsEquiv — Mathlib

English

There is a bijection between terms with constants and terms with extra variables, giving a one-to-one correspondence between the two representations.

Русский

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

LaTeX

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

Lean4

/-- A bijection between terms with constants and terms with extra variables. -/
@[simps]
def constantsVarsEquiv : L[[γ]].Term α ≃ L.Term (γ ⊕ α) :=
  ⟨constantsToVars, varsToConstants, by
    intro t
    induction t with
    | var => rfl
    | @func n f _ ih =>
      cases n
      · cases f
        · simp [constantsToVars, varsToConstants, ih]
        · simp [constantsToVars, varsToConstants, Constants.term, eq_iff_true_of_subsingleton]
      · obtain - | f := f
        · simp [constantsToVars, varsToConstants, ih]
        · exact isEmptyElim f,
    by
    intro t
    induction t with
    | var x => cases x <;> rfl
    | @func n f _ ih => cases n <;> · simp [varsToConstants, constantsToVars, ih]⟩

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