fac_app — Mathlib

English

Within a FunctorialFactorizationData, the left component composed with the right component equals the original morphism; i.e., i.app f ≫ p.app f = f.hom.

Русский

В рамках данных факторизации для функториального случая левая часть, затем правая, равна исходному морфизму: i.app f ≫ p.app f = f.hom.

LaTeX

$$$f : Arrow C \; \Rightarrow\; (data.i.app f) ≫ (data.p.app f) = f.hom$$$

Lean4

@[reassoc (attr := simp)]
theorem fac_app {f : Arrow C} : data.i.app f ≫ data.p.app f = f.hom := by
  rw [← NatTrans.comp_app, fac, Arrow.leftToRight_app]

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