Theorems · Theorem · global analysis

range_mvfderiv_subtypeVal

∀ {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)), (↑(d% Subtype.val v)).range = (ℝ ∙ ↑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. The range of this map is the orthogonal complement of v in E.

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