English
If f is an open partial homeomorphism with nonzero strict derivative f' at a point on its inverse, then the inverse has derivative f'^{-1} at the corresponding point.
Русский
Если f является открытым частичным гомоморфизмом и имеет строгую производную f' не равную нулю в точке соответствующей обратной карты, тогда обратная карта имеет производную f'^{-1}.
LaTeX
$$$ (f \\text{ open partial homeomorph}) \\land (f' \\neq 0) \\Rightarrow \\mathrm{HasStrictDerivAt} (f^{-1}) {f'^{-1}} $$$
Lean4
/-- If a function is equal to a constant at a set of points that accumulates to `x` in `s`,
then its derivative within `s` at `x` equals zero,
either because it has derivative zero or because it isn't differentiable at this point. -/
theorem derivWithin_zero_of_frequently_const {c} (h : ∃ᶠ y in 𝓝[s \ { x }] x, f y = c) : derivWithin f s x = 0 :=
by
by_cases hf : DifferentiableWithinAt 𝕜 f s x
· contrapose h
rw [not_frequently]
exact hf.hasDerivWithinAt.eventually_ne h
· exact derivWithin_zero_of_not_differentiableWithinAt hf
