TheoremsconcaveOn_univ_of_deriv, concaveOn_of_deriv, antitoneOn_deriv, antitoneOn_derivWithin, antitoneOn_slope_gt, antitoneOn_slope_lt, derivWithin_le_slope, deriv_le_slope, le_slope_of_hasDerivAt, le_slope_of_hasDerivWithinAt, le_slope_of_hasDerivWithinAt_Iio, leftDeriv_le_slope, slope_anti, slope_le_deriv, slope_le_derivWithin, slope_le_of_hasDerivAt, slope_le_of_hasDerivWithinAt, slope_le_of_hasDerivWithinAt_Ioi, slope_le_rightDeriv, derivWithin_le_slope, deriv_le_slope, differentiableWithinAt_Iio_of_mem_interior, differentiableWithinAt_Ioi_of_mem_interior, hasDerivWithinAt_leftDeriv_of_mem_interior, hasDerivWithinAt_rightDeriv_of_mem_interior, hasDerivWithinAt_sInf_slope_of_mem_interior, hasDerivWithinAt_sSup_slope_of_mem_interior, isMinOn_of_leftDeriv_eq_zero, isMinOn_of_leftDeriv_nonpos_of_rightDeriv_nonneg, isMinOn_of_rightDeriv_eq_zero, le_slope_of_hasDerivAt, le_slope_of_hasDerivWithinAt, le_slope_of_hasDerivWithinAt_Ioi, leftDeriv_eq_sSup_slope_of_mem_interior, leftDeriv_le_rightDeriv_of_mem_interior, monotoneOn_deriv, monotoneOn_derivWithin, monotoneOn_leftDeriv, monotoneOn_rightDeriv, monotoneOn_slope_gt, monotoneOn_slope_lt, rightDeriv_eq_sInf_slope_of_mem_interior, rightDeriv_le_slope, rightDeriv_le_slope_of_mem_interior, slope_le_deriv, slope_le_derivWithin, slope_le_leftDeriv, slope_le_leftDeriv_of_mem_interior, slope_le_of_hasDerivAt, slope_le_of_hasDerivWithinAt, slope_le_of_hasDerivWithinAt_Iio, slope_mono, convexOn_univ_of_deriv, convexOn_of_deriv, strictConcaveOn_univ_of_deriv, strictConcaveOn_of_deriv, derivWithin_lt_slope, deriv_lt_slope, leftDeriv_lt_slope, lt_slope_of_hasDerivAt, lt_slope_of_hasDerivWithinAt, lt_slope_of_hasDerivWithinAt_Iio, slope_lt_deriv, slope_lt_derivWithin, slope_lt_of_hasDerivAt, slope_lt_of_hasDerivWithinAt, slope_lt_of_hasDerivWithinAt_Ioi, slope_lt_rightDeriv, strictAntiOn_deriv, strictAntiOn_derivWithin, derivWithin_lt_slope, deriv_lt_slope, lt_slope_of_hasDerivAt, lt_slope_of_hasDerivWithinAt, lt_slope_of_hasDerivWithinAt_Ioi, rightDeriv_lt_slope, slope_lt_deriv, slope_lt_derivWithin, slope_lt_leftDeriv, slope_lt_of_hasDerivAt, slope_lt_of_hasDerivWithinAt, slope_lt_of_hasDerivWithinAt_Iio, strictMonoOn_deriv, strictMonoOn_derivWithin, strictConvexOn_univ_of_deriv, exists_deriv_lt_slope, exists_deriv_lt_slope_aux, exists_slope_lt_deriv, exists_slope_lt_deriv_aux, strictConvexOn_of_deriv, bddAbove_slope_gt_of_mem_interior, bddBelow_slope_lt_of_mem_interior, concaveOn_of_deriv2_nonpos, concaveOn_of_deriv2_nonpos', concaveOn_of_hasDerivWithinAt2_nonpos, concaveOn_univ_of_deriv2_nonpos, convexOn_of_deriv2_nonneg, convexOn_of_deriv2_nonneg', convexOn_of_hasDerivWithinAt2_nonneg, convexOn_univ_of_deriv2_nonneg, strictConcaveOn_of_deriv2_neg, strictConcaveOn_of_deriv2_neg', strictConcaveOn_univ_of_deriv2_neg, strictConvexOn_of_deriv2_pos, strictConvexOn_of_deriv2_pos', strictConvexOn_univ_of_deriv2_pos | 106 |