of_precomp — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem of_precomp [W.HasOfPrecompProperty W'] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : W' f) (hfg : W (f ≫ g)) :
    W g :=
  HasOfPrecompProperty.of_precomp f g hf hfg

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