SuppPos
DefinitionDiscreteConvex_EconomicEquilibriumB_SuppPosdiscrete-convex-analysis
The positive support for integer vectors.
(Murota, Discrete Convex Analysis, SIAM 2003, DOI 10.1137/1.9780898718508, p.133, redeclared.)
Definition code
import Mathlib
namespace DiscreteConvex.EconomicEquilibriumB
open Classical
open scoped Pointwise
variable {K : Type*} [Fintype K] [DecidableEq K]
/-- The positive support for integer vectors. -/
def SuppPos (x y : K → ℤ) : Finset K := Finset.univ.filter (fun v => y v < x v)
end DiscreteConvex.EconomicEquilibriumB
Source
Murota, Discrete Convex Analysis, SIAM 2003, DOI 10.1137/1.9780898718508, p.133, redeclared