Prove2Me

Theorem 4.3 -- the four exchange axiom variants are equivalent

Proved
DiscreteConvex.MConvexSets.exchange_axioms_equivalent

by Shuze Chen · 1 vote · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsdiscrete-convex-analysis

Theorem 4.3 (p.103). Conditions (B-EXC[Z]), (B-EXCw[Z]), (B-EXC+[Z]), and (B-EXC-[Z]) are equivalent for a set B⊆ZVB \subseteq \mathbb Z^V.

(Murota, Discrete Convex Analysis, SIAM 2003, DOI 10.1137/1.9780898718508, p.103, Theorem 4.3.)

Preamble
import Mathlib
import Definitions.Def_DiscreteConvex_MConvexSets_ExchangeAxiomB
import Definitions.Def_DiscreteConvex_MConvexSets_ExchangeAxiomBWeak
import Definitions.Def_DiscreteConvex_MConvexSets_ExchangeAxiomBPlus
import Definitions.Def_DiscreteConvex_MConvexSets_ExchangeAxiomBMinus
Formal statement
namespace DiscreteConvex.MConvexSets

/-- Theorem 4.3 (Murota, *Discrete Convex Analysis*, SIAM 2003, p.103). Conditions
`(B-EXC[Z])`, `(B-EXCw[Z])`, `(B-EXC+[Z])`, and `(B-EXC-[Z])` are equivalent for a set
`B ⊆ Zⱽ`. -/
theorem exchange_axioms_equivalent {V : Type*} [Fintype V] [DecidableEq V] (B : Set (V → ℤ)) :
    [ExchangeAxiomB B, ExchangeAxiomBWeak B, ExchangeAxiomBPlus B, ExchangeAxiomBMinus B].TFAE := by sorry

end DiscreteConvex.MConvexSets
Source
Murota, Discrete Convex Analysis, SIAM 2003, DOI 10.1137/1.9780898718508, p.103, Theorem 4.3
Human review

  • Endorsed by Community (Bot) · Oct 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Shuze Chen · Oct 1, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph