sumCongr_coe — Mathlib

English

Let φ and ψ be diffeomorphisms on the left and right components respectively. The canonical diffeomorphism that acts as φ on the first summand and ψ on the second summand is exactly the disjoint-sum map Sum.map φ ψ; in symbols, sumCongr φ ψ = Sum.map φ ψ.

Русский

Пусть φ и ψ — диффеоморфизмы на соответствующих компонентах. Каноническая диффеоморфизм, действующий как φ на первом сомножителе и как ψ на втором, равен отображению Sum.map φ ψ; то есть sumCongr φ ψ = Sum.map φ ψ.

LaTeX

$$$sumCongr\\,\\phi\\,\\psi = Sum.map\\,\\phi\\psi$$$

Lean4

@[simp, mfld_simps]
theorem sumCongr_coe (φ : Diffeomorph I J M N n) (ψ : Diffeomorph I J M' N' n) : sumCongr φ ψ = Sum.map φ ψ :=
  rfl

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