theorem chapter11Exercise112_eq_nearestPoint_of_mem_of_isMinOn {p : EuclideanSpace ℝ (Fin 3)} (hp : p ∈ exercise89FeasibleSet) (hmin : IsMinOn exercise89SquaredDistanceToOrigin exercise89FeasibleSet p) : p = exercise89NearestPoint

Any feasible minimizer of the squared distance to the origin on the Exercise 11.2 ellipse is the explicit point exercise89NearestPoint = (1 / 3, 2 / 3, 0). The feasibility hypothesis is essential because IsMinOn alone does not imply membership in exercise89FeasibleSet.