llp_rlp_llp

Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.llp_rlp_llp

English

Applying LLP, then RLP, then LLP yields the same as applying LLP: T.llp.rlp.llp = T.llp.

Русский

Применение LLP, затем RLP, затем LLP даёт то же, что и один раз LLP: T.llp.rlp.llp = T.llp.

LaTeX

$$$T.llp.rlp.llp = T.llp$$$

Lean4

@[simp]
theorem llp_rlp_llp : T.llp.rlp.llp = T.llp :=
  gc_llp_rlp.l_u_l_eq_l T

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru