comp_antitoneOn

Mathlib.Order.Monotone.Defs

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

English

If x ≤ y iff f y ≤ f x, then f is StrictAnti.

Русский

Если x ≤ y ⇔ f y ≤ f x, то f строго антимонотонна.

LaTeX

$$[Preorder α] [Preorder β] {f : α → β} (h : ∀ x y, x ≤ y ↔ f y ≤ f x) → StrictAnti f$$

Lean4

protected theorem comp_antitoneOn (hg : Antitone g) (hf : AntitoneOn f s) : MonotoneOn (g ∘ f) s := fun _ ha _ hb h ↦
  hg (hf ha hb h)

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

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

Разделы

Аффилиация

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