onBoundedFormula_symm — Mathlib

English

A specialized identity for symmetry of bounded formula mapping: the symmetrized bounded formula mapping equals the mapped symmetric bounded formula.

Русский

Специальная тождественность симметрии отображения ограниченной формулы: симметризованное отображение ограниченной формулы равно отображению симметричного соответствия.

LaTeX

$$$\\text{onBoundedFormula_symm}(\\phi) : (\\phi.onBoundedFormula).symm = \\phi.symm.onBoundedFormula$$$

Lean4

theorem onBoundedFormula_symm (φ : L ≃ᴸ L') :
    (φ.onBoundedFormula.symm : L'.BoundedFormula α n ≃ L.BoundedFormula α n) = φ.symm.onBoundedFormula :=
  rfl

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