rlp_retracts — Mathlib

English

Let P be a morphism property on arrows in a category. Then the right lifting property with respect to retracts of P coincides with the right lifting property with respect to P itself.

Русский

Пусть P — свойство морфизмов в категории. Тогда правое заполнение диаграммы относительно retracts(P) совпадает с правым заполнением относительно P.

LaTeX

$$$T_{\mathrm{retracts}} \; \mathrm{rlp} = T \; \mathrm{rlp}$$$

Lean4

@[simp]
theorem rlp_retracts : T.retracts.rlp = T.rlp := by
  apply le_antisymm
  · exact antitone_rlp T.le_retracts
  · rw [← le_llp_iff_le_rlp]
    exact T.retracts_le_llp_rlp

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