monotone

Mathlib.CategoryTheory.Category.Preorder

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.monotone

English

A functor between preorder categories is monotone on objects.

Русский

Функтор между категориями порядков монотонно отображает вершины.

LaTeX

$$$\forall x,x'\in X,\ x \le x' \Rightarrow F(x) \le F(x').$$$

Lean4

/-- A functor between preorder categories is monotone. -/
@[mono]
theorem monotone (f : X ⥤ Y) : Monotone f.obj := fun _ _ hxy => (f.map hxy.hom).le

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

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

Разделы

Аффилиация

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