English
For any embedding f: α ⊕ β ↪ γ, mapping the disjoint sum s.disjSum t is equal to the disjoint union of mapped left and mapped right parts: map f (s.disjSum t) = (s.map (inl ∘ f)).disjUnion (t.map (inr ∘ f)).
Русский
Для вложения f: α ⊕ β ↪ γ отображение дизьитной суммы s.disjSum t равно дизьитному объединению образций слева и справа: map f (s.disjSum t) = (s.map (inl ∘ f)).disjUnion (t.map (inr ∘ f)).
LaTeX
$$$ (s.disjSum t).map f = (s.map (\\mathrm{inl} \\circ f)).disjUnion (t.map (\\mathrm{inr} \\circ f)) $$$
Lean4
theorem map_disjSum (f : α ⊕ β ↪ γ) :
(s.disjSum t).map f =
(s.map (.trans .inl f)).disjUnion (t.map (.trans .inr f))
(by as_aux_lemma => simpa only [← map_map] using (Finset.disjoint_map f).2 (disjoint_map_inl_map_inr _ _)) :=
val_injective <| Multiset.map_disjSum _
