theorem prox_extendedIndicator_eq_singleton_metricProjection {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (C : Set E) (hC_nonempty : C.Nonempty) (hC_closed : IsClosed C) (hC_convex : Convex ℝ C) (x : E) : prox[δ_ C] x = {projectionPoint C hC_nonempty hC_closed hC_convex x}

For a nonempty closed convex set, the proximal mapping of the indicator δ_C is the singleton containing the metric projection P_C(x).