mapTermRelEquiv — Mathlib

English

An equivalence between languages induces an equivalence between bounded formulas.

Русский

Эквивалентность между языками индуцирует эквивалентность между ограниченными формулам.

LaTeX

$$$\forall L, L', α, β, g, φ,\; (L \to L') \text{ Equiv induces } φ \mapsto φ'.$$$

Lean4

/-- An equivalence of bounded formulas given by an equivalence of terms and an equivalence of
relations. -/
@[simps]
def mapTermRelEquiv (ft : ∀ n, L.Term (α ⊕ (Fin n)) ≃ L'.Term (β ⊕ (Fin n))) (fr : ∀ n, L.Relations n ≃ L'.Relations n)
    {n} : L.BoundedFormula α n ≃ L'.BoundedFormula β n :=
  ⟨mapTermRel (fun n => ft n) (fun n => fr n) fun _ => id,
    mapTermRel (fun n => (ft n).symm) (fun n => (fr n).symm) fun _ => id, fun φ => by simp, fun φ => by simp⟩

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