not_differentiableWithinAt_of_local_left_inverse_hasDerivWithinAt_zero

English

Under the same hypotheses as the previous, differentiability of g at a is contradicted.

Русский

При тех же предпосылках предыдущее утверждение противоречит существованию дифференцируемости g в точке a.

LaTeX

$$$ \\text{If } hf = \\mathrm{HasDerivAt} f 0 (g a) \\text{ and } hfg : f \\circ g = id \\text{ near } a, \\text{ then } \\neg \\mathrm{DifferentiableAt} g a $$$

Lean4

theorem not_differentiableWithinAt_of_local_left_inverse_hasDerivWithinAt_zero {f g : 𝕜 → 𝕜} {a : 𝕜} {s t : Set 𝕜}
    (ha : a ∈ s) (hsu : UniqueDiffWithinAt 𝕜 s a) (hf : HasDerivWithinAt f 0 t (g a)) (hst : MapsTo g s t)
    (hfg : f ∘ g =ᶠ[𝓝[s] a] id) : ¬DifferentiableWithinAt 𝕜 g s a :=
  by
  intro hg
  have := (hf.comp a hg.hasDerivWithinAt hst).congr_of_eventuallyEq_of_mem hfg.symm ha
  simpa using hsu.eq_deriv _ this (hasDerivWithinAt_id _ _)

Похожие утверждения