Theorems · Theorem · global analysis

injective_mvfderiv_subtypeVal_sphere

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
  [inst_2 : Fact (Module.finrank ℝ E = n + 1)] (v : ↑(Metric.sphere 0 1)), Function.Injective ⇑(d% Subtype.val v)

Consider the differential of the inclusion of the sphere in E at the point v as a continuous linear map from TangentSpace (𝓡 n) v to E. This map is injective.

Defined in

Mathlib.Geometry.Manifold.Instances.Sphere

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceFact