lineDifferentiableAt_iff — Mathlib

English

If f0 and f1 are eventually equal on a neighborhood of x and f0(x)=f1(x), then LineDifferentiableWithinAt for f0 equals that for f1 on s, x, v.

Русский

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

LaTeX

$$$f_{0} =_{\\mathcal{N}(x)[s]} f_{1} \\land f_{0}(x)=f_{1}(x) \\Rightarrow \\mathrm{LineDifferentiableWithinAt}_{\\mathbb{K}}(f_{0};s;x,v) \\iff \\mathrm{LineDifferentiableWithinAt}_{\\mathbb{K}}(f_{1};s;x,v)$$$

Lean4

theorem lineDifferentiableAt_iff (h : f₀ =ᶠ[𝓝 x] f₁) : LineDifferentiableAt 𝕜 f₀ x v ↔ LineDifferentiableAt 𝕜 f₁ x v :=
  ⟨fun h' ↦ (h.hasLineDerivAt_iff.1 h'.hasLineDerivAt).lineDifferentiableAt, fun h' ↦
    (h.hasLineDerivAt_iff.2 h'.hasLineDerivAt).lineDifferentiableAt⟩

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