antitone_rlp

Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

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

English

The RLP operation is antitone with respect to the base order on morphism properties: if T ≤ T', then T'.rlp ≤ T.rlp.

Русский

Операция RLP антитонична по отношению к базовому порядку свойств: если T ≤ T', то T'.rlp ≤ T.rlp.

LaTeX

$$$\mathrm{Antitone}(\mathrm{rlp})$$$

Lean4

theorem antitone_rlp : Antitone (rlp : MorphismProperty C → _) := fun _ _ h ↦ gc_llp_rlp.monotone_u h

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

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

Разделы

Аффилиация

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