differentiable_set_eq_D — Mathlib

English

If K is complete, then the set D(f,K) is contained in the set of differentiability points with derivative in K.

Русский

Если K полное, тогда D(f,K) ⊆ {x | DifferentiableWithinAt f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}.

LaTeX

$$D f K ⊆ \\{ x \\mid DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K \\}$$

Lean4

theorem differentiable_set_eq_D (hK : IsComplete K) :
    {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K} = D f K :=
  Subset.antisymm (differentiable_set_subset_D _) (D_subset_differentiable_set hK)

Похожие утверждения