Theorems · Definition · global analysis

oneTangentSpaceIcc

{x y : ℝ} → [h : Fact (x < y)] → (z : ↑(Set.Icc x y)) → TangentSpace (modelWithCornersEuclideanHalfSpace 1) z

Unit vector in the tangent space to a segment, as the image of the unit vector in the real line under the canonical projection. It is also mapped to the unit vector in the real line through the canonical injection, see mfderiv_subtypeVal_Icc_one. Note that one cannot abuse defeqs for this definition: this is not the same as the vector fun _ ↦ 1 in EuclideanSpace ℝ (Fin 1) through defeqs, as one of the charts of Icc x y is orientation-reversing.

Defined in

Mathlib.Geometry.Manifold.Instances.Icc

Cited by

1 results in Mathlib

Foundations

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

Assumes

Fact