structure SubgradientSelection {E : Type u} [AddCommGroup E] [Module ℝ E] (f : E → EReal) (C : Set E) : Type u

Definition 8.7: a subgradient selection for f on C is a deterministic rule assigning to each x ∈ C a chosen subgradient f'(x) ∈ ∂ f(x), that is, a function C → E* whose value at every feasible point belongs to the subdifferential of f at that point.

• toFun : ↑C → Module.Dual ℝ E
• mem_subdifferential (x : ↑C) : self.toFun x ∈ ∂f(↑x)

@[implicit_reducible]

instance instCoeFunSubgradientSelectionForallElemDualReal {E : Type u} [AddCommGroup E] [Module ℝ E] {f : E → EReal} {C : Set E} : CoeFun (SubgradientSelection f C) fun (x : SubgradientSelection f C) => ↑C → Module.Dual ℝ E

A subgradient selection is canonically used as the underlying function C → E*.