rlp_isStableUnderRetracts — Mathlib

English

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

Русский

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

LaTeX

$$$T.rlp.IsStableUnderRetracts$$$

Lean4

instance rlp_isStableUnderRetracts : T.rlp.IsStableUnderRetracts where
  of_retract h hf _ _ g
    hg :=
    letI := hf _ hg
    h.rightLiftingProperty g

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