imageToKernel_comp_left — Mathlib

English

Dually, composing on the left via h yields a formula: imageToKernel (h ≫ f) g w = Subobject.ofLE _ _ (imageSubobject_comp_le h f) ≫ imageToKernel f g w.

Русский

Слева: imageToKernel (h ≫ f) g w = Subobject.ofLE ... ≫ imageToKernel f g w.

LaTeX

$$imageToKernel (h ≫ f) g w = Subobject.ofLE _ _ (imageSubobject_comp_le h f) ≫ imageToKernel f g w$$

Lean4

theorem imageToKernel_comp_left {Z : V} (h : Z ⟶ A) (w : f ≫ g = 0) :
    imageToKernel (h ≫ f) g (by simp [w]) = Subobject.ofLE _ _ (imageSubobject_comp_le h f) ≫ imageToKernel f g w :=
  by
  ext
  simp

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