antivaryOn_iff_antivary

Mathlib.Order.Monotone.Monovary

URI: https://scilib.ai/kg/mathlib#antivaryOn_iff_antivary

English

AntivaryOn f g s is equivalent to Antivary (fun i : s ↦ f i) fun i ↦ g i.

Русский

AntivaryOn f g s эквивалентно Antivary (fun i : s ↦ f i) (fun i ↦ g i).

LaTeX

$$$AntivaryOn(f,g,s) \iff Antivary(\lambda i:s. f i) (\lambda i:s. g i)$$$

Lean4

theorem antivaryOn_iff_antivary : AntivaryOn f g s ↔ Antivary (fun i : s ↦ f i) fun i ↦ g i := by
  simp [Antivary, AntivaryOn]

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

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

Разделы

Аффилиация

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