theorem Chapter10.derivative_of_monotone (X : Set ℝ) {x₀ : ℝ} (hx₀ : ClusterPt x₀ (Filter.principal (X \ {x₀}))) {f : ℝ → ℝ} (hmono : Monotone f) (hderiv : DifferentiableWithinAt ℝ f X x₀) : derivWithin f X x₀ ≥ 0

Proposition 10.3.1 / Exercise 10.3.1

theorem Chapter10.derivative_of_antitone (X : Set ℝ) {x₀ : ℝ} (hx₀ : ClusterPt x₀ (Filter.principal (X \ {x₀}))) {f : ℝ → ℝ} (hmono : Antitone f) (hderiv : DifferentiableWithinAt ℝ f X x₀) : derivWithin f X x₀ ≤ 0

theorem Chapter10.strictMono_of_positive_derivative {a b : ℝ} (hab : a < b) {f : ℝ → ℝ} (hderiv : DifferentiableOn ℝ f (Set.Icc a b)) (hpos : ∀ x ∈ Set.Ioo a b, derivWithin f (Set.Icc a b) x > 0) : StrictMonoOn f (Set.Icc a b)

Proposition 10.3.3 / Exercise 10.3.4

theorem Chapter10.strictAnti_of_negative_derivative {a b : ℝ} (hab : a < b) {f : ℝ → ℝ} (hderiv : DifferentiableOn ℝ f (Set.Icc a b)) (hneg : ∀ x ∈ Set.Ioo a b, derivWithin f (Set.Icc a b) x < 0) : StrictAntiOn f (Set.Icc a b)