IsLNaturalConvexPolyhedron
DefinitionDiscreteConvex_EconomicEquilibriumB_IsLNaturalConvexPolyhedrondiscrete-convex-analysisdiscrete-geometry
is an L-convex polyhedron.
(Murota, Discrete Convex Analysis, SIAM 2003, DOI 10.1137/1.9780898718508, p.131, axiom (SBS^\\natural[R]), Eq. (5.20), redeclared.)
Definition code
import Mathlib
namespace DiscreteConvex.EconomicEquilibriumB
open Classical
open scoped Pointwise
variable {K : Type*} [Fintype K] [DecidableEq K]
/-- `P ⊆ Rᴷ` is an L♮-convex polyhedron (axiom (SBS♮[R]), Eq. (5.20)). -/
def IsLNaturalConvexPolyhedron (P : Set (K → ℝ)) : Prop :=
∀ p ∈ P, ∀ q ∈ P, ∀ alpha : ℝ, 0 ≤ alpha →
(fun k => max (p k - alpha) (q k)) ∈ P ∧ (fun k => min (p k) (q k + alpha)) ∈ P
end DiscreteConvex.EconomicEquilibriumB
Source
Murota, Discrete Convex Analysis, SIAM 2003, DOI 10.1137/1.9780898718508, p.131, axiom (SBS^\\natural[R]), Eq. (5.20), redeclared