trans_antivary

Mathlib.Order.Monotone.Monovary

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

English

If f is strictly antitone and g antivaries with f, then g is monotone.

Русский

Если f строго антитонична, а g антивариантна по отношению к f, то g монотонна.

LaTeX

$$$$ (StrictAnti\\;f) \\land (Antivary\\;g\\;f) \\Rightarrow Monotone\\;g $$$$

Lean4

theorem trans_antivary (hf : StrictAnti f) (h : Antivary g f) : Monotone g :=
  monotone_iff_forall_lt.2 fun _a _b hab ↦ h <| hf hab

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

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

Разделы

Аффилиация

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