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.

Equations
Instances For
    @[reducible, inline]
    abbrev 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.

    Equations
    Instances For

      Bundled n times continuously differentiable maps.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Bundled n times continuously differentiable maps.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          instance ContMDiffMap.instFunLike {𝕜 : 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 M'
          Equations
          • ContMDiffMap.instFunLike = { coe := Subtype.val, coe_injective' := }
          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) :
          f, 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.instContinuousMapClass {𝕜 : 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'
          Equations
          • =
          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.

          Equations
          • ContMDiffMap.id = id,
          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.

            Equations
            • f.comp g = fun (a : M) => f (g a),
            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) :
              (f.comp g) x = f (g x)
              instance ContMDiffMap.instInhabited {𝕜 : 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)
              Equations
              • ContMDiffMap.instInhabited = { default := fun (x : M) => default, }
              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

              Equations
              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 : ℕ∞} :
                ContMDiffMap (I.prod I') I (M × M') M n

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

                Equations
                • ContMDiffMap.fst = Prod.fst,
                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 (I.prod I') I' (M × M') M' n

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

                  Equations
                  • ContMDiffMap.snd = Prod.snd,
                  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) :
                    ContMDiffMap J (I.prod I') N (M × M') n

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

                    Equations
                    • f.prodMk g = fun (x : N) => (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)
                      Equations