trans_antivary

Mathlib.Order.Monotone.Monovary

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

English

If f is strictly monotone and Antivary g f, then g is Antitone.

Русский

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

LaTeX

$$$ (\operatorname{StrictMono} f) \land (\operatorname{Antivary} g f) \implies \operatorname{Antitone} g $$$

Lean4

theorem trans_antivary (hf : StrictMono f) (h : Antivary g f) : Antitone g :=
  antitone_iff_forall_lt.2 fun _a _b hab ↦ h <| hf hab

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

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

Разделы

Аффилиация

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