differentiableOn_dslope_of_notMem

English

If a ∉ s, then differentiability of dslope f a on s is equivalent to differentiability of f on s.

Русский

Если a ∉ s, то dslope f a на s дифференцируемо тогда и только тогда, когда f на s дифференцируемо.

LaTeX

$$(a ∉ s) → (DifferentiableOn 𝕜 (dslope f a) s ↔ DifferentiableOn 𝕜 f s)$$

Lean4

theorem differentiableOn_dslope_of_notMem (h : a ∉ s) : DifferentiableOn 𝕜 (dslope f a) s ↔ DifferentiableOn 𝕜 f s :=
  forall_congr' fun _ => forall_congr' fun hx => differentiableWithinAt_dslope_of_ne <| ne_of_mem_of_not_mem hx h

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