relabelEquiv — Mathlib

English

Relabeling a bounded formula along a bijection yields an equivalence between corresponding formulas.

Русский

Переназначение ограниченной формулы вдоль биекция приводит к эквивалентности соответствующих формул.

LaTeX

$$$\text{relabelEquiv } (g : α \simeq β) {k} : L.BoundedFormula α k \simeq L.BoundedFormula β k$.$$

Lean4

/-- Relabels a bounded formula's free variables along a bijection. -/
def relabelEquiv (g : α ≃ β) {k} : L.BoundedFormula α k ≃ L.BoundedFormula β k :=
  mapTermRelEquiv (fun _n => Term.relabelEquiv (g.sumCongr (_root_.Equiv.refl _))) fun _n => _root_.Equiv.refl _

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