Documentation

Mathlib.Geometry.Manifold.ContMDiffMap

Smooth bundled map #

In this file we define the type ContMDiffMap of n times continuously differentiable bundled maps.

def ContMDiffMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] (I : ModelWithCorners 𝕜 E H) (I' : ModelWithCorners 𝕜 E' H') (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] (M' : Type u_7) [TopologicalSpace M'] [ChartedSpace H' M'] (n : ℕ∞) :
Type (max 0 u_6 u_7)

Bundled n times continuously differentiable maps.

Instances For
    @[reducible]
    def SmoothMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] (I : ModelWithCorners 𝕜 E H) (I' : ModelWithCorners 𝕜 E' H') (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] (M' : Type u_7) [TopologicalSpace M'] [ChartedSpace H' M'] :
    Type (max 0 u_6 u_7)

    Bundled smooth maps.

    Instances For
      instance ContMDiffMap.funLike {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} :
      FunLike (ContMDiffMap I I' M M' n) M fun x => M'
      theorem ContMDiffMap.contMDiff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (f : ContMDiffMap I I' M M' n) :
      ContMDiff I I' n f
      theorem ContMDiffMap.smooth {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] (f : ContMDiffMap I I' M M' ) :
      Smooth I I' f
      @[simp]
      theorem ContMDiffMap.coeFn_mk {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (f : MM') (hf : ContMDiff I I' n f) :
      { val := f, property := hf } = f
      theorem ContMDiffMap.coe_injective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} ⦃f : ContMDiffMap I I' M M' n ⦃g : ContMDiffMap I I' M M' n (h : f = g) :
      f = g
      theorem ContMDiffMap.ext {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} {f : ContMDiffMap I I' M M' n} {g : ContMDiffMap I I' M M' n} (h : ∀ (x : M), f x = g x) :
      f = g
      instance ContMDiffMap.instContinuousMapClassContMDiffMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} :
      ContinuousMapClass (ContMDiffMap I I' M M' n) M M'
      def ContMDiffMap.id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {n : ℕ∞} :
      ContMDiffMap I I M M n

      The identity as a smooth map.

      Instances For
        def ContMDiffMap.comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {E'' : Type u_8} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H'' : Type u_9} [TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [TopologicalSpace M''] [ChartedSpace H'' M''] {n : ℕ∞} (f : ContMDiffMap I' I'' M' M'' n) (g : ContMDiffMap I I' M M' n) :
        ContMDiffMap I I'' M M'' n

        The composition of smooth maps, as a smooth map.

        Instances For
          @[simp]
          theorem ContMDiffMap.comp_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {E'' : Type u_8} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H'' : Type u_9} [TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [TopologicalSpace M''] [ChartedSpace H'' M''] {n : ℕ∞} (f : ContMDiffMap I' I'' M' M'' n) (g : ContMDiffMap I I' M M' n) (x : M) :
          ↑(ContMDiffMap.comp f g) x = f (g x)
          instance ContMDiffMap.instInhabitedContMDiffMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} [Inhabited M'] :
          Inhabited (ContMDiffMap I I' M M' n)
          def ContMDiffMap.const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (y : M') :
          ContMDiffMap I I' M M' n

          Constant map as a smooth map

          Instances For
            def ContMDiffMap.fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} :

            The first projection of a product, as a smooth map.

            Instances For
              def ContMDiffMap.snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} :
              ContMDiffMap (ModelWithCorners.prod I I') I' (M × M') M' n

              The second projection of a product, as a smooth map.

              Instances For
                def ContMDiffMap.prodMk {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_12} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (f : ContMDiffMap J I N M n) (g : ContMDiffMap J I' N M' n) :

                Given two smooth maps f and g, this is the smooth map x ↦ (f x, g x).

                Instances For
                  instance ContinuousLinearMap.hasCoeToContMDiffMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (n : ℕ∞) :
                  Coe (E →L[𝕜] E') (ContMDiffMap (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' n)