rlp_llp_rlp

Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem rlp_llp_rlp : T.rlp.llp.rlp = T.rlp :=
  gc_llp_rlp.u_l_u_eq_u T

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

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

Разделы

Аффилиация

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