English
Let f: E → F be a function between normed spaces, t ⊆ E, s ⊆ (E →L[𝕜] F) and x ∈ E. Then fderivWithin 𝕜 f t x ∈ s holds if and only if either f is differentiable within t at x and its derivative lies in s, or f is not differentiable within t at x and the zero operator lies in s.
Русский
Пусть f: E → F. Пусть t ⊆ E, s ⊆ (E →L[𝕜] F) и x ∈ E. Тогда fderivWithin 𝕜 f t x ∈ s тогда и только тогда, когда либо f дифференцируем внутри t в x и его производная лежит в s, либо f не дифференцируема внутри t в x и нулевой оператор принадлежит s.
LaTeX
$$$fderivWithin 𝕜 f t x ∈ s \iff \big( \text{DifferentiableWithinAt} 𝕜 f t x \land fderivWithin 𝕜 f t x ∈ s \big) \lor \big( \lnot \text{DifferentiableWithinAt} 𝕜 f t x \land (0 : E \toL[𝕜] F) ∈ s \big)$$$
Lean4
theorem fderivWithin_mem_iff {f : E → F} {t : Set E} {s : Set (E →L[𝕜] F)} {x : E} :
fderivWithin 𝕜 f t x ∈ s ↔
DifferentiableWithinAt 𝕜 f t x ∧ fderivWithin 𝕜 f t x ∈ s ∨
¬DifferentiableWithinAt 𝕜 f t x ∧ (0 : E →L[𝕜] F) ∈ s :=
by by_cases hx : DifferentiableWithinAt 𝕜 f t x <;> simp [fderivWithin_zero_of_not_differentiableWithinAt, *]
