differentiableOn_add_const_iff — Mathlib

English

For any c, DifferentiableOn 𝕜 (f y + c) s iff DifferentiableOn 𝕜 f s.

Русский

Для любого c: DifferentiableOn 𝕜 (f y + c) s эквивалентно DifferentiableOn 𝕜 f s.

LaTeX

$$$\forall c,\ DifferentiableOn 𝕜 (f + c) s \iff DifferentiableOn 𝕜 f s.$$$

Lean4

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

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