relabel_id_eq_id

Mathlib.ModelTheory.Syntax

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Term.relabel_id_eq_id

English

Relabeling variables by the identity yields the same term; i.e., relabel id = id on L.Term α.

Русский

Переметка переменных по тождественному биекцию даёт тот же терм; relabel id = id на L.Term α.

LaTeX

$$$ \operatorname{Term.relabel} (\mathrm{id}) = \mathrm{id} $$$

Lean4

@[simp]
theorem relabel_id_eq_id : (Term.relabel id : L.Term α → L.Term α) = id :=
  funext relabel_id

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru