Theorems · Theorem · real analysis

domain_mvt

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {x y : E}
  {f' : E → StrongDual ℝ E},
  (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
    Convex ℝ s → x ∈ s → y ∈ s → ∃ z ∈ segment ℝ x y, f y - f x = (f' z) (y - x)

Lagrange's Mean Value Theorem, applied to convex domains.

Defined in

Mathlib.Analysis.Calculus.Deriv.MeanValue

Cited by

0 results in Mathlib

Foundations

Depth 188 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace