English
If W1 has a factorization data toward W2 in the opposite direction and W2 is stable under retracts, and W2 ≤ W1.rlp, then W1.rlp = W2.
Русский
Если W1 есть факторизационные данные в отношении W2 противоположно направленным образом, и W2 устойчив к retracts, и W2 ≤ W1.rlp, то W1.rlp = W2.
LaTeX
$$$[HasFactorization W_1 W_2] \land [W_2.IsStableUnderRetracts] \land (W_2 \le W_1.rlp) \Rightarrow W_1.rlp = W_2$$$
Lean4
theorem rlp_eq_of_le_rlp_of_hasFactorization_of_isStableUnderRetracts [HasFactorization W₁ W₂]
[W₂.IsStableUnderRetracts] (h₂ : W₂ ≤ W₁.rlp) : W₁.rlp = W₂ :=
le_antisymm
(fun X Y p hp ↦ by
have h := factorizationData W₁ W₂ p
have := hp _ h.hi
simpa using of_retract (RetractArrow.ofRightLiftingProperty h.fac) h.hp)
h₂
