inl_ofComponents — Mathlib

English

For components f11,f12,f21,f22, the map Biprod.ofComponents fed into biprod.inl equals f11 ∘ biprod.inl + f12 ∘ biprod.inr.

Русский

Для компонент f11,f12,f21,f22 отображение Biprod.ofComponents через biprod.inl равно f11 ∘ biprod.inl + f12 ∘ biprod.inr.

LaTeX

$$$\mathrm{Biprod.ofComponents}(f_{11},f_{12},f_{21},f_{22}) \circ \mathrm{biprod.inl} = f_{11} \circ \mathrm{biprod.inl} + f_{12} \circ \mathrm{biprod.inr}$$$

Lean4

@[simp]
theorem inl_ofComponents : biprod.inl ≫ Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂ = f₁₁ ≫ biprod.inl + f₁₂ ≫ biprod.inr := by
  simp [Biprod.ofComponents]

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