trans_monovary

Mathlib.Order.Monotone.Monovary

URI: https://scilib.ai/kg/mathlib#StrictMono.trans_monovary

English

If f is strictly monotone and Monovary g f, then g is monotone.

Русский

Если f строго монотонна и Monovary g f, то g монотонна.

LaTeX

$$$ (\operatorname{StrictMono} f) \land (\operatorname{Monovary} g f) \implies \operatorname{Monotone} g $$$

Lean4

theorem trans_monovary (hf : StrictMono f) (h : Monovary g f) : Monotone g :=
  monotone_iff_forall_lt.2 fun _a _b hab ↦ h <| hf hab

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

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

Разделы

Аффилиация

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