llp_isMultiplicative — Mathlib

English

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

Русский

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

LaTeX

$$$T.llp.IsMultiplicative$$$

Lean4

instance llp_isMultiplicative : T.llp.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

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