antitone

Mathlib.Order.Monotone.Defs

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

English

If f is strictly antitone on s, then f is antitone on α.

Русский

Если f строго антитонна на s, то она антитонна на всей области определения.

LaTeX

$$$$\\text{StrictAntiOn } f s \\Rightarrow \\text{Antitone } f.$$$$

Lean4

protected theorem antitone (hf : StrictAnti f) : Antitone f :=
  antitone_iff_forall_lt.2 fun _ _ h ↦ (hf h).le

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

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

Разделы

Аффилиация

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