English
Let E be a real inner product space and consider the univBall around c with radius r. The inverse map from the ball to the universal ball is C^n-differentiable on the ball of radius r around c; i.e., its restriction to ball(c, r) is of class C^n.
Русский
Пусть E — вещественное пространство с скалярным произведением. Рассматривается отображение univBall(c, r) и его обратное отображение. Обратное отображение ограничено на ball(c, r) и является отображением класса C^n.
LaTeX
$$$\big(\mathrm{univBall}(c,r)\big)^{-1} : \mathrm{ball}(c,r) \to \mathrm{univBall}(c,r) \quad \text{is of class } C^{n}.$$
Lean4
theorem contDiffOn_univBall_symm : ContDiffOn ℝ n (univBall c r).symm (ball c r) :=
by
unfold univBall; split_ifs with h
· refine contDiffOn_univUnitBall_symm.comp (contDiff_unitBallBall_symm h).contDiffOn ?_
rw [← unitBallBall_source c r h, ← unitBallBall_target c r h]
apply OpenPartialHomeomorph.symm_mapsTo
· exact contDiffOn_id.sub contDiffOn_const
