add_iff_left

Mathlib.Analysis.Calculus.FDeriv.Add

URI: https://scilib.ai/kg/mathlib#DifferentiableAt.add_iff_left

English

If hf : DifferentiableAt 𝕜 f x and hg : DifferentiableAt 𝕜 g x, then DifferentiableAt 𝕜 (f − g) x.

Русский

Если f и g дифференцируемы в точке x, то f − g дифференцируема в x.

LaTeX

$$DifferentiableAt 𝕜 (f − g) x$$

Lean4

@[simp]
theorem add_iff_left (hg : DifferentiableAt 𝕜 g x) : DifferentiableAt 𝕜 (f + g) x ↔ DifferentiableAt 𝕜 f x :=
  hg.fun_add_iff_left

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru