antitone_llp

Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

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

English

The LLP operation is antitone with respect to the base order: if T ≤ T', then T'.llp ≤ T.llp.

Русский

LLP антитонична по отношению к базовому порядку: если T ≤ T', то T'.llp ≤ T.llp.

LaTeX

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

Lean4

theorem antitone_llp : Antitone (llp : MorphismProperty C → _) := fun _ _ h ↦ gc_llp_rlp.monotone_l h

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

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

Разделы

Аффилиация

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