sumCongr — Mathlib

English

Product of sums of two transported structures yields a transported sum on the sum spaces.

Русский

Произведение сумм двух перенесённых объектов даёт перенесённую сумму на пространствах суммы.

LaTeX

$$$SumCongr(\phi, \psi): (M ⊕ M') \to (N ⊕ N')$ is transported$$

Lean4

/-- The sum of two diffeomorphisms: this is `Sum.map` as a diffeomorphism. -/
def sumCongr (φ : Diffeomorph I J M N n) (ψ : Diffeomorph I J M' N' n) : Diffeomorph I J (M ⊕ M') (N ⊕ N') n
    where
  toEquiv := Equiv.sumCongr φ.toEquiv ψ.toEquiv
  contMDiff_toFun := ContMDiff.sumMap φ.contMDiff_toFun ψ.contMDiff_toFun
  contMDiff_invFun := ContMDiff.sumMap φ.contMDiff_invFun ψ.contMDiff_invFun

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