map_id — Mathlib

English

The map on coproducts induced by the identity on each component is the identity on the coproduct.

Русский

Копроизведение, индуцированное тождественными отображениями на каждой компоненте, равняется тождественности на копроизведении.

LaTeX

$$Sigma.map (\lambda a. 𝟙 (f a)) = 𝟙 (∐ f)$$

Lean4

@[simp]
theorem map_id {f : α → C} [HasCoproduct f] : Sigma.map (fun a => 𝟙 (f a)) = 𝟙 (∐ f) := by ext; simp

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