English
Let I be an index set, and f: I → α, g: I → β be functions into a ordered ring α and an ordered module β over α. Antivary f g expresses that increases of f correspond to decreases of g (in the sense of the α–β action). Precisely, Antivary f g holds if and only if for all i, j in I the smoothed product (f j − f i) • (g j − g i) is ≤ 0.
Русский
Пусть i, j пронумерованы во множестве индексов I, функции f: I → α и g: I → β, где α — упорядоченное кольцо, β — упорядоченная аддитивная grupa с модулем над α. Антивариация означает, что приросты f и g противоположны по знаку в смысле действия α над β: для любых i, j ∈ I выполняется (f j − f i) • (g j − g i) ≤ 0.
LaTeX
$$$Antivary f g \\iff \\forall i j, (f j - f i) \\;\\bullet\\; (g j - g i) \\le 0$$$
Lean4
theorem antivary_iff_forall_smul_nonpos : Antivary f g ↔ ∀ i j, (f j - f i) • (g j - g i) ≤ 0 :=
monovary_toDual_right.symm.trans <| by rw [monovary_iff_forall_smul_nonneg]; rfl
