biprod_lift_snd_f — Mathlib

English

For α: M ⟶ K and β: M ⟶ L, the i-th component biprod.lift α β composed with the i-th component biprod.snd equals β.f i.

Русский

Пусть α: M ⟶ K и β: M ⟶ L; тогда (biprod.lift α β).f i ∘ (biprod.snd).f i = β.f i.

LaTeX

$$$ (\mathrm{biprod.lift} \alpha \beta).f i \circ (\mathrm{biprod.snd}).f i = \beta.f i. $$$

Lean4

@[reassoc (attr := simp)]
theorem biprod_lift_snd_f (α : M ⟶ K) (β : M ⟶ L) (i : ι) :
    (biprod.lift α β).f i ≫ (biprod.snd : K ⊞ L ⟶ L).f i = β.f i := by rw [← comp_f, biprod.lift_snd]

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