universally_mono

Mathlib.CategoryTheory.MorphismProperty.Limits

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

English

The universally operator is monotone: universally(P) ≤ universally(Q) whenever P ≤ Q.

Русский

Операция universally монотонна: если P ≤ Q, то universally(P) ≤ universally(Q).

LaTeX

$$Monotone(universally)$$

Lean4

theorem universally_mono : Monotone (universally : MorphismProperty C → MorphismProperty C) :=
  fun _ _ h _ _ _ h₁ _ _ _ _ _ H => h _ (h₁ _ _ _ H)

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

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

Разделы

Аффилиация

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