English
If a differentiable map has a bound on its derivative, then near x, for z ≠ x, f(z) ≠ c for any constant c, except possibly at x itself.
Русский
Если производная ограничена, то в окрестности x рядом с x точки z ≠ x удовлетворяют f(z) ≠ c для любого константного c.
LaTeX
$$$$ \\forall z \\in 𝓝[x] \\setminus \\{x\\}, f(z) \\neq c $$$$
Lean4
theorem eventually_ne (h : HasFDerivWithinAt f f' s x) (hf' : ∃ C, ∀ z, ‖z‖ ≤ C * ‖f' z‖) :
∀ᶠ z in 𝓝[s \ { x }] x, f z ≠ c := by
rcases eq_or_ne (f x) c with rfl | hc
· rw [nhdsWithin, diff_eq, ← inf_principal, ← inf_assoc, eventually_inf_principal]
have A : (fun z => z - x) =O[𝓝[s] x] fun z => f' (z - x) :=
isBigO_iff.2 <| hf'.imp fun C hC => Eventually.of_forall fun z => hC _
have : (fun z => f z - f x) ~[𝓝[s] x] fun z => f' (z - x) := h.isLittleO.trans_isBigO A
simpa [not_imp_not, sub_eq_zero] using (A.trans this.isBigO_symm).eq_zero_imp
· exact (h.continuousWithinAt.eventually_ne hc).filter_mono <| by gcongr; apply diff_subset
