Documentation

Mathlib.Geometry.Manifold.ContMDiff.Defs

Smooth functions between smooth manifolds #

We define Cⁿ functions between smooth manifolds, as functions which are Cⁿ in charts, and prove basic properties of these notions.

Main definitions and statements #

Let M and M' be two smooth manifolds, with respect to model with corners I and I'. Let f : M → M'.

We also give some basic properties of smooth functions between manifolds, following the API of smooth functions between vector spaces. See Basic.lean for further basic properties of smooth functions between smooth manifolds, NormedSpace.lean for the equivalence of manifold-smoothness to usual smoothness, Product.lean for smoothness results related to the product of manifolds and Atlas.lean for smoothness of atlas members and local structomorphisms.

Implementation details #

Many properties follow for free from the corresponding properties of functions in vector spaces, as being Cⁿ is a local property invariant under the smooth groupoid. We take advantage of the general machinery developed in LocalInvariantProperties.lean to get these properties automatically. For instance, the fact that being Cⁿ does not depend on the chart one considers is given by liftPropWithinAt_indep_chart.

For this to work, the definition of ContMDiffWithinAt and friends has to follow definitionally the setup of local invariant properties. Still, we recast the definition in terms of extended charts in contMDiffOn_iff and contMDiff_iff.

Definition of smooth functions between manifolds #

def ContDiffWithinAtProp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') (n : ℕ∞) (f : HH') (s : Set H) (x : H) :

Property in the model space of a model with corners of being C^n within at set at a point, when read in the model vector space. This property will be lifted to manifolds to define smooth functions between manifolds.

