A point of a convex set outside its relative interior lies in a face of smaller dimension

Proved

Plasticity.Aux.exists_proper_face

by scanstone · Oct 14, 2026 · Mathlib 0df444a (Lean v4.33.1)

Let $C$ be a convex subset of a real normed space whose affine hull is finite-dimensional, and let $x\in C$ lie outside the relative interior of $C$ . Then there is a convex extreme subset $C'$ of $C$ containing $x$ with $\dim\operatorname{span}(C'-C')<\dim\operatorname{span}(C-C)$ .

Preamble

import Mathlib.Analysis.Normed.Module.Basic
import Mathlib.Analysis.Convex.Extreme
import Mathlib.Analysis.Convex.Intrinsic
import Mathlib.LinearAlgebra.FiniteDimensional.Defs

Formal statement

namespace Plasticity.Aux
theorem exists_proper_face {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (C : Set E) (hconv : Convex ℝ C) (hfin : FiniteDimensional ℝ (vectorSpan ℝ C))
    (x : E) (hx : x ∈ C) (hxi : x ∉ intrinsicInterior ℝ C) :
    ∃ C' : Set E, C' ⊆ C ∧ Convex ℝ C' ∧ IsExtreme ℝ C C' ∧ x ∈ C' ∧
      Module.finrank ℝ (vectorSpan ℝ C') < Module.finrank ℝ (vectorSpan ℝ C) := by sorry
end Plasticity.Aux

Source

Supporting hyperplane theorem in the affine hull of C; e.g. R. T. Rockafellar, Convex Analysis (1970), Theorems 11.6 and 18.2

View graph