of_postcomp — Mathlib

English

If W has postcomp property with respect to W', and hg is W' g, and hfg is W(f ≫ g), then W f.

Русский

Если W имеет свойство посткомпоновки относительно W', и g удовлетворяет W', а f ≫ g удовлетворяет W, тогда верно W f.

LaTeX

$$$W' g \rightarrow (W(f \gg g) \rightarrow W f)$$$

Lean4

theorem of_postcomp [W.HasOfPostcompProperty W'] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (hg : W' g) (hfg : W (f ≫ g)) :
    W f :=
  HasOfPostcompProperty.of_postcomp f g hg hfg

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