English
Characterizes when derivWithin f t x lies in a set s, in terms of differentiability at x and whether the derivative lies in s or the zero vector lies in s.
Русский
Характеризация того, когда derivWithin f t x лежит в множестве s, через дифференцируемость и принадлежность производной или нуля в s.
LaTeX
$$$$ \\ derivWithin f t x ∈ s \\iff ( \\text{DifferentiableWithinAt } 𝕜 f t x ∧ derivWithin f t x ∈ s) ∨ (¬\\text{DifferentiableWithinAt } 𝕜 f t x ∧ 0 ∈ s) $$$$
Lean4
theorem derivWithin_mem_iff {f : 𝕜 → F} {t : Set 𝕜} {s : Set F} {x : 𝕜} :
derivWithin f t x ∈ s ↔
DifferentiableWithinAt 𝕜 f t x ∧ derivWithin f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ (0 : F) ∈ s :=
by by_cases hx : DifferentiableWithinAt 𝕜 f t x <;> simp [derivWithin_zero_of_not_differentiableWithinAt, *]
