inr_ofComponents — Mathlib

English

Similarly, biprod.inr ≫ Biprod.ofComponents f11 f12 f21 f22 = f21 ∘ biprod.inl + f22 ∘ biprod.inr.

Русский

Аналогично, biprod.inr ∘ Biprod.ofComponents f11 f12 f21 f22 = f21 ∘ biprod.inl + f22 ∘ biprod.inr.

LaTeX

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

Lean4

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

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