gfpApprox_antitone — Mathlib

English

The GFP approximation decreases as you move the index in the opposite order (antitone with respect to the underlying lattice dual).

Русский

Аппроксимация GFP убывает при переходе по индексу в противоположном порядке (антитонна к дуальной решётке).

LaTeX

$$$ \\text{Antitone}(\\mathrm{gfpApprox}\, f\, x) $$$

Lean4

theorem gfpApprox_antitone : Antitone (gfpApprox f x) :=
  lfpApprox_monotone f.dual x

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