English
If h is differentiableOn S and h(x) ≠ 0 for all x ∈ S, then the inverse-responsive function h^{-1} is differentiableOn S.
Русский
Если h дифференцируема на S и h(x) ≠ 0 для всех x ∈ S, то h^{-1} дифференцируема на S.
LaTeX
$$$\\text{DifferentiableOn}_{\\mathbb{K}}(h^{-1}, S)$$$
Lean4
theorem contDiffAt_norm_of_smul (h : ContDiffAt ℝ n (‖·‖) (t • x)) : ContDiffAt ℝ n (‖·‖) x :=
by
rcases eq_bot_or_bot_lt n with rfl | hn
· apply contDiffAt_zero.2
exact ⟨univ, univ_mem, continuous_norm.continuousOn⟩
replace hn : 1 ≤ n := ENat.add_one_natCast_le_withTop_of_lt hn
obtain rfl | ht := eq_or_ne t 0
· by_cases hE : Nontrivial E
· rw [zero_smul] at h
exact (mt (ContDiffAt.differentiableAt · (mod_cast hn))) (not_differentiableAt_norm_zero E) h |>.elim
· push_neg at hE
rw [eq_const_of_subsingleton (‖·‖) 0]
exact contDiffAt_const
· exact contDiffAt_norm_smul_iff ht |>.2 h
