onFormula_symm — Mathlib

English

Given a language equivalence φ, the induced onFormula mapping on formulas commutes with taking symmetries.

Русский

Пусть есть эквивалентность языка φ; индуцированное отображение формул onFormula коммутирует со симметрией.

LaTeX

$$$\\text{onFormula\_symm}(φ) : φ.onFormula.symm = φ.symm.onFormula$$$

Lean4

@[simp]
theorem onFormula_symm (φ : L ≃ᴸ L') : (φ.onFormula.symm : L'.Formula α ≃ L.Formula α) = φ.symm.onFormula :=
  rfl

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