Function subsmooth_function_ty 

pub fn subsmooth_function_ty() -> Expr

SubsmoothFunction : (List Real -> Real) -> Prop A subsmooth function: regular subdifferential equals limiting subdifferential everywhere.