Theorems · Theorem · real analysis

isLocalMin_of_deriv_Ioo

∀ {f : ℝ → ℝ} {a b c : ℝ},
  a < b →
    b < c →
      ContinuousAt f b →
        DifferentiableOn ℝ f (Set.Ioo a b) →
          DifferentiableOn ℝ f (Set.Ioo b c) →
            (∀ x ∈ Set.Ioo a b, deriv f x ≤ 0) → (∀ x ∈ Set.Ioo b c, 0 ≤ deriv f x) → IsLocalMin f b

The First-Derivative Test from calculus, minima version.

Defined in: Mathlib.Analysis.Calculus.DerivativeTest
Cited by: 1 results in Mathlib
Foundations: Depth 193 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement · cited by 53,352
Realstatement and proof · cited by 25,697
Set.Ioostatement and proof · cited by 1,214
ContinuousAtstatement and proof · cited by 697
derivstatement and proof · cited by 676
DifferentiableOnstatement and proof · cited by 419
IsLocalMinstatement · cited by 45
Ioo_mem_nhdsproof · cited by 27
IsMinOn.isLocalMinproof · cited by 3
isMinOn_Ioo_of_derivproof · cited by 1

Cited by1

Results whose statement or proof uses this declaration.

isLocalMin_of_deriv'proof · cited by 1