deriv_mem_iff — Mathlib

English

The differentiability within Ioi x is equivalent to differentiability within Ici x for a module over the reals.

Русский

Дифференцируемость внутри Ioi x эквивалентна внутри Ici x для модуля над ℝ.

LaTeX

$$$$ \\text{DifferentiableWithinAt } 𝕜 f (Ioi x) x \\iff \\text{DifferentiableWithinAt } 𝕜 f (Ici x) x $$$$

Lean4

theorem deriv_mem_iff {f : 𝕜 → F} {s : Set F} {x : 𝕜} :
    deriv f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ deriv f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ (0 : F) ∈ s := by
  by_cases hx : DifferentiableAt 𝕜 f x <;> simp [deriv_zero_of_not_differentiableAt, *]

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