Theorems · Theorem · real analysis

IsExtrOn.hasLineDerivAt_eq_zero

∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {f : E → ℝ} {s : Set E} {a b : E} {f' : ℝ},
  IsExtrOn f s a → HasLineDerivAt ℝ f f' a b → (∀ᶠ (t : ℝ) in nhds 0, a + t • b ∈ s) → f' = 0

Defined in

Mathlib.Analysis.Calculus.LocalExtr.LineDeriv

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddCommGroupModule