theorem section16_supportFunctionEReal_preimage_eq_adjoint_image_of_exists_mem_ri {n m : ℕ} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) (D : Set (Fin m → ℝ)) (hD : Convex ℝ D) (hri : ∃ (x : EuclideanSpace ℝ (Fin n)), A x ∈ euclideanRelativeInterior m ((fun (z : EuclideanSpace ℝ (Fin m)) => z.ofLp) ⁻¹' D)) : have Aadj := LinearMap.adjoint A; (supportFunctionEReal ((fun (x : Fin n → ℝ) => (A (WithLp.toLp 2 x)).ofLp) ⁻¹' D) = fun (xStar : Fin n → ℝ) => sInf ((fun (yStar : EuclideanSpace ℝ (Fin m)) => supportFunctionEReal D yStar.ofLp) '' {yStar : EuclideanSpace ℝ (Fin m) | Aadj yStar = WithLp.toLp 2 xStar})) ∧ ∀ (xStar : Fin n → ℝ), sInf ((fun (yStar : EuclideanSpace ℝ (Fin m)) => supportFunctionEReal D yStar.ofLp) '' {yStar : EuclideanSpace ℝ (Fin m) | Aadj yStar = WithLp.toLp 2 xStar}) = ⊤ ∨ ∃ (yStar : EuclideanSpace ℝ (Fin m)), Aadj yStar = WithLp.toLp 2 xStar ∧ supportFunctionEReal D yStar.ofLp = sInf ((fun (yStar : EuclideanSpace ℝ (Fin m)) => supportFunctionEReal D yStar.ofLp) '' {yStar : EuclideanSpace ℝ (Fin m) | Aadj yStar = WithLp.toLp 2 xStar})

Corollary 16.3.1.3: Let A : ℝ^n →ₗ[ℝ] ℝ^m be a linear map and let D ⊆ ℝ^m be convex. If there exists x such that A x ∈ ri D, then the closure on D can be omitted in Corollary 16.3.1.2. Equivalently, for every xStar,

δ^*(xStar | A⁻¹ D) = inf { δ^*(yStar | D) | A^* yStar = xStar },

and the infimum is attained (or the value is +∞ if the affine fiber is empty).