rlp_isStableUnderProductsOfShape — Mathlib

English

RLP is stable under products of shape J: if each component morphism has RLP, the product morphism has RLP.

Русский

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

LaTeX

$$$T.rlp.IsStableUnderProductsOfShape J$$$

Lean4

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

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