map_disjSum — Mathlib

English

For any function f, map f distributes over disjSum: map f (s.disjSum t) = map f on inl-s plus map f on inr-t.

Русский

Для любой функции f отображение над дизъюнктной суммой распределяется: map f (s.disjSum t) = map f на inl s + map f на inr t.

LaTeX

$$$ \\text{map } f\\ (s.disjSum t) = \\text{map } (f\\circ \\mathrm{inl})\, s \\; + \\; \\text{map } (f\\circ \\mathrm{inr})\, t $$$

Lean4

theorem map_disjSum (f : α ⊕ β → γ) : (s.disjSum t).map f = s.map (f <| .inl ·) + t.map (f <| .inr ·) := by
  simp_rw [disjSum, map_add, map_map, Function.comp_def]

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