English
If f(g(y)) = y near a, and f has a zero derivative at g(a), then g cannot be differentiable at a along the set s.
Русский
Если f(g(y)) = y в окрестности a и производная f в g(a) равна нулю, то g не может быть дифференцируема в a на заданном множестве.
LaTeX
$$$ \\text{If } hf = \\mathrm{HasDerivAt} f 0 (g a) \\text{ and } f \\circ g = id \\text{ near } a, \\text{ then } \\neg \\mathrm{DifferentiableAt} g a $$$
Lean4
/-- If a function is equal to a constant at a set of points that accumulates to `x`,
then its derivative at `x` equals zero,
either because it has derivative zero or because it isn't differentiable at this point. -/
theorem deriv_zero_of_frequently_const {c} (h : ∃ᶠ y in 𝓝[≠] x, f y = c) : deriv f x = 0 :=
by
rw [← derivWithin_univ, derivWithin_zero_of_frequently_const]
rwa [← compl_eq_univ_diff]
