hasStrictFDerivAt_iff — Mathlib

English

If f0 and f1 are tangent in the nhds sense and f0' and f1' agree pointwise, then HasStrictFDerivAt f0 f0' x is equivalent to HasStrictFDerivAt f1 f1' x.

Русский

Если f0 и f1 имеют одинаковую производную в окрестности x и их производные согласованы по точкам, то их строгие производные эквивалентны.

LaTeX

$$$HasStrictFDerivAt f0 f0' x \\iff HasStrictFDerivAt f1 f1' x \\text{ когда } f0 =ₙₕ𝚍 x f1 и f0'(y) = f1'(y) для всех y$$$

Lean4

theorem hasStrictFDerivAt_iff (h : f₀ =ᶠ[𝓝 x] f₁) (h' : ∀ y, f₀' y = f₁' y) :
    HasStrictFDerivAt f₀ f₀' x ↔ HasStrictFDerivAt f₁ f₁' x :=
  by
  rw [hasStrictFDerivAt_iff_isLittleOTVS, hasStrictFDerivAt_iff_isLittleOTVS]
  refine isLittleOTVS_congr ((h.prodMk_nhds h).mono ?_) .rfl
  rintro p ⟨hp₁, hp₂⟩
  simp only [*]

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