Equations
Instances For
    theorem contDiffWithinAtProp_self_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {n : ℕ∞} {f : EH'} {s : Set E} {x : E} :
    ContDiffWithinAtProp (modelWithCornersSelf 𝕜 E) I' n f s x ContDiffWithinAt 𝕜 (↑n) (I' f) s x
    theorem contDiffWithinAtProp_self {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {n : ℕ∞} {f : EE'} {s : Set E} {x : E} :
    theorem contDiffWithinAtProp_self_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {n : ℕ∞} {f : HE'} {s : Set H} {x : H} :
    ContDiffWithinAtProp I (modelWithCornersSelf 𝕜 E') n f s x ContDiffWithinAt 𝕜 (↑n) (f I.symm) (I.symm ⁻¹' s Set.range I) (I x)
    theorem contDiffWithinAt_localInvariantProp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} (n : ℕ∞) :
    (contDiffGroupoid (↑) I).LocalInvariantProp (contDiffGroupoid (↑) I') (ContDiffWithinAtProp I I' n)

    Being Cⁿ in the model space is a local property, invariant under smooth maps. Therefore, it will lift nicely to manifolds.

    theorem contDiffWithinAtProp_mono_of_mem_nhdsWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} (n : ℕ∞) ⦃s : Set H ⦃x : H ⦃t : Set H ⦃f : HH' (hts : s nhdsWithin x t) (h : ContDiffWithinAtProp I I' n f s x) :
    @[deprecated contDiffWithinAtProp_mono_of_mem_nhdsWithin]
    theorem contDiffWithinAtProp_mono_of_mem {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} (n : ℕ∞) ⦃s : Set H ⦃x : H ⦃t : Set H ⦃f : HH' (hts : s nhdsWithin x t) (h : ContDiffWithinAtProp I I' n f s x) :

    Alias of contDiffWithinAtProp_mono_of_mem_nhdsWithin.

    theorem contDiffWithinAtProp_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : ℕ∞} (x : H) :
    ContDiffWithinAtProp I I n id Set.univ x
    def ContMDiffWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] (n : ℕ∞) (f : MM') (s : Set M) (x : M) :

    A function is n times continuously differentiable within a set at a point in a manifold if it is continuous and it is n times continuously differentiable in this set around this point, when read in the preferred chart at this point.

    Equations
    Instances For
      @[deprecated ContMDiffWithinAt]
      def SmoothWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] (n : ℕ∞) (f : MM') (s : Set M) (x : M) :

      Alias of ContMDiffWithinAt.


      A function is n times continuously differentiable within a set at a point in a manifold if it is continuous and it is n times continuously differentiable in this set around this point, when read in the preferred chart at this point.

      Equations
      Instances For
        def ContMDiffAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] (n : ℕ∞) (f : MM') (x : M) :

        A function is n times continuously differentiable at a point in a manifold if it is continuous and it is n times continuously differentiable around this point, when read in the preferred chart at this point.

        Equations
        Instances For
          theorem contMDiffAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} {f : MM'} {x : M} :
          ContMDiffAt I I' n f x ContinuousAt f x ContDiffWithinAt 𝕜 (↑n) ((extChartAt I' (f x)) f (extChartAt I x).symm) (Set.range I) ((extChartAt I x) x)
          @[deprecated ContMDiffAt]
          def SmoothAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] (n : ℕ∞) (f : MM') (x : M) :

          Alias of ContMDiffAt.


          A function is n times continuously differentiable at a point in a manifold if it is continuous and it is n times continuously differentiable around this point, when read in the preferred chart at this point.

          Equations
          Instances For
            def ContMDiffOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] (n : ℕ∞) (f : MM') (s : Set M) :

            A function is n times continuously differentiable in a set of a manifold if it is continuous and, for any pair of points, it is n times continuously differentiable on this set in the charts around these points.

            Equations
            Instances For
              @[deprecated ContMDiffOn]
              def SmoothOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] (n : ℕ∞) (f : MM') (s : Set M) :

              Alias of ContMDiffOn.


              A function is n times continuously differentiable in a set of a manifold if it is continuous and, for any pair of points, it is n times continuously differentiable on this set in the charts around these points.

              Equations
              Instances For
                def ContMDiff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] (n : ℕ∞) (f : MM') :

                A function is n times continuously differentiable in a manifold if it is continuous and, for any pair of points, it is n times continuously differentiable in the charts around these points.

                Equations
                Instances For
                  @[deprecated ContMDiff]
                  def Smooth {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] (n : ℕ∞) (f : MM') :

                  Alias of ContMDiff.


                  A function is n times continuously differentiable in a manifold if it is continuous and, for any pair of points, it is n times continuously differentiable in the charts around these points.

                  Equations
                  Instances For

                    Deducing smoothness from higher smoothness #

                    theorem ContMDiffWithinAt.of_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {m n : ℕ∞} (hf : ContMDiffWithinAt I I' n f s x) (le : m n) :
                    ContMDiffWithinAt I I' m f s x
                    theorem ContMDiffAt.of_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {x : M} {m n : ℕ∞} (hf : ContMDiffAt I I' n f x) (le : m n) :
                    ContMDiffAt I I' m f x
                    theorem ContMDiffOn.of_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {m n : ℕ∞} (hf : ContMDiffOn I I' n f s) (le : m n) :
                    ContMDiffOn I I' m f s
                    theorem ContMDiff.of_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {m n : ℕ∞} (hf : ContMDiff I I' n f) (le : m n) :
                    ContMDiff I I' m f

                    Basic properties of smooth functions between manifolds #

                    @[deprecated ContMDiff.of_le]
                    theorem ContMDiff.smooth {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {m n : ℕ∞} (hf : ContMDiff I I' n f) (le : m n) :
                    ContMDiff I I' m f

                    Alias of ContMDiff.of_le.

                    @[deprecated ContMDiff.of_le]
                    theorem Smooth.contMDiff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {m n : ℕ∞} (hf : ContMDiff I I' n f) (le : m n) :
                    ContMDiff I I' m f

                    Alias of ContMDiff.of_le.

                    @[deprecated ContMDiffOn.of_le]
                    theorem ContMDiffOn.smoothOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {m n : ℕ∞} (hf : ContMDiffOn I I' n f s) (le : m n) :
                    ContMDiffOn I I' m f s

                    Alias of ContMDiffOn.of_le.

                    @[deprecated ContMDiffOn.of_le]
                    theorem SmoothOn.contMDiffOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {m n : ℕ∞} (hf : ContMDiffOn I I' n f s) (le : m n) :
                    ContMDiffOn I I' m f s

                    Alias of ContMDiffOn.of_le.

                    @[deprecated ContMDiffAt.of_le]
                    theorem ContMDiffAt.smoothAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {x : M} {m n : ℕ∞} (hf : ContMDiffAt I I' n f x) (le : m n) :
                    ContMDiffAt I I' m f x

                    Alias of ContMDiffAt.of_le.

                    @[deprecated ContMDiffOn.of_le]
                    theorem SmoothAt.contMDiffAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {m n : ℕ∞} (hf : ContMDiffOn I I' n f s) (le : m n) :
                    ContMDiffOn I I' m f s

                    Alias of ContMDiffOn.of_le.

                    @[deprecated ContMDiffWithinAt.of_le]
                    theorem ContMDiffWithinAt.smoothWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {m n : ℕ∞} (hf : ContMDiffWithinAt I I' n f s x) (le : m n) :
                    ContMDiffWithinAt I I' m f s x

                    Alias of ContMDiffWithinAt.of_le.

                    @[deprecated ContMDiffWithinAt.of_le]
                    theorem SmoothWithinAt.contMDiffWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {m n : ℕ∞} (hf : ContMDiffWithinAt I I' n f s x) (le : m n) :
                    ContMDiffWithinAt I I' m f s x

                    Alias of ContMDiffWithinAt.of_le.

                    theorem ContMDiff.contMDiffAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {x : M} {n : ℕ∞} (h : ContMDiff I I' n f) :
                    ContMDiffAt I I' n f x
                    @[deprecated ContMDiff.contMDiffAt]
                    theorem Smooth.smoothAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {x : M} {n : ℕ∞} (h : ContMDiff I I' n f) :
                    ContMDiffAt I I' n f x

                    Alias of ContMDiff.contMDiffAt.

                    theorem contMDiffWithinAt_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {x : M} {n : ℕ∞} :
                    ContMDiffWithinAt I I' n f Set.univ x ContMDiffAt I I' n f x
                    @[deprecated contMDiffWithinAt_univ]
                    theorem smoothWithinAt_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {x : M} {n : ℕ∞} :
                    ContMDiffWithinAt I I' n f Set.univ x ContMDiffAt I I' n f x

                    Alias of contMDiffWithinAt_univ.

                    theorem contMDiffOn_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {n : ℕ∞} :
                    ContMDiffOn I I' n f Set.univ ContMDiff I I' n f
                    @[deprecated contMDiffOn_univ]
                    theorem smoothOn_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {n : ℕ∞} :
                    ContMDiffOn I I' n f Set.univ ContMDiff I I' n f

                    Alias of contMDiffOn_univ.

                    theorem contMDiffWithinAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} :
                    ContMDiffWithinAt I I' n f s x ContinuousWithinAt f s x ContDiffWithinAt 𝕜 (↑n) ((extChartAt I' (f x)) f (extChartAt I x).symm) ((extChartAt I x).symm ⁻¹' s Set.range I) ((extChartAt I x) x)

                    One can reformulate smoothness within a set at a point as continuity within this set at this point, and smoothness in the corresponding extended chart.

                    theorem contMDiffWithinAt_iff' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} :
                    ContMDiffWithinAt I I' n f s x ContinuousWithinAt f s x ContDiffWithinAt 𝕜 (↑n) ((extChartAt I' (f x)) f (extChartAt I x).symm) ((extChartAt I x).target (extChartAt I x).symm ⁻¹' (s f ⁻¹' (extChartAt I' (f x)).source)) ((extChartAt I x) x)

                    One can reformulate smoothness within a set at a point as continuity within this set at this point, and smoothness in the corresponding extended chart. This form states smoothness of f written in such a way that the set is restricted to lie within the domain/codomain of the corresponding charts. Even though this expression is more complicated than the one in contMDiffWithinAt_iff, it is a smaller set, but their germs at extChartAt I x x are equal. It is sometimes useful to rewrite using this in the goal.

                    theorem contMDiffWithinAt_iff_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} :
                    ContMDiffWithinAt I I' n f s x ContinuousWithinAt f s x ContMDiffWithinAt I (modelWithCornersSelf 𝕜 E') n ((extChartAt I' (f x)) f) s x

                    One can reformulate smoothness within a set at a point as continuity within this set at this point, and smoothness in the corresponding extended chart in the target.

                    @[deprecated contMDiffWithinAt_iff]
                    theorem smoothWithinAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} :
                    ContMDiffWithinAt I I' n f s x ContinuousWithinAt f s x ContDiffWithinAt 𝕜 (↑n) ((extChartAt I' (f x)) f (extChartAt I x).symm) ((extChartAt I x).symm ⁻¹' s Set.range I) ((extChartAt I x) x)

                    Alias of contMDiffWithinAt_iff.


                    One can reformulate smoothness within a set at a point as continuity within this set at this point, and smoothness in the corresponding extended chart.

                    @[deprecated contMDiffWithinAt_iff_target]
                    theorem smoothWithinAt_iff_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} :
                    ContMDiffWithinAt I I' n f s x ContinuousWithinAt f s x ContMDiffWithinAt I (modelWithCornersSelf 𝕜 E') n ((extChartAt I' (f x)) f) s x

                    Alias of contMDiffWithinAt_iff_target.


                    One can reformulate smoothness within a set at a point as continuity within this set at this point, and smoothness in the corresponding extended chart in the target.

                    theorem contMDiffAt_iff_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {n : ℕ∞} {x : M} :
                    ContMDiffAt I I' n f x ContinuousAt f x ContMDiffAt I (modelWithCornersSelf 𝕜 E') n ((extChartAt I' (f x)) f) x
                    @[deprecated contMDiffAt_iff_target]
                    theorem smoothAt_iff_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {n : ℕ∞} {x : M} :
                    ContMDiffAt I I' n f x ContinuousAt f x ContMDiffAt I (modelWithCornersSelf 𝕜 E') n ((extChartAt I' (f x)) f) x

                    Alias of contMDiffAt_iff_target.

                    theorem contMDiffWithinAt_iff_source_of_mem_maximalAtlas {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {e : PartialHomeomorph M H} {f : MM'} {s : Set M} {x : M} {n : ℕ∞} [SmoothManifoldWithCorners I M] (he : e SmoothManifoldWithCorners.maximalAtlas I M) (hx : x e.source) :
                    ContMDiffWithinAt I I' n f s x ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) I' n (f (e.extend I).symm) ((e.extend I).symm ⁻¹' s Set.range I) ((e.extend I) x)
                    theorem contMDiffWithinAt_iff_source_of_mem_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} [SmoothManifoldWithCorners I M] {x' : M} (hx' : x' (chartAt H x).source) :
                    ContMDiffWithinAt I I' n f s x' ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) I' n (f (extChartAt I x).symm) ((extChartAt I x).symm ⁻¹' s Set.range I) ((extChartAt I x) x')
                    theorem contMDiffAt_iff_source_of_mem_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {x : M} {n : ℕ∞} [SmoothManifoldWithCorners I M] {x' : M} (hx' : x' (chartAt H x).source) :
                    ContMDiffAt I I' n f x' ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) I' n (f (extChartAt I x).symm) (Set.range I) ((extChartAt I x) x')
                    theorem contMDiffWithinAt_iff_target_of_mem_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {n : ℕ∞} [SmoothManifoldWithCorners I' M'] {x : M} {y : M'} (hy : f x (chartAt H' y).source) :
                    theorem contMDiffAt_iff_target_of_mem_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {n : ℕ∞} [SmoothManifoldWithCorners I' M'] {x : M} {y : M'} (hy : f x (chartAt H' y).source) :
                    ContMDiffAt I I' n f x ContinuousAt f x ContMDiffAt I (modelWithCornersSelf 𝕜 E') n ((extChartAt I' y) f) x
                    theorem contMDiffWithinAt_iff_of_mem_maximalAtlas {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {e : PartialHomeomorph M H} {e' : PartialHomeomorph M' H'} {f : MM'} {s : Set M} {n : ℕ∞} [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] {x : M} (he : e SmoothManifoldWithCorners.maximalAtlas I M) (he' : e' SmoothManifoldWithCorners.maximalAtlas I' M') (hx : x e.source) (hy : f x e'.source) :
                    ContMDiffWithinAt I I' n f s x ContinuousWithinAt f s x ContDiffWithinAt 𝕜 (↑n) ((e'.extend I') f (e.extend I).symm) ((e.extend I).symm ⁻¹' s Set.range I) ((e.extend I) x)
                    theorem contMDiffWithinAt_iff_image {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {e : PartialHomeomorph M H} {e' : PartialHomeomorph M' H'} {f : MM'} {s : Set M} {n : ℕ∞} [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] {x : M} (he : e SmoothManifoldWithCorners.maximalAtlas I M) (he' : e' SmoothManifoldWithCorners.maximalAtlas I' M') (hs : s e.source) (hx : x e.source) (hy : f x e'.source) :
                    ContMDiffWithinAt I I' n f s x ContinuousWithinAt f s x ContDiffWithinAt 𝕜 (↑n) ((e'.extend I') f (e.extend I).symm) ((e.extend I) '' s) ((e.extend I) x)

                    An alternative formulation of contMDiffWithinAt_iff_of_mem_maximalAtlas if the set if s lies in e.source.

                    theorem contMDiffWithinAt_iff_of_mem_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] {x' : M} {y : M'} (hx : x' (chartAt H x).source) (hy : f x' (chartAt H' y).source) :
                    ContMDiffWithinAt I I' n f s x' ContinuousWithinAt f s x' ContDiffWithinAt 𝕜 (↑n) ((extChartAt I' y) f (extChartAt I x).symm) ((extChartAt I x).symm ⁻¹' s Set.range I) ((extChartAt I x) x')

                    One can reformulate smoothness within a set at a point as continuity within this set at this point, and smoothness in any chart containing that point.

                    theorem contMDiffWithinAt_iff_of_mem_source' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] {x' : M} {y : M'} (hx : x' (chartAt H x).source) (hy : f x' (chartAt H' y).source) :
                    ContMDiffWithinAt I I' n f s x' ContinuousWithinAt f s x' ContDiffWithinAt 𝕜 (↑n) ((extChartAt I' y) f (extChartAt I x).symm) ((extChartAt I x).target (extChartAt I x).symm ⁻¹' (s f ⁻¹' (extChartAt I' y).source)) ((extChartAt I x) x')
                    theorem contMDiffAt_iff_of_mem_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {x : M} {n : ℕ∞} [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] {x' : M} {y : M'} (hx : x' (chartAt H x).source) (hy : f x' (chartAt H' y).source) :
                    ContMDiffAt I I' n f x' ContinuousAt f x' ContDiffWithinAt 𝕜 (↑n) ((extChartAt I' y) f (extChartAt I x).symm) (Set.range I) ((extChartAt I x) x')
                    theorem contMDiffOn_iff_of_mem_maximalAtlas {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {e : PartialHomeomorph M H} {e' : PartialHomeomorph M' H'} {f : MM'} {s : Set M} {n : ℕ∞} [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] (he : e SmoothManifoldWithCorners.maximalAtlas I M) (he' : e' SmoothManifoldWithCorners.maximalAtlas I' M') (hs : s e.source) (h2s : Set.MapsTo f s e'.source) :
                    ContMDiffOn I I' n f s ContinuousOn f s ContDiffOn 𝕜 (↑n) ((e'.extend I') f (e.extend I).symm) ((e.extend I) '' s)
                    theorem contMDiffOn_iff_of_mem_maximalAtlas' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {e : PartialHomeomorph M H} {e' : PartialHomeomorph M' H'} {f : MM'} {s : Set M} {n : ℕ∞} [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] (he : e SmoothManifoldWithCorners.maximalAtlas I M) (he' : e' SmoothManifoldWithCorners.maximalAtlas I' M') (hs : s e.source) (h2s : Set.MapsTo f s e'.source) :
                    ContMDiffOn I I' n f s ContDiffOn 𝕜 (↑n) ((e'.extend I') f (e.extend I).symm) ((e.extend I) '' s)
                    theorem contMDiffOn_iff_of_subset_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {n : ℕ∞} [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] {x : M} {y : M'} (hs : s (chartAt H x).source) (h2s : Set.MapsTo f s (chartAt H' y).source) :
                    ContMDiffOn I I' n f s ContinuousOn f s ContDiffOn 𝕜 (↑n) ((extChartAt I' y) f (extChartAt I x).symm) ((extChartAt I x) '' s)

                    If the set where you want f to be smooth lies entirely in a single chart, and f maps it into a single chart, the smoothness of f on that set can be expressed by purely looking in these charts. Note: this lemma uses extChartAt I x '' s instead of (extChartAt I x).symm ⁻¹' s to ensure that this set lies in (extChartAt I x).target.

                    theorem contMDiffOn_iff_of_subset_source' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {n : ℕ∞} [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] {x : M} {y : M'} (hs : s (extChartAt I x).source) (h2s : Set.MapsTo f s (extChartAt I' y).source) :
                    ContMDiffOn I I' n f s ContDiffOn 𝕜 (↑n) ((extChartAt I' y) f (extChartAt I x).symm) ((extChartAt I x) '' s)

                    If the set where you want f to be smooth lies entirely in a single chart, and f maps it into a single chart, the smoothness of f on that set can be expressed by purely looking in these charts. Note: this lemma uses extChartAt I x '' s instead of (extChartAt I x).symm ⁻¹' s to ensure that this set lies in (extChartAt I x).target.

                    theorem contMDiffOn_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {n : ℕ∞} [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] :
                    ContMDiffOn I I' n f s ContinuousOn f s ∀ (x : M) (y : M'), ContDiffOn 𝕜 (↑n) ((extChartAt I' y) f (extChartAt I x).symm) ((extChartAt I x).target (extChartAt I x).symm ⁻¹' (s f ⁻¹' (extChartAt I' y).source))

                    One can reformulate smoothness on a set as continuity on this set, and smoothness in any extended chart.

                    theorem contMDiffOn_iff_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {n : ℕ∞} [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] :
                    ContMDiffOn I I' n f s ContinuousOn f s ∀ (y : M'), ContMDiffOn I (modelWithCornersSelf 𝕜 E') n ((extChartAt I' y) f) (s f ⁻¹' (extChartAt I' y).source)

                    One can reformulate smoothness on a set as continuity on this set, and smoothness in any extended chart in the target.

                    @[deprecated contMDiffOn_iff]
                    theorem smoothOn_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {n : ℕ∞} [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] :
                    ContMDiffOn I I' n f s ContinuousOn f s ∀ (x : M) (y : M'), ContDiffOn 𝕜 (↑n) ((extChartAt I' y) f (extChartAt I x).symm) ((extChartAt I x).target (extChartAt I x).symm ⁻¹' (s f ⁻¹' (extChartAt I' y).source))

                    Alias of contMDiffOn_iff.


                    One can reformulate smoothness on a set as continuity on this set, and smoothness in any extended chart.

                    @[deprecated contMDiffOn_iff_target]
                    theorem smoothOn_iff_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {n : ℕ∞} [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] :
                    ContMDiffOn I I' n f s ContinuousOn f s ∀ (y : M'), ContMDiffOn I (modelWithCornersSelf 𝕜 E') n ((extChartAt I' y) f) (s f ⁻¹' (extChartAt I' y).source)

                    Alias of contMDiffOn_iff_target.


                    One can reformulate smoothness on a set as continuity on this set, and smoothness in any extended chart in the target.

                    theorem contMDiff_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {n : ℕ∞} [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] :
                    ContMDiff I I' n f Continuous f ∀ (x : M) (y : M'), ContDiffOn 𝕜 (↑n) ((extChartAt I' y) f (extChartAt I x).symm) ((extChartAt I x).target (extChartAt I x).symm ⁻¹' (f ⁻¹' (extChartAt I' y).source))

                    One can reformulate smoothness as continuity and smoothness in any extended chart.

                    theorem contMDiff_iff_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {n : ℕ∞} [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] :
                    ContMDiff I I' n f Continuous f ∀ (y : M'), ContMDiffOn I (modelWithCornersSelf 𝕜 E') n ((extChartAt I' y) f) (f ⁻¹' (extChartAt I' y).source)

                    One can reformulate smoothness as continuity and smoothness in any extended chart in the target.

                    @[deprecated contMDiff_iff]
                    theorem smooth_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {n : ℕ∞} [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] :
                    ContMDiff I I' n f Continuous f ∀ (x : M) (y : M'), ContDiffOn 𝕜 (↑n) ((extChartAt I' y) f (extChartAt I x).symm) ((extChartAt I x).target (extChartAt I x).symm ⁻¹' (f ⁻¹' (extChartAt I' y).source))

                    Alias of contMDiff_iff.


                    One can reformulate smoothness as continuity and smoothness in any extended chart.

                    @[deprecated contMDiff_iff_target]
                    theorem smooth_iff_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {n : ℕ∞} [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] :
                    ContMDiff I I' n f Continuous f ∀ (y : M'), ContMDiffOn I (modelWithCornersSelf 𝕜 E') n ((extChartAt I' y) f) (f ⁻¹' (extChartAt I' y).source)

                    Alias of contMDiff_iff_target.


                    One can reformulate smoothness as continuity and smoothness in any extended chart in the target.

                    Deducing smoothness from smoothness one step beyond #

                    theorem ContMDiffWithinAt.of_succ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : } (h : ContMDiffWithinAt I I' (↑n.succ) f s x) :
                    ContMDiffWithinAt I I' (↑n) f s x
                    theorem ContMDiffAt.of_succ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {x : M} {n : } (h : ContMDiffAt I I' (↑n.succ) f x) :
                    ContMDiffAt I I' (↑n) f x
                    theorem ContMDiffOn.of_succ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {n : } (h : ContMDiffOn I I' (↑n.succ) f s) :
                    ContMDiffOn I I' (↑n) f s
                    theorem ContMDiff.of_succ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {n : } (h : ContMDiff I I' (↑n.succ) f) :
                    ContMDiff I I' (↑n) f

                    Deducing continuity from smoothness #

                    theorem ContMDiffWithinAt.continuousWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} (hf : ContMDiffWithinAt I I' n f s x) :
                    theorem ContMDiffAt.continuousAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {x : M} {n : ℕ∞} (hf : ContMDiffAt I I' n f x) :
                    theorem ContMDiffOn.continuousOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {n : ℕ∞} (hf : ContMDiffOn I I' n f s) :
                    theorem ContMDiff.continuous {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {n : ℕ∞} (hf : ContMDiff I I' n f) :

                    C^∞ smoothness #

                    theorem contMDiffWithinAt_top {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} :
                    ContMDiffWithinAt I I' f s x ∀ (n : ), ContMDiffWithinAt I I' (↑n) f s x
                    theorem contMDiffAt_top {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {x : M} :
                    ContMDiffAt I I' f x ∀ (n : ), ContMDiffAt I I' (↑n) f x
                    theorem contMDiffOn_top {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} :
                    ContMDiffOn I I' f s ∀ (n : ), ContMDiffOn I I' (↑n) f s
                    theorem contMDiff_top {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} :
                    ContMDiff I I' f ∀ (n : ), ContMDiff I I' (↑n) f
                    theorem contMDiffWithinAt_iff_nat {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} :
                    ContMDiffWithinAt I I' n f s x ∀ (m : ), m nContMDiffWithinAt I I' (↑m) f s x

                    Restriction to a smaller set #

                    theorem ContMDiffWithinAt.mono_of_mem_nhdsWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s t : Set M} {x : M} {n : ℕ∞} (hf : ContMDiffWithinAt I I' n f s x) (hts : s nhdsWithin x t) :
                    ContMDiffWithinAt I I' n f t x
                    @[deprecated ContMDiffWithinAt.mono_of_mem_nhdsWithin]
                    theorem ContMDiffWithinAt.mono_of_mem {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s t : Set M} {x : M} {n : ℕ∞} (hf : ContMDiffWithinAt I I' n f s x) (hts : s nhdsWithin x t) :
                    ContMDiffWithinAt I I' n f t x

                    Alias of ContMDiffWithinAt.mono_of_mem_nhdsWithin.

                    theorem ContMDiffWithinAt.mono {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s t : Set M} {x : M} {n : ℕ∞} (hf : ContMDiffWithinAt I I' n f s x) (hts : t s) :
                    ContMDiffWithinAt I I' n f t x
                    theorem contMDiffWithinAt_congr_set {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s t : Set M} {x : M} {n : ℕ∞} (h : s =ᶠ[nhds x] t) :
                    ContMDiffWithinAt I I' n f s x ContMDiffWithinAt I I' n f t x
                    theorem ContMDiffWithinAt.congr_set {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s t : Set M} {x : M} {n : ℕ∞} (h : ContMDiffWithinAt I I' n f s x) (hst : s =ᶠ[nhds x] t) :
                    ContMDiffWithinAt I I' n f t x
                    @[deprecated contMDiffWithinAt_congr_set]
                    theorem contMDiffWithinAt_congr_nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s t : Set M} {x : M} {n : ℕ∞} (h : s =ᶠ[nhds x] t) :
                    ContMDiffWithinAt I I' n f s x ContMDiffWithinAt I I' n f t x

                    Alias of contMDiffWithinAt_congr_set.

                    theorem contMDiffWithinAt_insert_self {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} :
                    ContMDiffWithinAt I I' n f (insert x s) x ContMDiffWithinAt I I' n f s x
                    theorem ContMDiffWithinAt.of_insert {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} :
                    ContMDiffWithinAt I I' n f (insert x s) xContMDiffWithinAt I I' n f s x

                    Alias of the forward direction of contMDiffWithinAt_insert_self.

                    theorem ContMDiffWithinAt.insert {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} (h : ContMDiffWithinAt I I' n f s x) :
                    ContMDiffWithinAt I I' n f (insert x s) x
                    theorem contMDiffWithinAt_congr_set' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s t : Set M} {x : M} {n : ℕ∞} (y : M) (h : s =ᶠ[nhdsWithin x {y}] t) :
                    ContMDiffWithinAt I I' n f s x ContMDiffWithinAt I I' n f t x

                    Being C^n in a set only depends on the germ of the set. Version where one only requires the two sets to coincide locally in the complement of a point y.

                    theorem ContMDiffAt.contMDiffWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} (hf : ContMDiffAt I I' n f x) :
                    ContMDiffWithinAt I I' n f s x
                    @[deprecated ContMDiffAt.contMDiffWithinAt]
                    theorem SmoothAt.smoothWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} (hf : ContMDiffAt I I' n f x) :
                    ContMDiffWithinAt I I' n f s x

                    Alias of ContMDiffAt.contMDiffWithinAt.

                    theorem ContMDiffOn.mono {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s t : Set M} {n : ℕ∞} (hf : ContMDiffOn I I' n f s) (hts : t s) :
                    ContMDiffOn I I' n f t
                    theorem ContMDiff.contMDiffOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {n : ℕ∞} (hf : ContMDiff I I' n f) :
                    ContMDiffOn I I' n f s
                    @[deprecated ContMDiff.contMDiffOn]
                    theorem Smooth.smoothOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {n : ℕ∞} (hf : ContMDiff I I' n f) :
                    ContMDiffOn I I' n f s

                    Alias of ContMDiff.contMDiffOn.

                    theorem contMDiffWithinAt_inter' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s t : Set M} {x : M} {n : ℕ∞} (ht : t nhdsWithin x s) :
                    ContMDiffWithinAt I I' n f (s t) x ContMDiffWithinAt I I' n f s x
                    theorem contMDiffWithinAt_inter {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s t : Set M} {x : M} {n : ℕ∞} (ht : t nhds x) :
                    ContMDiffWithinAt I I' n f (s t) x ContMDiffWithinAt I I' n f s x
                    theorem ContMDiffWithinAt.contMDiffAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} (h : ContMDiffWithinAt I I' n f s x) (ht : s nhds x) :
                    ContMDiffAt I I' n f x
                    @[deprecated ContMDiffWithinAt.contMDiffAt]
                    theorem SmoothWithinAt.smoothAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} (h : ContMDiffWithinAt I I' n f s x) (ht : s nhds x) :
                    ContMDiffAt I I' n f x

                    Alias of ContMDiffWithinAt.contMDiffAt.

                    theorem ContMDiffOn.contMDiffAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} (h : ContMDiffOn I I' n f s) (hx : s nhds x) :
                    ContMDiffAt I I' n f x
                    @[deprecated ContMDiffOn.contMDiffAt]
                    theorem SmoothOn.smoothAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} (h : ContMDiffOn I I' n f s) (hx : s nhds x) :
                    ContMDiffAt I I' n f x

                    Alias of ContMDiffOn.contMDiffAt.

                    theorem contMDiffOn_iff_source_of_mem_maximalAtlas {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {e : PartialHomeomorph M H} {f : MM'} {s : Set M} {n : ℕ∞} [SmoothManifoldWithCorners I M] (he : e SmoothManifoldWithCorners.maximalAtlas I M) (hs : s e.source) :
                    ContMDiffOn I I' n f s ContMDiffOn (modelWithCornersSelf 𝕜 E) I' n (f (e.extend I).symm) ((e.extend I) '' s)
                    theorem contMDiffWithinAt_iff_contMDiffOn_nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] {n : } :
                    ContMDiffWithinAt I I' (↑n) f s x unhdsWithin x (insert x s), ContMDiffOn I I' (↑n) f u

                    A function is C^n within a set at a point, for n : ℕ, if and only if it is C^n on a neighborhood of this point.

                    theorem ContMDiffWithinAt.contMDiffOn' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] {m : } (hm : m n) (h : ContMDiffWithinAt I I' n f s x) :
                    ∃ (u : Set M), IsOpen u x u ContMDiffOn I I' (↑m) f (insert x s u)

                    If a function is C^m within a set at a point, for some finite m, then it is C^m within this set on an open set around the basepoint.

                    theorem ContMDiffWithinAt.contMDiffOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] {m : } (hm : m n) (h : ContMDiffWithinAt I I' n f s x) :
                    unhdsWithin x (insert x s), u insert x s ContMDiffOn I I' (↑m) f u

                    If a function is C^m within a set at a point, for some finite m, then it is C^m within this set on a neighborhood of the basepoint.

                    theorem contMDiffAt_iff_contMDiffOn_nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {x : M} [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] {n : } :
                    ContMDiffAt I I' (↑n) f x unhds x, ContMDiffOn I I' (↑n) f u

                    A function is C^n at a point, for n : ℕ, if and only if it is C^n on a neighborhood of this point.

                    theorem contMDiffAt_iff_contMDiffAt_nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {x : M} [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] {n : } :
                    ContMDiffAt I I' (↑n) f x ∀ᶠ (x' : M) in nhds x, ContMDiffAt I I' (↑n) f x'

                    Note: This does not hold for n = ∞. f being C^∞ at x means that for every n, f is C^n on some neighborhood of x, but this neighborhood can depend on n.

                    theorem contMDiffWithinAt_iff_contMDiffWithinAt_nhdsWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] {n : } :
                    ContMDiffWithinAt I I' (↑n) f s x ∀ᶠ (x' : M) in nhdsWithin x (insert x s), ContMDiffWithinAt I I' (↑n) f s x'

                    Note: This does not hold for n = ∞. f being C^∞ at x means that for every n, f is C^n on some neighborhood of x, but this neighborhood can depend on n.

                    Congruence lemmas #

                    theorem ContMDiffWithinAt.congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f f₁ : MM'} {s : Set M} {x : M} {n : ℕ∞} (h : ContMDiffWithinAt I I' n f s x) (h₁ : ys, f₁ y = f y) (hx : f₁ x = f x) :
                    ContMDiffWithinAt I I' n f₁ s x
                    theorem contMDiffWithinAt_congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f f₁ : MM'} {s : Set M} {x : M} {n : ℕ∞} (h₁ : ys, f₁ y = f y) (hx : f₁ x = f x) :
                    ContMDiffWithinAt I I' n f₁ s x ContMDiffWithinAt I I' n f s x
                    theorem ContMDiffWithinAt.congr_of_mem {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f f₁ : MM'} {s : Set M} {x : M} {n : ℕ∞} (h : ContMDiffWithinAt I I' n f s x) (h₁ : ys, f₁ y = f y) (hx : x s) :
                    ContMDiffWithinAt I I' n f₁ s x
                    theorem contMDiffWithinAt_congr_of_mem {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f f₁ : MM'} {s : Set M} {x : M} {n : ℕ∞} (h₁ : ys, f₁ y = f y) (hx : x s) :
                    ContMDiffWithinAt I I' n f₁ s x ContMDiffWithinAt I I' n f s x
                    theorem ContMDiffWithinAt.congr_of_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f f₁ : MM'} {s : Set M} {x : M} {n : ℕ∞} (h : ContMDiffWithinAt I I' n f s x) (h₁ : f₁ =ᶠ[nhdsWithin x s] f) (hx : f₁ x = f x) :
                    ContMDiffWithinAt I I' n f₁ s x
                    theorem ContMDiffWithinAt.congr_of_eventuallyEq_of_mem {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f f₁ : MM'} {s : Set M} {x : M} {n : ℕ∞} (h : ContMDiffWithinAt I I' n f s x) (h₁ : f₁ =ᶠ[nhdsWithin x s] f) (hx : x s) :
                    ContMDiffWithinAt I I' n f₁ s x
                    theorem Filter.EventuallyEq.contMDiffWithinAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f f₁ : MM'} {s : Set M} {x : M} {n : ℕ∞} (h₁ : f₁ =ᶠ[nhdsWithin x s] f) (hx : f₁ x = f x) :
                    ContMDiffWithinAt I I' n f₁ s x ContMDiffWithinAt I I' n f s x
                    theorem ContMDiffAt.congr_of_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f f₁ : MM'} {x : M} {n : ℕ∞} (h : ContMDiffAt I I' n f x) (h₁ : f₁ =ᶠ[nhds x] f) :
                    ContMDiffAt I I' n f₁ x
                    theorem Filter.EventuallyEq.contMDiffAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f f₁ : MM'} {x : M} {n : ℕ∞} (h₁ : f₁ =ᶠ[nhds x] f) :
                    ContMDiffAt I I' n f₁ x ContMDiffAt I I' n f x
                    theorem ContMDiffOn.congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f f₁ : MM'} {s : Set M} {n : ℕ∞} (h : ContMDiffOn I I' n f s) (h₁ : ys, f₁ y = f y) :
                    ContMDiffOn I I' n f₁ s
                    theorem contMDiffOn_congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f f₁ : MM'} {s : Set M} {n : ℕ∞} (h₁ : ys, f₁ y = f y) :
                    ContMDiffOn I I' n f₁ s ContMDiffOn I I' n f s
                    theorem ContMDiffOn.congr_mono {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f f₁ : MM'} {s s₁ : Set M} {n : ℕ∞} (hf : ContMDiffOn I I' n f s) (h₁ : ys₁, f₁ y = f y) (hs : s₁ s) :
                    ContMDiffOn I I' n f₁ s₁

                    Locality #

                    theorem contMDiffOn_of_locally_contMDiffOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {s : Set M} {n : ℕ∞} (h : xs, ∃ (u : Set M), IsOpen u x u ContMDiffOn I I' n f (s u)) :
                    ContMDiffOn I I' n f s

                    Being C^n is a local property.

                    theorem contMDiff_of_locally_contMDiffOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : MM'} {n : ℕ∞} (h : ∀ (x : M), ∃ (u : Set M), IsOpen u x u ContMDiffOn I I' n f u) :
                    ContMDiff I I' n f