right_mono

Mathlib.Order.SemiconjSup

URI: https://scilib.ai/kg/mathlib#IsOrderRightAdjoint.right_mono

← MathLib Explorer

English

If h is a right adjoint for f, then g is monotone.

Русский

Если h — правая сопряжённость к f, то g монотонна.

LaTeX

$$$\\forall \\; {f,g}: \\text{IsOrderRightAdjoint } f g \\Rightarrow \\text{Monotone } g.$$$

Lean4

theorem right_mono [Preorder α] [Preorder β] {f : α → β} {g : β → α} (h : IsOrderRightAdjoint f g) : Monotone g :=
  fun y₁ y₂ hy => ((h y₁).mono (h y₂)) fun _ hx => le_trans hx hy

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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