relabel — Mathlib

English

Relabeling a bounded formula along a function reindexes its bound variables and free variables accordingly.

Русский

Перелепление ограниченной формулы по функции перестраивает нумерацию переменных.

LaTeX

$$$\text{relabel } g \; \varphi = \text{mapTermRel} \big( t \mapsto t.labeled \big) \dots$$$

Lean4

/-- Relabels a bounded formula's variables along a particular function. -/
def relabel (g : α → β ⊕ (Fin n)) {k} (φ : L.BoundedFormula α k) : L.BoundedFormula β (n + k) :=
  φ.mapTermRel (fun _ t => t.relabel (relabelAux g _)) (fun _ => id) fun _ => castLE (ge_of_eq (add_assoc _ _ _))

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