Documentation

Mathlib.Geometry.Manifold.Instances.Icc

Manifold structure on real intervals #

The manifold structure on real intervals is defined in Mathlib.Geometry.Manifold.Instances.Real. We relate it to the manifold structure on the real line, by showing that the inclusion (contMDiff_subtypeVal_Icc) and projection (contMDiffOn_projIcc) are smooth, and showing that a function defined on the interval is smooth iff its composition with the projection is smooth on the interval in โ„ (see contMDiffOn_comp_projIcc_iff and friends).

We also define 1 : TangentSpace (๐“กโˆ‚ 1) z, and relate it to 1 in the real line.

TODO #

This file can be thoroughly rewritten once mathlib has a good theory of smooth submersions. Once this is done,

source
@[instance_reducible]
instance instOneTangentSpaceRealModelWithCornersSelf (x : โ„) :
One (TangentSpace (modelWithCornersSelf โ„ โ„) x)
Equations
source
theorem oneTangentSpaceIcc_def {x y : โ„} [h : Fact (x < y)] (z : โ†‘(Set.Icc x y)) :
oneTangentSpaceIcc z = (mfderiv[Set.Icc x y] (Set.projIcc x y โ‹ฏ) โ†‘z) 1
source
@[irreducible]
noncomputable def 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.

Equations
Instances For
    source
    @[instance_reducible]
    noncomputable instance instOneTangentSpaceRealEuclideanSpaceFinOfNatNatEuclideanHalfSpaceModelWithCornersEuclideanHalfSpaceElemIcc {x y : โ„} [h : Fact (x < y)] (z : โ†‘(Set.Icc x y)) :
    One (TangentSpace (modelWithCornersEuclideanHalfSpace 1) z)
    Equations
    source
    theorem isImmersionOfComplement_subtypeVal_Icc {x y : โ„} [h : Fact (x < y)] {n : WithTop โ„•โˆž} :
    Manifold.IsImmersionOfComplement Unit (modelWithCornersEuclideanHalfSpace 1) (modelWithCornersSelf โ„ โ„) n fun (z : โ†‘(Set.Icc x y)) => โ†‘z

    The inclusion map from a closed segment to โ„ is a smooth immersion

    source
    theorem isSmoothEmbedding_subtypeVal_Icc {x y : โ„} [h : Fact (x < y)] {n : WithTop โ„•โˆž} :
    Manifold.IsSmoothEmbedding (modelWithCornersEuclideanHalfSpace 1) (modelWithCornersSelf โ„ โ„) n fun (z : โ†‘(Set.Icc x y)) => โ†‘z

    The inclusion map from a closed segment to โ„ is a smooth embedding

    source
    theorem contMDiff_subtypeVal_Icc {x y : โ„} [h : Fact (x < y)] {n : WithTop โ„•โˆž} :
    ContMDiff (modelWithCornersEuclideanHalfSpace 1) (modelWithCornersSelf โ„ โ„) n fun (z : โ†‘(Set.Icc x y)) => โ†‘z

    The inclusion map from of a closed segment to โ„ is smooth in the manifold sense.

    source
    @[deprecated contMDiff_subtypeVal_Icc (since := "2026-07-22")]
    theorem contMDiff_subtype_coe_Icc {x y : โ„} [h : Fact (x < y)] {n : WithTop โ„•โˆž} :
    ContMDiff (modelWithCornersEuclideanHalfSpace 1) (modelWithCornersSelf โ„ โ„) n fun (z : โ†‘(Set.Icc x y)) => โ†‘z

    Alias of contMDiff_subtypeVal_Icc.

    The inclusion map from of a closed segment to โ„ is smooth in the manifold sense.

    source
    theorem contMDiff_iff_comp_subtypeVal_Icc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {x y : โ„} [h : Fact (x < y)] {n : WithTop โ„•โˆž} {f : M โ†’ โ†‘(Set.Icc x y)} :
    ContMDiff I (modelWithCornersEuclideanHalfSpace 1) n f โ†” Continuous f โˆง ContMDiff I (modelWithCornersSelf โ„ โ„) n ((fun (z : โ†‘(Set.Icc x y)) => โ†‘z) โˆ˜ f)

    A function f : M โ†’ Icc x y is smooth iff its composition with the inclusion into โ„ is smooth.

    source
    theorem contMDiffOn_projIcc {x y : โ„} [h : Fact (x < y)] {n : WithTop โ„•โˆž} :
    ContMDiffOn (modelWithCornersSelf โ„ โ„) (modelWithCornersEuclideanHalfSpace 1) n (Set.projIcc x y โ‹ฏ) (Set.Icc x y)

    The projection from โ„ to a closed segment is smooth on the segment, in the manifold sense.

    source
    theorem contMDiffOn_comp_projIcc_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {x y : โ„} [h : Fact (x < y)] {n : WithTop โ„•โˆž} {f : โ†‘(Set.Icc x y) โ†’ M} :
    ContMDiffOn (modelWithCornersSelf โ„ โ„) I n (f โˆ˜ Set.projIcc x y โ‹ฏ) (Set.Icc x y) โ†” ContMDiff (modelWithCornersEuclideanHalfSpace 1) I n f
    source
    theorem contMDiffWithinAt_comp_projIcc_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {x y : โ„} [h : Fact (x < y)] {n : WithTop โ„•โˆž} {f : โ†‘(Set.Icc x y) โ†’ M} {w : โ†‘(Set.Icc x y)} :
    ContMDiffWithinAt (modelWithCornersSelf โ„ โ„) I n (f โˆ˜ Set.projIcc x y โ‹ฏ) (Set.Icc x y) โ†‘w โ†” ContMDiffAt (modelWithCornersEuclideanHalfSpace 1) I n f w
    source
    theorem mdifferentiableWithinAt_comp_projIcc_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {x y : โ„} [h : Fact (x < y)] {f : โ†‘(Set.Icc x y) โ†’ M} {w : โ†‘(Set.Icc x y)} :
    MDiffAt[Set.Icc x y] (f โˆ˜ Set.projIcc x y โ‹ฏ) โ†‘w โ†” MDiffAt f w
    source
    theorem mfderivWithin_projIcc_one {x y : โ„} [h : Fact (x < y)] {z : โ„} (hz : z โˆˆ Set.Icc x y) :
    (mfderiv[Set.Icc x y] (Set.projIcc x y โ‹ฏ) z) 1 = 1
    source
    theorem mfderivWithin_comp_projIcc_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {x y : โ„} [h : Fact (x < y)] {f : โ†‘(Set.Icc x y) โ†’ M} {w : โ†‘(Set.Icc x y)} :
    (mfderiv[Set.Icc x y] (f โˆ˜ Set.projIcc x y โ‹ฏ) โ†‘w) 1 = (mfderiv% f w) 1
    source
    theorem mfderiv_subtypeVal_Icc_one {x y : โ„} [h : Fact (x < y)] (z : โ†‘(Set.Icc x y)) :
    (mfderiv% Subtype.val z) 1 = 1
    source
    @[deprecated mfderiv_subtypeVal_Icc_one (since := "2026-07-22")]
    theorem mfderiv_subtype_coe_Icc_one {x y : โ„} [h : Fact (x < y)] (z : โ†‘(Set.Icc x y)) :
    (mfderiv% Subtype.val z) 1 = 1

    Alias of mfderiv_subtypeVal_Icc_one.