coprod_inl_inr — Mathlib

English

For any f : M × M₂ → M₃, composing with inl and inr and then taking coprod recovers f: (f ∘ inl) coprod (f ∘ inr) = f.

Русский

Для любого f: M×M₂ → M₃ композиция с inl и inr и затем взятие coprod восстанавливает f: (f ∘ inl) coprod (f ∘ inr) = f.

LaTeX

$$$ (f\\circ (inl\\ R\\ M\\ M_2)).coprod (f\\circ (inr\\ R\\ M\\ M_2)) = f $$$

Lean4

@[simp]
theorem coprod_inl_inr : coprod (inl R M M₂) (inr R M M₂) = LinearMap.id := by
  ext <;> simp only [Prod.mk_add_mk, add_zero, id_apply, coprod_apply, inl_apply, inr_apply, zero_add]

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