NegGS

import Mathlib
import Definitions.Def_DiscreteConvex_EconomicEquilibriumB_ArgMaxBot
import Definitions.Def_DiscreteConvex_EconomicEquilibriumB_PriceShiftGen

namespace DiscreteConvex.EconomicEquilibriumB

open Classical
open scoped Pointwise
variable {K : Type*} [Fintype K] [DecidableEq K]
/-- Axiom (−M♮-GS[Z]) (a version of the gross substitutes property). -/
def NegGS (U : (K → ℤ) → WithBot ℝ) : Prop :=
  ∀ p q : K → ℝ, ∀ p0 q0 : ℝ, (∀ k, p k ≤ q k) → p0 ≤ q0 →
    ∀ x : K → ℤ, x ∈ ArgMaxBot (PriceShiftGen U p p0) →
    (ArgMaxBot (PriceShiftGen U q q0)).Nonempty →
    ∃ y : K → ℤ, y ∈ ArgMaxBot (PriceShiftGen U q q0) ∧
      (∀ i : K, p i = q i → x i ≤ y i) ∧ (p0 = q0 → (∑ k, y k) ≤ ∑ k, x k)

end DiscreteConvex.EconomicEquilibriumB