sumCongr_symm_symm — Mathlib

English

The diffeomorphism induced by swapping the sums is symmetric under taking inverses.

Русский

Диффеоморфизм, индуцируемый обменом сумм, симметричен относительно взятия обратной.

LaTeX

$$sumCongr φ.symm ψ.symm = (sumCongr φ ψ).symm$$

Lean4

theorem sumCongr_symm_symm (φ : Diffeomorph I J M N n) (ψ : Diffeomorph I J M' N' n) :
    sumCongr φ.symm ψ.symm = (sumCongr φ ψ).symm :=
  rfl

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