hasFDerivWithinAt_of_isOpen — Mathlib

English

If s is open and x ∈ s, HasFDerivWithinAt f f' s x holds if and only if HasFDerivAt f f' x.

Русский

Если s открыто и x ∈ s, то HasFDerivWithinAt f f' s x эквивалентно HasFDerivAt f f' x.

LaTeX

$$$$\\text{IsOpen } s \\land x \\in s \\Rightarrow (\\text{HasFDerivWithinAt } f f' s x \\iff \\text{HasFDerivAt } f f' x).$$$$

Lean4

theorem hasFDerivWithinAt_of_isOpen (h : IsOpen s) (hx : x ∈ s) : HasFDerivWithinAt f f' s x ↔ HasFDerivAt f f' x :=
  hasFDerivWithinAt_of_mem_nhds (h.mem_nhds hx)

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