Theorems · Theorem · measure theory

RightDerivMeasurableAux.D_subset_differentiable_set

∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {f : ℝ → F} {K : Set F},
  IsComplete K →
    RightDerivMeasurableAux.D f K ⊆ {x | DifferentiableWithinAt ℝ f (Set.Ici x) x ∧ derivWithin f (Set.Ici x) x ∈ K}

Harder inclusion: at a point in D f K, the function f has a derivative, in K.

Defined in

Mathlib.Analysis.Calculus.FDeriv.Measurable

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace