theorem subdifferential_setIndicator_eq_normalCone {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (C : Set H) (hC_nonempty : C.Nonempty) : ERealFunction.subdifferential ι[C] = C.normalCone

Example 16.13: for a nonempty subset C of a real Hilbert space, hence in particular for a nonempty convex subset, the subdifferential of the indicator ι_C is exactly the normal cone mapping N_C.