sumEmpty — Mathlib

English

The canonical sumEmpty diffeomorphism corresponds to Equiv.sumEmpty on the underlying types.

Русский

Каноническое отображение sumEmpty совпадает с Equiv.sumEmpty.

LaTeX

$$$ sumEmpty I I (M \\oplus M') M n = Equiv.sumEmpty M M' $$$

Lean4

/-- The canonical diffeomorphism `M ⊕ ∅ → M` -/
def sumEmpty [IsEmpty M'] : Diffeomorph I I (M ⊕ M') M n
    where
  toEquiv := Equiv.sumEmpty M M'
  contMDiff_toFun := contMDiff_id.sumElim fun x ↦ (IsEmpty.false x).elim
  contMDiff_invFun := ContMDiff.inl

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