English
For a set s of linear maps, fderiv 𝕜 f x belongs to s iff either f is differentiable at x and fderiv 𝕜 f x ∈ s or f is not differentiable at x and 0 ∈ s.
Русский
Для множества линейных отображений s: fderiv 𝕜 f x принадлежит s тогда и только тогда, когда либо f дифференцируема в x и fderiv 𝕜 f x ∈ s, либо f не дифференцируем в x и 0 ∈ s.
LaTeX
$$$fderiv 𝕜 f x \in s \iff \bigl(\text{DifferentiableAt } 𝕜 f x \land fderiv 𝕜 f x \in s\bigr) \lor \bigl(\lnot \text{DifferentiableAt } 𝕜 f x \land (0 : E \to L[𝕜] F) \in s\bigr)$$$
Lean4
theorem fderiv_mem_iff {f : E → F} {s : Set (E →L[𝕜] F)} {x : E} :
fderiv 𝕜 f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ (0 : E →L[𝕜] F) ∈ s := by
by_cases hx : DifferentiableAt 𝕜 f x <;> simp [fderiv_zero_of_not_differentiableAt, *]
