English
If HasDerivWithinAt f f' s x, then the update map is continuous at x within s.
Русский
Если HasDerivWithinAt f f' s x, то отображение обновления непрерывно в x внутри s.
LaTeX
$$$\\mathrm{HasDerivWithinAt}(f,f',s,x) \\Rightarrow \\mathrm{ContinuousAt}(\\lambda x, (f x - f c)/(x - c)) x$$$
Lean4
/-- If a monotone function has a derivative within a set at a non-isolated point, then this
derivative is nonnegative. -/
theorem nonneg_of_monotoneOn (hx : AccPt x (𝓟 s)) (hd : HasDerivWithinAt g g' s x) (hg : MonotoneOn g s) : 0 ≤ g' :=
by
have : (𝓝[s \ { x }] x).NeBot := accPt_principal_iff_nhdsWithin.mp hx
have h'g : MonotoneOn g (insert x s) := hg.insert_of_continuousWithinAt hx.clusterPt hd.continuousWithinAt
have : Tendsto (slope g x) (𝓝[s \ { x }] x) (𝓝 g') := hasDerivWithinAt_iff_tendsto_slope.mp hd
apply ge_of_tendsto this
filter_upwards [self_mem_nhdsWithin] with y hy
simp only [mem_diff, mem_singleton_iff] at hy
rcases lt_or_gt_of_ne hy.2 with h'y | h'y
· simp only [slope, vsub_eq_sub, smul_eq_mul]
apply mul_nonneg_of_nonpos_of_nonpos
· simpa using h'y.le
· simpa using h'g (by simp [hy]) (by simp) h'y.le
· simp only [slope, vsub_eq_sub, smul_eq_mul]
apply mul_nonneg
· simpa using h'y.le
· simpa [sub_nonneg] using h'g (by simp) (by simp [hy]) h'y.le
