relabelEquiv — Mathlib

English

Relabels a term's variables along a bijection; this yields a natural equivalence between L.Term α and L.Term β when α ≃ β.

Русский

Переименовывает переменные терма по биекции, образуя естественное эквивалентное соответствие между L.Term α и L.Term β при α ≃ β.

LaTeX

$$$ \text{relabelEquiv }(g) : L.\text{Term }\alpha \simeq L.\text{Term }\beta $$$

Lean4

/-- Relabels a term's variables along a bijection. -/
@[simps]
def relabelEquiv (g : α ≃ β) : L.Term α ≃ L.Term β :=
  ⟨relabel g, relabel g.symm, fun t => by simp, fun t => by simp⟩

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