English
If a is a limit point of s, then dslope f a is continuous on s if and only if f is continuous on s and f is differentiable at a.
Русский
Пусть a — предел области s. Тогда dslope f a непрерывна на s тогда и только тогда, когда f непрерывна на s и дифференцируема в a.
LaTeX
$$$\text{ContinuousOn}( dslope\ f\ a, s) \iff \bigl( \text{ContinuousOn}( f, s) \wedge \text{DifferentiableAt}( f, a) \bigr), \; \text{при } s \in \mathcal{N}(a)$$$
Lean4
theorem continuousOn_dslope (h : s ∈ 𝓝 a) : ContinuousOn (dslope f a) s ↔ ContinuousOn f s ∧ DifferentiableAt 𝕜 f a :=
by
refine ⟨fun hc => ⟨hc.of_dslope, continuousAt_dslope_same.1 <| hc.continuousAt h⟩, ?_⟩
rintro ⟨hc, hd⟩ x hx
rcases eq_or_ne x a with (rfl | hne)
exacts [(continuousAt_dslope_same.2 hd).continuousWithinAt, (continuousWithinAt_dslope_of_ne hne).2 (hc x hx)]
