le_llp_rlp

Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

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

English

The left-hand side is less than or equal to the LLP of the right-hand side: T ≤ T.rlp.llp.

Русский

Левое неравенство не превосходит LLP у правой стороны: T ≤ T.rlp.llp.

LaTeX

$$$T \le T.rlp.llp$$$

Lean4

theorem le_llp_rlp : T ≤ T.rlp.llp := by rw [le_llp_iff_le_rlp]

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

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

Разделы

Аффилиация

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