functor_obj

Mathlib.CategoryTheory.Category.Preorder

URI: https://scilib.ai/kg/mathlib#Monotone.functor_obj

English

For a monotone function h, the object map of the induced functor h.functor equals the original function.

Русский

Для монотонной функции h отображение объектов функторa, полученного из h, совпадает с самой функцией h.

LaTeX

$$$h.\mathrm{functor}.\mathrm{obj} = f$$$

Lean4

@[simp]
theorem functor_obj {f : X → Y} (h : Monotone f) : h.functor.obj = f :=
  rfl

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

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

Разделы

Аффилиация

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