theorem subdifferential_extended_indicator_eq_normal_cone {E : Type u} [AddCommGroup E] [Module ℝ E] (S : Set E) (x : E) : ∂δ_ S(x) = N[S](x)

Proposition 3.2: the subdifferential of the indicator function δ_S coincides with the normal cone of S at every point. In this bridge formulation, the textbook nonemptiness hypothesis on S is redundant because both sides are empty outside S.