theorem normalCone_ell2PositiveOrthant_eq_setOf_nonpos_mul_eq_zero {I : Type u} {x : ↥(lp (fun (x : I) => ℝ) 2)} (hx : x ∈ {ξ : ↥(lp (fun (x : I) => ℝ) 2) | ∀ (i : I), 0 ≤ ↑ξ i}) : {ξ : ↥(lp (fun (x : I) => ℝ) 2) | ∀ (i : I), 0 ≤ ↑ξ i}.normalCone x = {v : ↥(lp (fun (x : I) => ℝ) 2) | ∀ (i : I), ↑v i ≤ 0 ∧ ↑x i * ↑v i = 0}

Example 6.41: at a point x of the positive orthant in ℓ²(I), the normal cone consists exactly of the vectors with nonpositive coordinates that satisfy the complementary-slackness relations x i * v i = 0 coordinatewise.