comp_reflectsFiniteProducts — Mathlib

English

If F reflects finite products and G reflects finite products, then the composite F ∘ G reflects finite products.

Русский

Если F отражает конечные произведения и G отражает конечные произведения, то композиция F ∘ G отражает конечные произведения.

LaTeX

$$$\mathrm{ReflectsFiniteProducts}(F) \land \mathrm{ReflectsFiniteProducts}(G) \Rightarrow \mathrm{ReflectsFiniteProducts}(F \circ G)$$$

Lean4

instance comp_reflectsFiniteProducts (F : C ⥤ D) (G : D ⥤ E) [ReflectsFiniteProducts F] [ReflectsFiniteProducts G] :
    ReflectsFiniteProducts (F ⋙ G) where reflects _ := inferInstance

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