Documentation

Mathlib.Geometry.Manifold.IsManifold.Basic

C^n manifolds (possibly with boundary or corners) #

A C^n manifold is a manifold modelled on a normed vector space, or a subset like a half-space (to get manifolds with boundaries) for which the changes of coordinates are C^n maps. We define a model with corners as a map I : H β†’ E embedding nicely the topological space H in the vector space E (or more precisely as a structure containing all the relevant properties). Given such a model with corners I on (E, H), we define the groupoid of local homeomorphisms of H which are C^n when read in E (for any regularity n : WithTop β„•βˆž). With this groupoid at hand and the general machinery of charted spaces, we thus get the notion of C^n manifold with respect to any model with corners I on (E, H).

Some texts assume manifolds to be Hausdorff and second countable. We (in mathlib) assume neither, but add these assumptions later as needed. (Quite a few results still do not require them.)

Main definitions #

We define a few constructions of smooth manifolds:

As specific examples of models with corners, we define (in Geometry.Manifold.Instances.Real)

With these definitions at hand, to invoke an n-dimensional C^∞ real manifold without boundary, one could use

variable {n : β„•} {M : Type*} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsManifold (𝓑 n) ∞ M].

However, this is not the recommended way: a theorem proved using this assumption would not apply for instance to the tangent space of such a manifold, which is modelled on (EuclideanSpace ℝ (Fin n)) Γ— (EuclideanSpace ℝ (Fin n)) and not on EuclideanSpace ℝ (Fin (2 * n))! In the same way, it would not apply to product manifolds, modelled on (EuclideanSpace ℝ (Fin n)) Γ— (EuclideanSpace ℝ (Fin m)). The right invocation does not focus on one specific construction, but on all constructions sharing the right properties, like

variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {I : ModelWithCorners ℝ E E} [I.Boundaryless] {M : Type*} [TopologicalSpace M] [ChartedSpace E M] [IsManifold I ∞ M]

Here, I.Boundaryless is a typeclass property ensuring that there is no boundary (this is for instance the case for modelWithCornersSelf, or products of these). Note that one could consider as a natural assumption to only use the trivial model with corners modelWithCornersSelf ℝ E, but again in product manifolds the natural model with corners will not be this one but the product one (and they are not defeq as (fun p : E Γ— F ↦ (p.1, p.2)) is not defeq to the identity). So, it is important to use the above incantation to maximize the applicability of theorems.

Even better, if the result should apply in a parallel way to smooth manifolds and to analytic manifolds, the last typeclass should be replaced with [IsManifold I n M] for n : WithTop β„•βˆž.

We also define TangentSpace I (x : M) as a type synonym of E, and TangentBundle I M as a type synonym for Ξ  (x : M), TangentSpace I x (in the form of an abbrev of Bundle.TotalSpace E (TangentSpace I : M β†’ Type _)). Apart from basic typeclasses on TangentSpace I x, nothing is proved about them in this file, but it is useful to have them available as definitions early on to get a clean import structure below. The smooth bundle structure is defined in VectorBundle.Tangent, while the definition is used to talk about manifold derivatives in MFDeriv.Basic, and neither file needs import the other.

Implementation notes #

We want to talk about manifolds modelled on a vector space, but also on manifolds with boundary, modelled on a half space (or even manifolds with corners). For the latter examples, we still want to define smooth functions, tangent bundles, and so on. As smooth functions are well defined on vector spaces or subsets of these, one could take for model space a subtype of a vector space. With the drawback that the whole vector space itself (which is the most basic example) is not directly a subtype of itself: the inclusion of univ : Set E in Set E would show up in the definition, instead of id.

A good abstraction covering both cases it to have a vector space E (with basic example the Euclidean space), a model space H (with basic example the upper half space), and an embedding of H into E (which can be the identity for H = E, or Subtype.val for manifolds with corners). We say that the pair (E, H) with their embedding is a model with corners, and we encompass all the relevant properties (in particular the fact that the image of H in E should have unique differentials) in the definition of ModelWithCorners.

I have considered using the model with corners I as a typeclass argument, possibly outParam, to get lighter notations later on, but it did not turn out right, as on E Γ— F there are two natural model with corners, the trivial (identity) one, and the product one, and they are not defeq and one needs to indicate to Lean which one we want to use. This means that when talking on objects on manifolds one will most often need to specify the model with corners one is using. For instance, the tangent bundle will be TangentBundle I M and the derivative will be mfderiv I I' f, instead of the more natural notations TangentBundle π•œ M and mfderiv π•œ f (the field has to be explicit anyway, as some manifolds could be considered both as real and complex manifolds).

