def subdifferential_domain {E : Type u} [AddCommGroup E] [Module ℝ E] (f : E → EReal) : Set E

Definition 3.6: the domain of the subdifferential dom(∂ f) is the set of points where the extended-real-valued function f is subdifferentiable, equivalently where ∂ f(x) is nonempty.

@[simp]

theorem mem_subdifferential_domain {E : Type u} [AddCommGroup E] [Module ℝ E] {f : E → EReal} {x : E} : x ∈ subdifferential_domain f ↔ ∂f(x).Nonempty

Membership in dom(∂ f) means that the subdifferential at the point is nonempty.

theorem subdifferential_domain_subset_effective_domain {E : Type u} [AddCommGroup E] [Module ℝ E] {f : E → EReal} : subdifferential_domain f ⊆ effective_domain f

Every point in the domain of the subdifferential belongs to the effective domain.