Theorems · Theorem · global analysis

contMDiff_neg_sphere

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {m : WithTop ℕ∞} {n : ℕ}
  [inst_2 : Fact (Module.finrank ℝ E = n + 1)],
  ContMDiff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) m
    fun x => -x

The antipodal map is analytic.

Defined in

Mathlib.Geometry.Manifold.Instances.Sphere

Cited by

0 results in Mathlib

Foundations

Depth 248 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceFact