Antivary

Mathlib.Order.Monotone.Monovary

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

English

AntivaryOn on s is equivalent to Antivary on the restricted domain s.

Русский

AntivaryOn на s равносильна Antivary на ограниченной области s.

LaTeX

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

Lean4

/-- `f` antivaries with `g` if `g i < g j` implies `f j ≤ f i`. -/
def Antivary (f : ι → α) (g : ι → β) : Prop :=
  ∀ ⦃i j⦄, g i < g j → f j ≤ f i

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

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

Разделы

Аффилиация

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