llp_isStableUnderCoproductsOfShape

English

LLP is stable under coproducts of shape J: if each component morphism has LLP, the induced coproduct morphism has LLP.

Русский

LLP сохраняется при копроизведениях формы J: если каждый компонентный морфизм имеет LLP, то индуцированный копроизведением морфизм имеет LLP.

LaTeX

$$$T.llp.IsStableUnderCoproductsOfShape J$$$

Lean4

instance llp_isStableUnderCoproductsOfShape (J : Type*) : T.llp.IsStableUnderCoproductsOfShape J :=
  by
  apply IsStableUnderCoproductsOfShape.mk
  intro A B _ _ f hf X Y p hp
  have := fun j ↦ hf j _ hp
  infer_instance

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