Appendix, p. 269 — the extreme points of a segment [a, b] with a < b are a and b

Proved

FlexCommitRO.BoxExt.extremePoints_Icc

by mikedeng1 · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

convexityextreme-pointsp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $a < b$ be real numbers. The set of extreme points of the segment $[a,b] \subset \mathbb R$ is its pair of endpoints:

\operatorname{ext}[a,b] = \{a, b\}.

In the Appendix this identifies $\operatorname{ext}(\mathcal U_t) = \{d_t^{\min}, d_t^{\max}\}$ , which is how the problem $(P_+)$ of Proposition 1 is written.

Preamble

import Mathlib

Formal statement

namespace FlexCommitRO.BoxExt

theorem extremePoints_Icc (a b : ℝ) (hab : a < b) :
    (Set.Icc a b).extremePoints ℝ = {a, b} := by sorry

end FlexCommitRO.BoxExt

Source

Ben-Tal, Golany, Nemirovski & Vial, Retailer-supplier flexible commitments contracts: a robust optimization approach, MSOM 7(3) (2005), p. 269, Appendix, first paragraph (ext(𝒰_t) = {d_t^min, d_t^max})

Human review

Endorsed by Shuze Chen · Oct 7, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph