llp_isStableUnderRetracts — Mathlib

English

The left lifting property with respect to T is stable under retracts: if a morphism with LLP is a retract of another, then the latter also has LLP.

Русский

Левое свойство заполнения по отношению к T сохраняется под retracts: если стрелка с LLP является retract другой стрелки, то последняя стрелка тоже имеет LLP.

LaTeX

$$$T.llp.IsStableUnderRetracts$$$

Lean4

instance llp_isStableUnderRetracts : T.llp.IsStableUnderRetracts where
  of_retract h hg _ _ f
    hf :=
    letI := hg _ hf
    h.leftLiftingProperty f

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