theorem
isExposedDirection_recessionCone_of_isExposedDirection
{n : ℕ}
(C : Set (EuclideanSpace ℝ (Fin n)))
(hCclosed : IsClosed C)
{d : EuclideanSpace ℝ (Fin n)}
(hd : IsExposedDirection C d)
:
Text 18.0.14 (exposed directions). If d is an exposed direction of a closed convex set C,
then d is an exposed direction of the recession cone 0⁺ C (formalized as Set.recessionCone C).
theorem
exists_isExposedDirection_recessionCone_not_isExposedDirection :
∃ (C : Set (EuclideanSpace ℝ (Fin 2))) (d : EuclideanSpace ℝ (Fin 2)),
IsClosed C ∧ Convex ℝ C ∧ IsExposedDirection C.recessionCone d ∧ ¬IsExposedDirection C d
Text 18.0.14 (converse fails for exposed directions). There exists a closed convex set C and a
vector d such that d is an exposed direction of 0⁺ C but not an exposed direction of C.