theorem ERealFunction.inequalityMultiplier_eq_zero_of_strictlyInactiveConstraint {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {m p : ℕ} (f : H → ↑(Set.Ioi ⊥)) (g : Fin p → H → ℝ) (u : Fin (m - p) → H) (ρ : Fin (m - p) → ℝ) (hdom : (effectiveDomain f).Nonempty) {xbar : H} {νbar : EuclideanSpace ℝ (Fin p ⊕ Fin (m - p))} (hsaddle : IsSaddlePointOn Set.univ Set.univ ℒ[mixedConstraintPerturbation f g u ρ] xbar νbar) (i : Fin p) (hstrict : g i xbar < 0) : νbar.ofLp (Sum.inl i) = 0

Remark 19.31: in Corollary 19.30, the inequality-block coordinates of a saddle-point parameter vector are the Lagrange multipliers associated with the primal solution, they satisfy complementary slackness, and if dom f is nonempty then any strictly inactive inequality constraint has zero multiplier.