sumComm — Mathlib

English

There is a canonical diffeomorphism that interchanges the two summands: sumComm : Diffeomorph I I (M ⊕ M') (M' ⊕ M) n equals Sum.swap.

Русский

Существуют канонические диффеоморфизмы, переставляющие два сомножителя: sumComm = Sum.swap.

LaTeX

$$$sumComm = Sum.swap$$$

Lean4

/-- The canonical diffeomorphism `M ⊕ M' → M' ⊕ M`: this is `Sum.swap` as a diffeomorphism -/
def sumComm : Diffeomorph I I (M ⊕ M') (M' ⊕ M) n
    where
  toEquiv := Equiv.sumComm M M'
  contMDiff_toFun := ContMDiff.swap
  contMDiff_invFun := ContMDiff.swap

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