contDiff_unitBallBall_symm — Mathlib

English

The inverse of the affine unit-ball map is C^n on its domain.

Русский

Обратная аффинному отображению единичного шара функция гладка класса C^n на области определения.

LaTeX

$$$\\text{ContDiff}_{\\mathbb{R}}^{n} (\\mathrm{unitBallBall}\\; c\\; r\\; \\mathrm hr).\\mathrm{symm}$$$

Lean4

theorem contDiff_unitBallBall_symm (hr : 0 < r) : ContDiff ℝ n (unitBallBall c r hr).symm :=
  (contDiff_id.sub contDiff_const).const_smul _

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