Models with corners. #

structure ModelWithCorners (π•œ : Type u_1) [NontriviallyNormedField π•œ] (E : Type u_2) [NormedAddCommGroup E] [NormedSpace π•œ E] (H : Type u_3) [TopologicalSpace H] extends PartialEquiv H E :
Type (max u_2 u_3)

A structure containing information on the way a space H embeds in a model vector space E over the field π•œ. This is all what is needed to define a C^n manifold with model space H, and model vector space E.

We require that, when the field is ℝ or β„‚, the range is ℝ-convex, as this is what is needed to do calculus and covers the standard examples of manifolds with boundary. Over other fields, we require that the range is univ, as there is no relevant notion of manifold of boundary there.

Instances For
    theorem ModelWithCorners.ext_iff {π•œ : Type u_1} {inst✝ : NontriviallyNormedField π•œ} {E : Type u_2} {inst✝¹ : NormedAddCommGroup E} {inst✝² : NormedSpace π•œ E} {H : Type u_3} {inst✝³ : TopologicalSpace H} {x y : ModelWithCorners π•œ E H} :
    theorem ModelWithCorners.ext {π•œ : Type u_1} {inst✝ : NontriviallyNormedField π•œ} {E : Type u_2} {inst✝¹ : NormedAddCommGroup E} {inst✝² : NormedSpace π•œ E} {H : Type u_3} {inst✝³ : TopologicalSpace H} {x y : ModelWithCorners π•œ E H} (toFun : ↑x.toPartialEquiv = ↑y.toPartialEquiv) (invFun : x.invFun = y.invFun) (source : x.source = y.source) (target : x.target = y.target) :
    x = y
    theorem ModelWithCorners.range_eq_target {π•œ : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField π•œ] [NormedAddCommGroup E] [NormedSpace π•œ E] [TopologicalSpace H] (I : ModelWithCorners π•œ E H) :
    def ModelWithCorners.of_target_univ (π•œ : Type u_1) [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (Ο† : PartialEquiv H E) (hsource : Ο†.source = Set.univ) (htarget : Ο†.target = Set.univ) (hcont : Continuous ↑φ) (hcont_inv : Continuous ↑φ.symm) :
    ModelWithCorners π•œ E H

    If a model with corners has full range, the convex_range' condition is satisfied.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def modelWithCornersSelf (π•œ : Type u_1) [NontriviallyNormedField π•œ] (E : Type u_2) [NormedAddCommGroup E] [NormedSpace π•œ E] :
      ModelWithCorners π•œ E E

      A vector space is a model with corners, denoted as π“˜(π•œ, E) within the Manifold namespace.

      Equations
      Instances For

        A vector space is a model with corners, denoted as π“˜(π•œ, E) within the Manifold namespace.

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

          A normed field is a model with corners.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            def ModelWithCorners.toFun' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (e : ModelWithCorners π•œ E H) :
            H β†’ E

            Coercion of a model with corners to a function. We don't use e.toFun because it is actually e.toPartialEquiv.toFun, so simp will apply lemmas about toPartialEquiv. While we may want to switch to this behavior later, doing it mid-port will break a lot of proofs.

            Equations
            Instances For
              instance ModelWithCorners.instCoeFunForall {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] :
              CoeFun (ModelWithCorners π•œ E H) fun (x : ModelWithCorners π•œ E H) => H β†’ E
              Equations
              def ModelWithCorners.symm {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) :

              The inverse to a model with corners, only registered as a PartialEquiv.

              Equations
              Instances For
                def ModelWithCorners.Simps.apply (π•œ : Type u_4) [NontriviallyNormedField π•œ] (E : Type u_5) [NormedAddCommGroup E] [NormedSpace π•œ E] (H : Type u_6) [TopologicalSpace H] (I : ModelWithCorners π•œ E H) :
                H β†’ E

                See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

                Equations
                Instances For
                  def ModelWithCorners.Simps.symm_apply (π•œ : Type u_4) [NontriviallyNormedField π•œ] (E : Type u_5) [NormedAddCommGroup E] [NormedSpace π•œ E] (H : Type u_6) [TopologicalSpace H] (I : ModelWithCorners π•œ E H) :
                  E β†’ H

                  See Note [custom simps projection]

                  Equations
                  Instances For
                    @[simp]
                    theorem ModelWithCorners.toPartialEquiv_coe {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) :
                    ↑I.toPartialEquiv = ↑I
                    @[simp]
                    theorem ModelWithCorners.mk_coe {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (e : PartialEquiv H E) (a : e.source = Set.univ) (b : if h : IsRCLikeNormedField π•œ then Convex ℝ (Set.range ↑e) else Set.range ↑e = Set.univ) (c : (interior (Set.range ↑e)).Nonempty) (d : Continuous ↑e) (d' : Continuous e.invFun) :
                    ↑{ toPartialEquiv := e, source_eq := a, convex_range' := b, nonempty_interior' := c, continuous_toFun := d, continuous_invFun := d' } = ↑e
                    @[simp]
                    theorem ModelWithCorners.toPartialEquiv_coe_symm {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) :
                    ↑I.symm = ↑I.symm
                    @[simp]
                    theorem ModelWithCorners.mk_symm {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (e : PartialEquiv H E) (a : e.source = Set.univ) (b : if h : IsRCLikeNormedField π•œ then Convex ℝ (Set.range ↑e) else Set.range ↑e = Set.univ) (c : (interior (Set.range ↑e)).Nonempty) (d : Continuous ↑e) (d' : Continuous e.invFun) :
                    { toPartialEquiv := e, source_eq := a, convex_range' := b, nonempty_interior' := c, continuous_toFun := d, continuous_invFun := d' }.symm = e.symm
                    theorem ModelWithCorners.continuous {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) :
                    Continuous ↑I
                    theorem ModelWithCorners.continuousAt {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) {x : H} :
                    ContinuousAt (↑I) x
                    theorem ModelWithCorners.continuousWithinAt {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) {s : Set H} {x : H} :
                    ContinuousWithinAt (↑I) s x
                    theorem ModelWithCorners.continuous_symm {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) :
                    theorem ModelWithCorners.continuousAt_symm {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) {x : E} :
                    ContinuousAt (↑I.symm) x
                    theorem ModelWithCorners.continuousWithinAt_symm {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) {s : Set E} {x : E} :
                    ContinuousWithinAt (↑I.symm) s x
                    theorem ModelWithCorners.continuousOn_symm {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) {s : Set E} :
                    ContinuousOn (↑I.symm) s
                    @[simp]
                    theorem ModelWithCorners.target_eq {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) :
                    I.target = Set.range ↑I
                    theorem ModelWithCorners.nonempty_interior {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) :
                    theorem Convex.convex_isRCLikeNormedField {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] [NormedSpace ℝ E] [h : IsRCLikeNormedField π•œ] {s : Set E} (hs : Convex ℝ s) :

                    If a set is ℝ-convex for some normed space structure, then it is ℝ-convex for the normed space structure coming from an IsRCLikeNormedField π•œ. Useful when constructing model spaces to avoid diamond issues when populating the field convex_range'.

                    def ModelWithCorners.of_convex_range {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_5} [TopologicalSpace H] (Ο† : PartialEquiv H E) (hsource : Ο†.source = Set.univ) (htarget : Convex ℝ Ο†.target) (hcont : Continuous ↑φ) (hcont_inv : Continuous ↑φ.symm) (hint : (interior Ο†.target).Nonempty) :

                    Construct a model with corners over ℝ from a continuous partial equiv with convex range.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      theorem ModelWithCorners.convex_range {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) [NormedSpace ℝ E] :
                      theorem ModelWithCorners.uniqueDiffOn {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) :
                      UniqueDiffOn π•œ (Set.range ↑I)
                      theorem ModelWithCorners.range_subset_closure_interior {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) :
                      @[simp]
                      theorem ModelWithCorners.left_inv {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) (x : H) :
                      ↑I.symm (↑I x) = x
                      theorem ModelWithCorners.leftInverse {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) :
                      Function.LeftInverse ↑I.symm ↑I
                      theorem ModelWithCorners.injective {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) :
                      @[simp]
                      theorem ModelWithCorners.symm_comp_self {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) :
                      ↑I.symm ∘ ↑I = id
                      theorem ModelWithCorners.rightInvOn {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) :
                      Set.RightInvOn (↑I.symm) (↑I) (Set.range ↑I)
                      @[simp]
                      theorem ModelWithCorners.right_inv {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) {x : E} (hx : x ∈ Set.range ↑I) :
                      ↑I (↑I.symm x) = x
                      theorem ModelWithCorners.preimage_image {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) (s : Set H) :
                      ↑I ⁻¹' (↑I '' s) = s
                      theorem ModelWithCorners.image_eq {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) (s : Set H) :
                      ↑I '' s = ↑I.symm ⁻¹' s ∩ Set.range ↑I
                      theorem ModelWithCorners.isClosedEmbedding {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) :
                      theorem ModelWithCorners.isClosed_range {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) :
                      theorem ModelWithCorners.range_eq_closure_interior {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) :
                      Set.range ↑I = closure (interior (Set.range ↑I))
                      theorem ModelWithCorners.map_nhds_eq {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) (x : H) :
                      Filter.map (↑I) (nhds x) = nhdsWithin (↑I x) (Set.range ↑I)
                      theorem ModelWithCorners.map_nhdsWithin_eq {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) (s : Set H) (x : H) :
                      Filter.map (↑I) (nhdsWithin x s) = nhdsWithin (↑I x) (↑I '' s)
                      theorem ModelWithCorners.image_mem_nhdsWithin {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) {x : H} {s : Set H} (hs : s ∈ nhds x) :
                      ↑I '' s ∈ nhdsWithin (↑I x) (Set.range ↑I)
                      theorem ModelWithCorners.symm_map_nhdsWithin_image {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) {x : H} {s : Set H} :
                      Filter.map (↑I.symm) (nhdsWithin (↑I x) (↑I '' s)) = nhdsWithin x s
                      theorem ModelWithCorners.symm_map_nhdsWithin_range {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) (x : H) :
                      Filter.map (↑I.symm) (nhdsWithin (↑I x) (Set.range ↑I)) = nhds x
                      theorem ModelWithCorners.uniqueDiffOn_preimage {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) {s : Set H} (hs : IsOpen s) :
                      UniqueDiffOn π•œ (↑I.symm ⁻¹' s ∩ Set.range ↑I)
                      theorem ModelWithCorners.uniqueDiffOn_preimage_source {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) {Ξ² : Type u_4} [TopologicalSpace Ξ²] {e : PartialHomeomorph H Ξ²} :
                      UniqueDiffOn π•œ (↑I.symm ⁻¹' e.source ∩ Set.range ↑I)
                      theorem ModelWithCorners.uniqueDiffWithinAt_image {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) {x : H} :
                      UniqueDiffWithinAt π•œ (Set.range ↑I) (↑I x)
                      theorem ModelWithCorners.symm_continuousWithinAt_comp_right_iff {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) {X : Type u_4} [TopologicalSpace X] {f : H β†’ X} {s : Set H} {x : H} :
                      ContinuousWithinAt (f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ Set.range ↑I) (↑I x) ↔ ContinuousWithinAt f s x
                      theorem ModelWithCorners.t1Space {π•œ : 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] :

                      Every manifold is a FrΓ©chet space (T1 space) -- regardless of whether it is Hausdorff.

                      @[simp]

                      In the trivial model with corners, the associated PartialEquiv is the identity.

                      @[simp]
                      theorem modelWithCornersSelf_coe (π•œ : Type u_1) [NontriviallyNormedField π•œ] (E : Type u_2) [NormedAddCommGroup E] [NormedSpace π•œ E] :
                      ↑(modelWithCornersSelf π•œ E) = id
                      @[simp]
                      theorem modelWithCornersSelf_coe_symm (π•œ : Type u_1) [NontriviallyNormedField π•œ] (E : Type u_2) [NormedAddCommGroup E] [NormedSpace π•œ E] :
                      ↑(modelWithCornersSelf π•œ E).symm = id
                      def ModelWithCorners.prod {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type w} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) {E' : Type v'} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {H' : Type w'} [TopologicalSpace H'] (I' : ModelWithCorners π•œ E' H') :
                      ModelWithCorners π•œ (E Γ— E') (ModelProd H H')

                      Given two model_with_corners I on (E, H) and I' on (E', H'), we define the model with corners I.prod I' on (E Γ— E', ModelProd H H'). This appears in particular for the manifold structure on the tangent bundle to a manifold modelled on (E, H): it will be modelled on (E Γ— E, H Γ— E). See note [Manifold type tags] for explanation about ModelProd H H' vs H Γ— H'.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        theorem ModelWithCorners.prod_source {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type w} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) {E' : Type v'} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {H' : Type w'} [TopologicalSpace H'] (I' : ModelWithCorners π•œ E' H') :
                        (I.prod I').source = {x : ModelProd H H' | x.1 ∈ I.source ∧ x.2 ∈ I'.source}
                        theorem ModelWithCorners.prod_symm_apply {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type w} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) {E' : Type v'} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {H' : Type w'} [TopologicalSpace H'] (I' : ModelWithCorners π•œ E' H') (x : E Γ— E') :
                        ↑(I.prod I').symm x = (↑I.symm x.1, ↑I'.symm x.2)
                        theorem ModelWithCorners.prod_target {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type w} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) {E' : Type v'} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {H' : Type w'} [TopologicalSpace H'] (I' : ModelWithCorners π•œ E' H') :
                        theorem ModelWithCorners.prod_apply {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type w} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) {E' : Type v'} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {H' : Type w'} [TopologicalSpace H'] (I' : ModelWithCorners π•œ E' H') (x : ModelProd H H') :
                        ↑(I.prod I') x = (↑I x.1, ↑I' x.2)
                        def ModelWithCorners.pi {π•œ : Type u} [NontriviallyNormedField π•œ] {ΞΉ : Type v} [Fintype ΞΉ] {E : ΞΉ β†’ Type w} [(i : ΞΉ) β†’ NormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] {H : ΞΉ β†’ Type u'} [(i : ΞΉ) β†’ TopologicalSpace (H i)] (I : (i : ΞΉ) β†’ ModelWithCorners π•œ (E i) (H i)) :
                        ModelWithCorners π•œ ((i : ΞΉ) β†’ E i) (ModelPi H)

                        Given a finite family of ModelWithCorners I i on (E i, H i), we define the model with corners pi I on (Ξ  i, E i, ModelPi H). See note [Manifold type tags] for explanation about ModelPi H.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[reducible, inline]
                          abbrev ModelWithCorners.tangent {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type w} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) :
                          ModelWithCorners π•œ (E Γ— E) (ModelProd H E)

                          Special case of product model with corners, which is trivial on the second factor. This shows up as the model to tangent bundles.

                          Equations
                          Instances For
                            @[simp]
                            theorem modelWithCorners_prod_toPartialEquiv {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ F] {H : Type u_5} [TopologicalSpace H] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners π•œ E H} {J : ModelWithCorners π•œ F G} :
                            @[simp]
                            theorem modelWithCorners_prod_coe {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] (I : ModelWithCorners π•œ E H) (I' : ModelWithCorners π•œ E' H') :
                            ↑(I.prod I') = Prod.map ↑I ↑I'
                            @[simp]
                            theorem modelWithCorners_prod_coe_symm {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] (I : ModelWithCorners π•œ E H) (I' : ModelWithCorners π•œ E' H') :
                            ↑(I.prod I').symm = Prod.map ↑I.symm ↑I'.symm
                            theorem modelWithCornersSelf_prod {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ F] :
                            modelWithCornersSelf π•œ (E Γ— F) = (modelWithCornersSelf π•œ E).prod (modelWithCornersSelf π•œ F)

                            This lemma should be erased, or at least burn in hell, as it uses bad defeq: the left model with corners is for E times F, the right one for ModelProd E F, and there's a good reason we are distinguishing them.

                            theorem ModelWithCorners.range_prod {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace π•œ F] {H : Type u_5} [TopologicalSpace H] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners π•œ E H} {J : ModelWithCorners π•œ F G} :
                            Set.range ↑(I.prod J) = Set.range ↑I Γ—Λ’ Set.range ↑J
                            class ModelWithCorners.Boundaryless {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) :

                            Property ensuring that the model with corners I defines manifolds without boundary. This differs from the more general BoundarylessManifold, which requires every point on the manifold to be an interior point.

                            Instances
                              theorem ModelWithCorners.range_eq_univ {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) [I.Boundaryless] :
                              def ModelWithCorners.toHomeomorph {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) [I.Boundaryless] :

                              If I is a ModelWithCorners.Boundaryless model, then it is a homeomorphism.

                              Equations
                              Instances For
                                @[simp]
                                theorem ModelWithCorners.toHomeomorph_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) [I.Boundaryless] (a✝ : H) :
                                I.toHomeomorph a✝ = ↑I a✝
                                @[simp]
                                theorem ModelWithCorners.toHomeomorph_symm_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) [I.Boundaryless] (a✝ : E) :
                                I.toHomeomorph.symm a✝ = ↑I.symm a✝
                                instance modelWithCornersSelf_boundaryless (π•œ : Type u_1) [NontriviallyNormedField π•œ] (E : Type u_2) [NormedAddCommGroup E] [NormedSpace π•œ E] :

                                The trivial model with corners has no boundary

                                instance ModelWithCorners.range_eq_univ_prod {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type w} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) [I.Boundaryless] {E' : Type v'} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {H' : Type w'} [TopologicalSpace H'] (I' : ModelWithCorners π•œ E' H') [I'.Boundaryless] :

                                If two model with corners are boundaryless, their product also is

                                C^n functions on models with corners #

                                def contDiffPregroupoid (n : WithTop β„•βˆž) {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) :

                                Given a model with corners (E, H), we define the pregroupoid of C^n transformations of H as the maps that are C^n when read in E through I.

                                Equations
                                Instances For
                                  def contDiffGroupoid (n : WithTop β„•βˆž) {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) :

                                  Given a model with corners (E, H), we define the groupoid of invertible C^n transformations of H as the invertible maps that are C^n when read in E through I.

                                  Equations
                                  Instances For
                                    theorem contDiffGroupoid_le {m n : WithTop β„•βˆž} {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners π•œ E H} (h : m ≀ n) :

                                    Inclusion of the groupoid of C^n local diffeos in the groupoid of C^m local diffeos when m ≀ n

                                    theorem contDiffGroupoid_zero_eq {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners π•œ E H} :

                                    The groupoid of 0-times continuously differentiable maps is just the groupoid of all partial homeomorphisms

                                    theorem ContDiffGroupoid.mem_of_source_eq_empty {n : WithTop β„•βˆž} {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners π•œ E H} (f : PartialHomeomorph H H) (hf : f.source = βˆ…) :

                                    Any change of coordinates with empty source belongs to contDiffGroupoid.

                                    theorem ContinuousGroupoid.mem_of_source_eq_empty {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners π•œ E H} (f : PartialHomeomorph H H) (hf : f.source = βˆ…) :

                                    Any change of coordinates with empty source belongs to continuousGroupoid.

                                    theorem ofSet_mem_contDiffGroupoid {n : WithTop β„•βˆž} {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners π•œ E H} {s : Set H} (hs : IsOpen s) :

                                    An identity partial homeomorphism belongs to the C^n groupoid.

                                    theorem symm_trans_mem_contDiffGroupoid {n : WithTop β„•βˆž} {π•œ : 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] (e : PartialHomeomorph M H) :

                                    The composition of a partial homeomorphism from H to M and its inverse belongs to the C^n groupoid.

                                    theorem contDiffGroupoid_prod {n : WithTop β„•βˆž} {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] {E' : Type u_5} {H' : Type u_6} [NormedAddCommGroup E'] [NormedSpace π•œ E'] [TopologicalSpace H'] {I : ModelWithCorners π•œ E H} {I' : ModelWithCorners π•œ E' H'} {e : PartialHomeomorph H H} {e' : PartialHomeomorph H' H'} (he : e ∈ contDiffGroupoid n I) (he' : e' ∈ contDiffGroupoid n I') :

                                    The product of two C^n partial homeomorphisms is C^n.

                                    The C^n groupoid is closed under restriction.

                                    C^n manifolds (possibly with boundary or corners) #

                                    class IsManifold {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) (n : WithTop β„•βˆž) (M : Type u_4) [TopologicalSpace M] [ChartedSpace H M] extends HasGroupoid M (contDiffGroupoid n I) :

                                    Typeclass defining manifolds with respect to a model with corners, over a field π•œ. This definition includes the model with corners I (which might allow boundary, corners, or not, so this class covers both manifolds with boundary and manifolds without boundary), and a smoothness parameter n : WithTop β„•βˆž (where n = 0 means topological manifold, n = ∞ means smooth manifold and n = Ο‰ means analytic manifold).

                                    Instances
                                      @[deprecated IsManifold (since := "2025-01-09")]
                                      def SmoothManifoldWithCorners {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) (n : WithTop β„•βˆž) (M : Type u_4) [TopologicalSpace M] [ChartedSpace H M] :

                                      Alias of IsManifold.


                                      Typeclass defining manifolds with respect to a model with corners, over a field π•œ. This definition includes the model with corners I (which might allow boundary, corners, or not, so this class covers both manifolds with boundary and manifolds without boundary), and a smoothness parameter n : WithTop β„•βˆž (where n = 0 means topological manifold, n = ∞ means smooth manifold and n = Ο‰ means analytic manifold).

                                      Equations
                                      Instances For
                                        theorem IsManifold.mk' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) (n : WithTop β„•βˆž) (M : Type u_4) [TopologicalSpace M] [ChartedSpace H M] [gr : HasGroupoid M (contDiffGroupoid n I)] :

                                        Building a C^n manifold from a HasGroupoid assumption.

                                        @[deprecated IsManifold.mk' (since := "2025-01-09")]
                                        theorem SmoothManifoldWithCorners.mk' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) (n : WithTop β„•βˆž) (M : Type u_4) [TopologicalSpace M] [ChartedSpace H M] [gr : HasGroupoid M (contDiffGroupoid n I)] :

                                        Alias of IsManifold.mk'.


                                        Building a C^n manifold from a HasGroupoid assumption.

                                        theorem isManifold_of_contDiffOn {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) (n : WithTop β„•βˆž) (M : Type u_4) [TopologicalSpace M] [ChartedSpace H M] (h : βˆ€ (e e' : PartialHomeomorph M H), e ∈ atlas H M β†’ e' ∈ atlas H M β†’ ContDiffOn π•œ n (↑I ∘ ↑(e.symm.trans e') ∘ ↑I.symm) (↑I.symm ⁻¹' (e.symm.trans e').source ∩ Set.range ↑I)) :
                                        @[deprecated isManifold_of_contDiffOn (since := "2025-01-09")]
                                        theorem smoothManifoldWithCorners_of_contDiffOn {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) (n : WithTop β„•βˆž) (M : Type u_4) [TopologicalSpace M] [ChartedSpace H M] (h : βˆ€ (e e' : PartialHomeomorph M H), e ∈ atlas H M β†’ e' ∈ atlas H M β†’ ContDiffOn π•œ n (↑I ∘ ↑(e.symm.trans e') ∘ ↑I.symm) (↑I.symm ⁻¹' (e.symm.trans e').source ∩ Set.range ↑I)) :

                                        Alias of isManifold_of_contDiffOn.

                                        instance instIsManifoldModelSpace {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} :

                                        For any model with corners, the model space is a C^n manifold

                                        @[deprecated instIsManifoldModelSpace (since := "2025-04-22")]
                                        theorem intIsManifoldModelSpace {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} :

                                        Alias of instIsManifoldModelSpace.


                                        For any model with corners, the model space is a C^n manifold

                                        theorem IsManifold.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] {m n : WithTop β„•βˆž} (hmn : m ≀ n) [IsManifold I n M] :

                                        A typeclass registering that a smoothness exponent is smaller than ∞. Used to deduce that some manifolds are C^n when they are C^∞.

                                        Instances
                                          instance IsManifold.instOfSomeENatTopOfLEInfty {π•œ : 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] {a : WithTop β„•βˆž} [IsManifold I (β†‘βŠ€) M] [h : ENat.LEInfty a] :
                                          instance IsManifold.instOfTopWithTopENat {π•œ : 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] {a : WithTop β„•βˆž} [IsManifold I ⊀ M] :
                                          instance IsManifold.instOfNatWithTopENat {π•œ : 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] :
                                          instance IsManifold.instOfNatWithTopENat_1 {π•œ : 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] [IsManifold I 2 M] :
                                          instance IsManifold.instOfNatWithTopENat_2 {π•œ : 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] [IsManifold I 3 M] :
                                          def IsManifold.maximalAtlas {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) (n : WithTop β„•βˆž) (M : Type u_4) [TopologicalSpace M] [ChartedSpace H M] :

                                          The maximal atlas of M for the C^n manifold with corners structure corresponding to the model with corners I.

                                          Equations
                                          Instances For
                                            theorem IsManifold.subset_maximalAtlas {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I n M] :
                                            theorem IsManifold.chart_mem_maximalAtlas {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I n M] (x : M) :
                                            theorem IsManifold.compatible_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} {n : WithTop β„•βˆž} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {e e' : PartialHomeomorph M H} (he : e ∈ maximalAtlas I n M) (he' : e' ∈ maximalAtlas I n M) :
                                            theorem IsManifold.maximalAtlas_subset_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] {m n : WithTop β„•βˆž} (h : m ≀ n) :
                                            instance IsManifold.empty {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners π•œ E H} (n : WithTop β„•βˆž) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsEmpty M] :

                                            The empty set is a C^n manifold w.r.t. any charted space and model.

                                            theorem IsManifold.of_discreteTopology {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] (n : WithTop β„•βˆž) {M : Type u_4} [TopologicalSpace M] [DiscreteTopology M] [Unique E] :

                                            A discrete space M is a smooth manifold over the trivial model on a trivial normed space.

                                            instance IsManifold.prod {n : WithTop β„•βˆž} {π•œ : Type u_5} [NontriviallyNormedField π•œ] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace π•œ E] {E' : Type u_7} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {H : Type u_8} [TopologicalSpace H] {I : ModelWithCorners π•œ E H} {H' : Type u_9} [TopologicalSpace H'] {I' : ModelWithCorners π•œ E' H'} (M : Type u_10) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I n M] (M' : Type u_11) [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' n M'] :
                                            IsManifold (I.prod I') n (M Γ— M')

                                            The product of two C^n manifolds is naturally a C^n manifold.

                                            instance IsManifold.disjointUnion {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_5} [TopologicalSpace M'] [ChartedSpace H M'] [hM : IsManifold I n M] [hM' : IsManifold I n M'] :
                                            IsManifold I n (M βŠ• M')

                                            The disjoint union of two C^n manifolds modelled on (E, H) is a C^n manifold modeled on (E, H).

                                            theorem PartialHomeomorph.isManifold_singleton {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {M : Type u_4} [TopologicalSpace M] (e : PartialHomeomorph M H) (h : e.source = Set.univ) :
                                            @[deprecated PartialHomeomorph.isManifold_singleton (since := "2025-01-09")]
                                            theorem PartialHomeomorph.singleton_smoothManifoldWithCorners {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {M : Type u_4} [TopologicalSpace M] (e : PartialHomeomorph M H) (h : e.source = Set.univ) :

                                            Alias of PartialHomeomorph.isManifold_singleton.

                                            theorem Topology.IsOpenEmbedding.isManifold_singleton {π•œ : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField π•œ] [NormedAddCommGroup E] [NormedSpace π•œ E] [TopologicalSpace H] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {M : Type u_4} [TopologicalSpace M] [Nonempty M] {f : M β†’ H} (h : IsOpenEmbedding f) :
                                            @[deprecated Topology.IsOpenEmbedding.isManifold_singleton (since := "2025-01-09")]
                                            theorem Topology.IsOpenEmbedding.singleton_smoothManifoldWithCorners {π•œ : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField π•œ] [NormedAddCommGroup E] [NormedSpace π•œ E] [TopologicalSpace H] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {M : Type u_4} [TopologicalSpace M] [Nonempty M] {f : M β†’ H} (h : IsOpenEmbedding f) :

                                            Alias of Topology.IsOpenEmbedding.isManifold_singleton.

                                            instance TopologicalSpace.Opens.instIsManifoldSubtypeMem {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I n M] (s : Opens M) :
                                            IsManifold I n β†₯s
                                            def TangentSpace {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] (_x : M) :

                                            The tangent space at a point of the manifold M. It is just E. We could use instead (tangentBundleCore I M).to_topological_vector_bundle_core.fiber x, but we use E to help the kernel.

                                            Equations
                                            Instances For
                                              instance instAddCommGroupTangentSpace {π•œ : 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] {x : M} :
                                              Equations
                                              instance instIsTopologicalAddGroupTangentSpace {π•œ : 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] {x : M} :
                                              instance instModuleTangentSpace {π•œ : 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] {x : M} :
                                              Module π•œ (TangentSpace I x)
                                              Equations
                                              instance instInhabitedTangentSpace {π•œ : 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] {x : M} :
                                              Equations
                                              @[reducible, inline]
                                              abbrev TangentBundle {π•œ : 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] :
                                              Type (max u_4 u_2)

                                              The tangent bundle to a manifold, as a Sigma type. Defined in terms of Bundle.TotalSpace to be able to put a suitable topology on it.

                                              Equations
                                              Instances For