rlp_isMultiplicative — Mathlib

English

The RLP class is closed under identities and composition: identities satisfy RLP, and if two arrows have RLP, then their composition has RLP.

Русский

RLP замкнуто относительно тождественных стрелок и композиции: тождественные стрелки удовлетворяют RLP, а если две стрелки удовлетворяют RLP, то их композиция удовлетворяет RLP.

LaTeX

$$$T.rlp.IsMultiplicative$$$

Lean4

instance rlp_isMultiplicative : T.rlp.IsMultiplicative
    where
  id_mem X _ _ p hp := by infer_instance
  comp_mem i j hi hj _ _ p
    hp := by
    have := hi _ hp
    have := hj _ hp
    infer_instance

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