decomp_hom_from — Mathlib

English

For any morphism f : X ⊞ Y → Z, there exist f1 : X → Z and f2 : Y → Z such that f equals fst ∘ f1 plus snd ∘ f2.

Русский

Для любого морфизма f: X ⊞ Y → Z существуют f1: X → Z и f2: Y → Z такие, что f = fst ∘ f1 + snd ∘ f2.

LaTeX

$$$\exists f_1: X \to Z, \exists f_2: Y \to Z, \ f = \pi_1 \circ f_1 + \pi_2 \circ f_2$$$

Lean4

theorem decomp_hom_from (f : X ⊞ Y ⟶ Z) : ∃ f₁ f₂, f = biprod.fst ≫ f₁ + biprod.snd ≫ f₂ :=
  ⟨biprod.inl ≫ f, biprod.inr ≫ f, by aesop⟩

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