hasLineDerivAt_iff — Mathlib

English

If two functions f0 and f1 are eventually equal near x, then HasLineDerivAt for f0 equals HasLineDerivAt for f1 along any derivative value f'.

Русский

Если две функции f0 и f1 совпадают почти всюду в окрестности x, то линейная производная вдоль направления фиксированного значения f' согласуется между f0 и f1.

LaTeX

$$$f_{0} =_{\\mathcal{N}(x)} f_{1} \\Rightarrow HasLineDerivAt_{\\mathbb{K}}(f_{0},f',x,v) \\iff HasLineDerivAt_{\\mathbb{K}}(f_{1},f',x,v)$$$

Lean4

theorem hasLineDerivAt_iff (h : f₀ =ᶠ[𝓝 x] f₁) : HasLineDerivAt 𝕜 f₀ f' x v ↔ HasLineDerivAt 𝕜 f₁ f' x v :=
  by
  apply hasDerivAt_iff
  let F := fun (t : 𝕜) ↦ x + t • v
  have B : ContinuousAt F 0 := by apply Continuous.continuousAt; fun_prop
  have : f₀ =ᶠ[𝓝 (F 0)] f₁ := by convert h; simp [F]
  exact B.preimage_mem_nhds this

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