English
Let E be a real inner product space. Then the natural inclusion of the unit sphere into E is an analytic map (in particular smooth of any finite differentiability class).
Русский
Пусть E – вещественное скалярное пространство с внутренним произведением. Тогда естественное включение единичной сферы в E является аналитической отображением (в частности гладким любой конечной степени).
LaTeX
$$$\mathrm{ContMDiff}_{\mathcal{R}^n}(\mathcal{I}(\mathbb{R},E))_{m}\big((\uparrow) : \mathrm{sphere}(0:E)\,1 \to E\big)$$$
Lean4
/-- The inclusion map (i.e., `coe`) from the sphere in `E` to `E` is analytic. -/
theorem contMDiff_coe_sphere {m : WithTop ℕ∞} {n : ℕ} [Fact (finrank ℝ E = n + 1)] :
ContMDiff (𝓡 n) 𝓘(ℝ, E) m ((↑) : sphere (0 : E) 1 → E) :=
by
rw [contMDiff_iff]
constructor
· exact continuous_subtype_val
· intro v _
let U : _ ≃ₗᵢ[ℝ] _ := (OrthonormalBasis.fromOrthogonalSpanSingleton n (ne_zero_of_mem_unit_sphere (-v))).repr
exact ((contDiff_stereoInvFunAux.comp (ℝ ∙ (-v : E))ᗮ.subtypeL.contDiff).comp U.symm.contDiff).contDiffOn
