hasFDerivWithinAt_of_mem_nhds — Mathlib

English

If t ∈ 𝓝 x, then HasFDerivWithinAt f f' t x is equivalent to HasFDerivAt f f' x.

Русский

Если t принадлежит 𝓝 x, тогда HasFDerivWithinAt f f' t x эквивалентно HasFDerivAt f f' x.

LaTeX

$$$$\\text{Filter.mem}(\\,nhds\\ x\\, , t) \\Rightarrow (\\text{HasFDerivWithinAt } f f' t x \\iff \\text{HasFDerivAt } f f' x).$$$$

Lean4

theorem hasFDerivWithinAt_of_mem_nhds (h : s ∈ 𝓝 x) : HasFDerivWithinAt f f' s x ↔ HasFDerivAt f f' x := by
  rw [HasFDerivAt, HasFDerivWithinAt, nhdsWithin_eq_nhds.mpr h]

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