hasFDerivWithinAt_congr_set — Mathlib

English

If y-neighborhoods of x reflect s and t, then HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x.

Русский

Если окрестности x отражают s и t, то производная внутри согласуется.

LaTeX

$$$HasFDerivWithinAt f f' s x \\iff HasFDerivWithinAt f f' t x \\text{ when } s=ᶠ_{𝓝 x} t.$$$

Lean4

theorem hasFDerivWithinAt_congr_set (h : s =ᶠ[𝓝 x] t) : HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x :=
  hasFDerivWithinAt_congr_set' x <| h.filter_mono inf_le_left

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