isSymmSndFDerivWithinAt_congr_set

English

If h holds for s and s and t are equivalent near x, then h holds for t.

Русский

Если свойство справедливо на s, а s эквивалентно t близко к x, тогда свойство справедливо и на t.

LaTeX

$$$IsSymmSndFDerivWithinAt 𝕜 f s x \\Rightarrow (nhds x).EventuallyEq s t \\Rightarrow IsSymmSndFDerivWithinAt 𝕜 f t x$$$

Lean4

theorem isSymmSndFDerivWithinAt_congr_set (hst : s =ᶠ[𝓝 x] t) :
    IsSymmSndFDerivWithinAt 𝕜 f s x ↔ IsSymmSndFDerivWithinAt 𝕜 f t x :=
  ⟨fun h ↦ h.congr_set hst, fun h ↦ h.congr_set hst.symm⟩

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