differentiableOn_const_add_iff — Mathlib

English

For every constant c ∈ F, the function y ↦ c + f(y) is differentiable on s if and only if f is differentiable on s.

Русский

Для каждого константы c ∈ F функция y ↦ c + f(y) дифференцируема на s тогда и только тогда, когда f дифференцируема на s.

LaTeX

$$$\operatorname{DifferentiableOn}_{\mathbb{k}}\left(\lambda y. c + f(y)\right)\ s \iff \operatorname{DifferentiableOn}_{\mathbb{k}}\left(f\right)\ s$$$

Lean4

@[simp]
theorem differentiableOn_const_add_iff (c : F) : DifferentiableOn 𝕜 (fun y => c + f y) s ↔ DifferentiableOn 𝕜 f s :=
  forall₂_congr fun _ _ ↦ differentiableWithinAt_const_add_iff c

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