contMDiff_neg_sphere — Mathlib

English

The antipodal map on the unit sphere in E is analytic (C^n for all n).

Русский

Антиподальное отображение на единичной сфере в E аналитично (гладко любого конечного порядка).

LaTeX

$$The map $x\mapsto -x$ on $\mathrm{sphere}(0:E)1$ is ContMDiff of class $(\mathcal{R}n)$ to itself.$$

Lean4

/-- The antipodal map is analytic. -/
theorem contMDiff_neg_sphere {m : WithTop ℕ∞} {n : ℕ} [Fact (finrank ℝ E = n + 1)] :
    ContMDiff (𝓡 n) (𝓡 n) m fun x : sphere (0 : E) 1 => -x := by
  -- this doesn't elaborate well in term mode

  apply ContMDiff.codRestrict_sphere
  apply contDiff_neg.contMDiff.comp _
  exact contMDiff_coe_sphere

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