coe_emptySum — Mathlib

English

The canonical homeomorphism from the swapped empty sum to the swapped space corresponds to the standard Equiv.emptySum in the base category.

Русский

Каноническая гомеоморфия между обратной суммой и соответствующим пространством совпадает с обычной эквивалентностью Equiv.emptySum.

LaTeX

$$$ (emptySum X Y)^{toEquiv} = \\mathrm{Equiv.emptySum } Y X $$$

Lean4

@[simp]
theorem coe_emptySum [IsEmpty Y] : (emptySum X Y).toEquiv = Equiv.emptySum Y X :=
  rfl

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