monovary

Mathlib.Order.Monotone.Monovary

URI: https://scilib.ai/kg/mathlib#Antitone.monovary

English

If f is antitone and g is monotone, then g monovaries with f.

Русский

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

LaTeX

$$$$ (Antitone\\;f) \\land (Monotone\\;g) \\Rightarrow Monovary\\;f\\;g $$$$

Lean4

protected theorem monovary (hf : Antitone f) (hg : Antitone g) : Monovary f g :=
  (hf.dual_right.antivary hg).dual_left

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

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

Разделы

Аффилиация

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