ModelWithCorners.image_eq
theorem ModelWithCorners.image_eq :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners ๐ E H) (s : Set H),
โI '' s = โI.symm โปยน' s โฉ Set.range โI
This theorem states that for any type `๐` that is a nontrivially normed field, any type `E` that is a normed additive commutative group and a normed space over `๐`, and any type `H` that is a topological space, given a ModelWithCorners `I` from `๐` to `E` to `H` and a set `s` of type `H`, the image of `s` under `I` is equal to the intersection of the preimage of `s` under the inverse of `I` and the range of `I`. In other words, it's stating that applying a function to a set and then applying the inverse function returns the original set, assuming the functions are well-behaved in a certain mathematical sense.
More concisely: For any nontrivially normed field `๐`, normed additive commutative group and normed space `E` over `๐`, topological space `H`, ModelWithCorners `I` from `๐` to `E` to `H`, and set `s` in `H`, the image of `s` under `I` equals the intersection of the preimage of `s` under `Iโปยน` and the range of `I`.
|
ofSet_mem_contDiffGroupoid
theorem ofSet_mem_contDiffGroupoid :
โ (n : โโ) {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners ๐ E H) {s : Set H}
(hs : IsOpen s), PartialHomeomorph.ofSet s hs โ contDiffGroupoid n I
The theorem `ofSet_mem_contDiffGroupoid` states that for any natural number `n` (which could be infinity), a given type `๐` that is a nontrivially normed field, a given type `E` that is a normed additive commutative group and a normed space over `๐`, a given type `H` that is a topological space, a model `I` with corners of type `๐`, `E`, `H`, and a set `s` of `H` that is open in the topological space `H`, the identity partial homeomorphism on the set `s` belongs to the `C^n` groupoid. In other words, the identity map which is a homeomorphism from an open set `s` to itself, is also `C^n`-differentiable, where `C^n` refers to the class of functions which have continuous derivatives up to order `n`.
More concisely: For any nontrivially normed field `๐`, normed additive commutative group and normed space `E` over `๐`, topological space `H`, open set `s` in `H`, and identity partial homeomorphism on `s`, the identity map is a `C^n`-differentiable function from `s` to itself.
|
PartialHomeomorph.map_extend_nhdsWithin_eq_image
theorem PartialHomeomorph.map_extend_nhdsWithin_eq_image :
โ {๐ : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField ๐]
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ๐ E] [inst_3 : TopologicalSpace H]
[inst_4 : TopologicalSpace M] (f : PartialHomeomorph M H) (I : ModelWithCorners ๐ E H) {s : Set M} {y : M},
y โ f.source โ
Filter.map (โ(f.extend I)) (nhdsWithin y s) =
nhdsWithin (โ(f.extend I) y) (โ(f.extend I) '' ((f.extend I).source โฉ s))
The theorem `PartialHomeomorph.map_extend_nhdsWithin_eq_image` states that for any non-trivially normed field `๐`, a normed add commutative group `E`, a normed space `๐ E`, and topological spaces `M` and `H`, given a partial homeomorphism `f` from `M` to `H`, a Model with Corners `I` from `๐` to `E` and `H`, a set `s` of `M`, and an element `y` of `M` that belongs to the source of `f`, the forward map of the "neighborhood within" filter of `y` and `s` using the extension of the partial homeomorphism equals the "neighborhood within" filter of the image of `y` under the extension of the partial homeomorphism, and the image of the intersection of the source of the extension of the partial homeomorphism and `s`.
More concisely: For a non-trivially normed field `๐`, a normed add commutative group `E`, a normed space `๐ E`, topological spaces `M` and `H`, a partial homeomorphism `f` from `M` to `H`, a Model with Corners `I` from `๐` to `E` and `H`, and a set `s` of `M` and an element `y` of `M` in the domain of `f`, the neighborhood filters of `y` and the image of `y` under the extension of `f`, with respect to the neighborhood within relation, are equal.
|
contDiffGroupoid_le
theorem contDiffGroupoid_le :
โ {m n : โโ} {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners ๐ E H),
m โค n โ contDiffGroupoid n I โค contDiffGroupoid m I
The given theorem states that for any non-trivially normed field `๐`, any normed add commutative group `E` over `๐`, and any topological space `H` with a model with corners `I`, if we consider the groupoid of `C^n` and `C^m` local diffeomorphisms (smooth maps with a smooth inverse), then the groupoid of `C^n` local diffeomorphisms is included in the groupoid of `C^m` local diffeomorphisms when `m` is less than or equal to `n`. In other words, if a transformation is smooth to degree `n`, it is also smooth to any lesser degree `m`.
More concisely: For any non-trivially normed field `๐`, any normed add commutative group `E` over `๐`, and any topological space `H` with a model of corners `I`, the groupoid of `C^n` local diffeomorphisms is a subgroupoid of the groupoid of `C^m` local diffeomorphisms for `m <= n`.
|
symm_trans_mem_analyticGroupoid
theorem symm_trans_mem_analyticGroupoid :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners ๐ E H)
{M : Type u_4} [inst_4 : TopologicalSpace M] (e : PartialHomeomorph M H), e.symm.trans e โ analyticGroupoid I
This theorem states that for any non-trivially normed field `๐`, any normed add commutative group `E` over `๐`, any topological space `H`, any model `I` with corners using `๐`, `E`, and `H`, any topological space `M`, and any partial homeomorphism `e` from `M` to `H`, the composition of the inverse of `e` and `e` itself belongs to the analytic groupoid associated with the model `I`.
More concisely: For any non-trivially normed field `๐`, any normed add commutative group `E` over `๐`, any model `I` with corners using `๐`, `E`, and a topological space `H`, any topological space `M`, and any partial homeomorphism `e` from `M` to `H`, the composition of `e` and its inverse belongs to the analytic groupoid of `I`.
|
ModelWithCorners.left_inv
theorem ModelWithCorners.left_inv :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners ๐ E H) (x : H),
โI.symm (โI x) = x
The theorem `ModelWithCorners.left_inv` states that for any nontrivially normed field `๐`, any normed add commutative group `E` over `๐`, and any topological space `H`, if `I` is a model with corners from `E` to `H` and `x` is an element of `H`, then applying the inverse operation `ModelWithCorners.symm` to the result of applying `I` to `x` gives us back `x`. In essence, this is a theorem about the left-inverse property of the model with corners, which asserts that applying the model and then its inverse leaves any space element unchanged.
More concisely: For any nontrivially normed field `๐`, normed add commutative group `E` over `๐`, topological space `H`, and a model with corners `I` from `E` to `H`, `ModelWithCorners.symm โ I = id_H`, where `id_H` is the identity function on `H`.
|
PartialHomeomorph.map_extend_symm_nhdsWithin
theorem PartialHomeomorph.map_extend_symm_nhdsWithin :
โ {๐ : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField ๐]
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ๐ E] [inst_3 : TopologicalSpace H]
[inst_4 : TopologicalSpace M] (f : PartialHomeomorph M H) (I : ModelWithCorners ๐ E H) {s : Set M} {y : M},
y โ f.source โ
Filter.map (โ(f.extend I).symm) (nhdsWithin (โ(f.extend I) y) (โ(f.extend I).symm โปยน' s โฉ Set.range โI)) =
nhdsWithin y s
The theorem `PartialHomeomorph.map_extend_symm_nhdsWithin` states that for any non-trivially normed field `๐`, normed add commutative group `E`, normed space `E` over `๐`, topological spaces `H` and `M`, a partial homeomorphism `f` from `M` to `H`, a model with corners `I` from `๐` to `E` to `H`, a set `s` in `M`, and a point `y` in `M` that is in the source of `f`, the forward map of the neighborhood within filter of `(โ(PartialHomeomorph.extend f I) y)` in the set `((โ(PartialEquiv.symm (PartialHomeomorph.extend f I)) โปยน' s) โฉ Set.range โI)` under the inverse of the partial equivalence of the extension of `f` using `I` is equal to the neighborhood within filter of `y` in `s`.
In simple terms, this theorem involves the mapping from one local neighbourhood to another in the context of partial homeomorphisms and topological spaces.
More concisely: For a non-trivially normed field `๐`, normed add commutative group `E`, normed space `E` over `๐`, topological spaces `H` and `M`, a partial homeomorphism `f` from `M` to `H`, a model with corners `I` from `๐` to `E` to `H`, and a set `s` in `M` with `y` in `s` being in the domain of `f`, the neighborhood filter of `(f(y))` in `(f(s))` is equal to the neighborhood filter of `y` in `s`, under the inverse of the partial equivalence of the extension of `f` using `I`.
|
PartialHomeomorph.extend_target
theorem PartialHomeomorph.extend_target :
โ {๐ : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField ๐]
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ๐ E] [inst_3 : TopologicalSpace H]
[inst_4 : TopologicalSpace M] (f : PartialHomeomorph M H) (I : ModelWithCorners ๐ E H),
(f.extend I).target = โI.symm โปยน' f.target โฉ Set.range โI
The theorem `PartialHomeomorph.extend_target` takes in a non-trivially normed field `๐`, a normed add commutative group `E`, a normed space over `๐` and `E`, and two topological spaces `M` and `H`. The theorem also takes in a partial homeomorphism `f` from `M` to `H`, and a ModelWithCorners `I` from `๐` to `E` to `H`. The theorem states that the target of the extension of the partial homeomorphism `f` using `I` is equal to the preimage of the target of `f` under the inverse of `I`, intersected with the range of `I`. This theorem essentially relates the target of the extended partial homeomorphism with the target of the original partial homeomorphism and the model with corners.
More concisely: The theorem asserts that the target of the extension of a partial homeomorphism between topological spaces using a ModelWithCorners is equal to the preimage of the original target under the inverse of the ModelWithCorners, intersected with the range of the ModelWithCorners.
|
extChartAt_preimage_inter_eq
theorem extChartAt_preimage_inter_eq :
โ {๐ : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField ๐]
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ๐ E] [inst_3 : TopologicalSpace H]
[inst_4 : TopologicalSpace M] (I : ModelWithCorners ๐ E H) {s t : Set M} [inst_5 : ChartedSpace H M] (x : M),
โ(extChartAt I x).symm โปยน' (s โฉ t) โฉ Set.range โI =
โ(extChartAt I x).symm โปยน' s โฉ Set.range โI โฉ โ(extChartAt I x).symm โปยน' t
This theorem states that for any nontrivially normed field `๐`, normed add commutative group `E`, normed space `๐ E`, topological spaces `H` and `M`, model with corners `I` (a structural framework for manifold concepts) relating `๐`, `E` and `H`, sets `s` and `t` of type `M`, and any charted space `H M`, for any point `x` in `M`, the preimage of the intersection of `s` and `t` under the inverse of an extended chart at `x` intersected with the range of `I` is equal to the intersection of the preimage of `s` under the same inverse extended chart and the range of `I`, intersected with the preimage of `t` under the same inverse extended chart. This is a technical lemma used to rewrite the preimage of an intersection under an extended chart in a form that is convenient for applying derivative theorems.
More concisely: For any nontrivially normed field `๐`, normed add commutative group `E`, normed space `๐ E`, topological spaces `H` and `M`, model with corners `I`, sets `s` and `t` in `M`, and charted space `H M`, the preimage of `s โฉ t` under an extended chart at a point `x` in `M` equals the intersection of the preimages of `s` and `t` under the same chart, intersected with the range of `I`.
|
contDiffGroupoid_zero_eq
theorem contDiffGroupoid_zero_eq :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners ๐ E H),
contDiffGroupoid 0 I = continuousGroupoid H
The theorem `contDiffGroupoid_zero_eq` states that for any non-trivially normed field `๐`, normed additive commutative group `E`, normed space `E` over `๐`, and topological space `H`, along with a model with corners `I` of `๐`, `E` and `H`, the groupoid of `0`-times continuously differentiable maps (represented by `contDiffGroupoid 0 I`) is equivalent to the groupoid of all partial homeomorphisms on the topological space `H` (represented by `continuousGroupoid H`).
In other words, in this setting, zero times continuously differentiable maps correspond exactly to partial homeomorphisms.
More concisely: The groupoid of zero-times continuously differentiable maps from a non-trivially normed field to a normed additive commutative group and a topological space is equivalent to the groupoid of partial homeomorphisms on the topological space.
|
extChartAt_model_space_eq_id
theorem extChartAt_model_space_eq_id :
โ (๐ : Type u_1) {E : Type u_2} [inst : NontriviallyNormedField ๐] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] (x : E), extChartAt (modelWithCornersSelf ๐ E) x = PartialEquiv.refl E
This theorem states that for any vector space, when viewed as a manifold, its extended charts are simply the identity map. More specifically, for any non-trivial normed field ๐, and any type E that forms a normed additive commutative group and has a normed space structure over ๐, the extended chart at any point x in E, when using the model with corners associated to the vector space itself, is just the identity partial equivalence on E.
More concisely: For any normed vector space over a non-trivial normed field, the extended charts are equal to the identity map when viewed as a manifold.
|
PartialHomeomorph.extend_preimage_inter_eq
theorem PartialHomeomorph.extend_preimage_inter_eq :
โ {๐ : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField ๐]
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ๐ E] [inst_3 : TopologicalSpace H]
[inst_4 : TopologicalSpace M] (f : PartialHomeomorph M H) (I : ModelWithCorners ๐ E H) {s t : Set M},
โ(f.extend I).symm โปยน' (s โฉ t) โฉ Set.range โI =
โ(f.extend I).symm โปยน' s โฉ Set.range โI โฉ โ(f.extend I).symm โปยน' t
This theorem states that for any nontrivially-normed field ๐, normed add commutative group E, normed space over ๐ E, topological spaces H and M, a partial homeomorphism `f` from M to H, a model with corners `I` from ๐ to E to H, and any sets `s` and `t` of type M, the preimage of the intersection of `s` and `t` under the inverse of the extension of `f` by `I`, intersected with the range of `I`, is equal to the intersection of the preimage of `s` under the inverse of the extension, the range of `I`, and the preimage of `t`. In simpler terms, this theorem is a technical lemma used in the context of differential geometry to manipulate the preimage of the intersection of two sets under an extension of a partial homeomorphism, making it easier to apply theorems related to derivatives.
More concisely: For any nontrivially-normed field ๐, normed add commutative group E, topological spaces H and M, a partial homeomorphism `f` from M to H, a model with corners `I` from ๐ to E to H, and sets `s` and `t` in M, the inverse image of `s โฉ t` under `Iโปยน โ fโปยน` equals the intersection of the inverse image of `s` under `Iโปยน`, the inverse image of `t` under `Iโปยน`, and the range of `I`.
|
PartialHomeomorph.extend_source
theorem PartialHomeomorph.extend_source :
โ {๐ : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField ๐]
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ๐ E] [inst_3 : TopologicalSpace H]
[inst_4 : TopologicalSpace M] (f : PartialHomeomorph M H) (I : ModelWithCorners ๐ E H),
(f.extend I).source = f.source
This theorem states that for any non-trivially normed field `๐`, normed addition commutative group `E`, normed space `๐ E`, and topological spaces `H` and `M`, given a partial homeomorphism `f` from `M` to `H` and a model with corners `I` on `๐ E H`, the source of the extended partial homeomorphism `f` through `I` is equal to the source of `f`. In other words, extending a partial homeomorphism via a model with corners doesn't change its source.
More concisely: For any non-trivially normed field `๐`, normed addition commutative group `E`, normed space `๐ E`, topological spaces `H` and `M`, a partial homeomorphism `f` from `M` to `H`, and a model with corners `I` on `๐ E H`, the source of the extended partial homeomorphism `f` through `I` equals the source of `f`.
|
ModelWithCorners.continuous
theorem ModelWithCorners.continuous :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners ๐ E H),
Continuous โI
This theorem states that for any non-trivially normed field `๐`, normed add commutative group `E`, topological space `H`, and a model with corners `I : ModelWithCorners ๐ E H`, the model with corners `I` is continuous. In other words, the function represented by the model with corners respects the topology of the spaces it maps between, not tearing or gluing points apart.
More concisely: For any non-trivially normed field `๐`, normed additive group `E`, topological space `H`, and `I : ModelWithCorners ๐ E H`, the function represented by `I` is continuous.
|
PartialHomeomorph.isOpen_extend_source
theorem PartialHomeomorph.isOpen_extend_source :
โ {๐ : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField ๐]
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ๐ E] [inst_3 : TopologicalSpace H]
[inst_4 : TopologicalSpace M] (f : PartialHomeomorph M H) (I : ModelWithCorners ๐ E H),
IsOpen (f.extend I).source
This theorem states that for any non-trivially normed field `๐`, normed additive commutative group `E`, normed space `E` over `๐`, and topological spaces `H` and `M`, given a partial homeomorphism `f` from `M` to `H` and a model with corners `I` on `๐`, `E`, and `H`, the source set of the extension of the partial homeomorphism `f` by the model with corners `I` is an open set in the ambient topological space on `M`.
More concisely: For any non-trivially normed field `๐`, normed additive commutative group `E`, and topological spaces `H` and `M`, given a partial homeomorphism `f` from `M` to `H`, and a model with corners `I` on `๐`, `E`, and `H`, the source set of the extension of `f` by `I` is open in `M`.
|
ModelWithCorners.right_inv
theorem ModelWithCorners.right_inv :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners ๐ E H) {x : E},
x โ Set.range โI โ โI (โI.symm x) = x
This theorem, `ModelWithCorners.right_inv`, states that for any nontrivially normed field `๐`, a normed add commutative group `E` which is also a normed space over `๐`, and a topological space `H`, given a model with corners `I` from `๐` to `E` to `H` and any element `x` from `E`, if `x` is in the range of `I`, then applying `I` to the inverse of `I` applied to `x` gives back `x`. In simpler terms, `I` and its inverse cancel each other out when `x` is in the range of `I`.
More concisely: For any nontrivially normed field `๐`, normed add commutative group `E` over `๐`, and topological space `H`, if `I` is a model with corners from `๐` to `E` to `H` and `x` is in the range of `I`, then `I (I x) = x`.
|
Manifold.locallyCompact_of_finiteDimensional
theorem Manifold.locallyCompact_of_finiteDimensional :
โ {E : Type u_1} {๐ : Type u_2} [inst : NontriviallyNormedField ๐] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_3} [inst_3 : TopologicalSpace H],
ModelWithCorners ๐ E H โ
โ {M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : LocallyCompactSpace ๐]
[inst : FiniteDimensional ๐ E], LocallyCompactSpace M
The theorem `Manifold.locallyCompact_of_finiteDimensional` states that in the context of a nontrivially normed field `๐` and a normed additive commutative group `E` that forms a normed space over `๐`, if we have a manifold `M` modeled with corners on a topological space `H` and `E`, and both `๐` and `E` are locally compact with `E` being a finite-dimensional space over `๐`, then the manifold `M` is also locally compact. This theorem holds for models on locally compact fields such as the real numbers โ, complex numbers โ, or the p-adic numbers.
More concisely: If `M` is a manifold modeled with corners on a topological space `H` and `E` is a finite-dimensional, normed space over a locally compact normed field `๐`, then `M` is locally compact.
|
ofSet_mem_analyticGroupoid
theorem ofSet_mem_analyticGroupoid :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners ๐ E H) {s : Set H}
(hs : IsOpen s), PartialHomeomorph.ofSet s hs โ analyticGroupoid I
This theorem states that for any nontrivially normed field `๐`, any normed additive commutative group `E`, any normed space `E` over `๐`, any topological space `H`, any model with corners `I` of `E` with respect to `H`, and any open set `s` in `H`, the identity partial homeomorphism of the set `s` (defined by `PartialHomeomorph.ofSet`) belongs to the analytic groupoid determined by the model with corners `I`. In other words, this identity partial homeomorphism preserves the analytic structure defined by the model with corners `I`.
More concisely: For any nontrivially normed field `๐`, normed additive commutative group `E` over `๐`, topological space `H`, model with corners `I` of `E` with respect to `H`, and open set `s` in `H`, the identity partial homeomorphism of `s` belongs to the analytic groupoid of `I`.
|
extChartAt_preimage_mem_nhds
theorem extChartAt_preimage_mem_nhds :
โ {๐ : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField ๐]
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ๐ E] [inst_3 : TopologicalSpace H]
[inst_4 : TopologicalSpace M] (I : ModelWithCorners ๐ E H) {t : Set M} [inst_5 : ChartedSpace H M] {x : M},
t โ nhds x โ โ(extChartAt I x).symm โปยน' t โ nhds (โ(extChartAt I x) x)
This theorem, named `extChartAt_preimage_mem_nhds`, states that for any point 'x' in a topological space 'M', equipped with additional structures like a Model (`ModelWithCorners`), if a set 't' is a neighborhood of 'x' (namely, 't' is in the neighborhood filter of 'x', denoted as 't โ nhds x'), then the preimage of 't' under the inverse of an extended chart at 'x' is also a neighborhood of the image of 'x' under the extended chart (i.e., 'โ(extChartAt I x).symm โปยน' t โ nhds (โ(extChartAt I x) x)'). Here, 'extChartAt I x' is a mapping from the model space to the topological space, and its inverse '.symm' pulls back neighborhoods from the model space to the topological space. This theorem is a key technical result in the theory of manifolds, ensuring that neighborhoods behave well under the transition maps between different charts.
More concisely: For any point x in a topological space M with additional structures, if t is a neighborhood of x and extChartAt I x is an extended chart at x, then the preimage of t under the inverse of extChartAt I x is a neighborhood of the image of x under extChartAt I x.
|
PartialHomeomorph.map_extend_nhdsWithin
theorem PartialHomeomorph.map_extend_nhdsWithin :
โ {๐ : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField ๐]
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ๐ E] [inst_3 : TopologicalSpace H]
[inst_4 : TopologicalSpace M] (f : PartialHomeomorph M H) (I : ModelWithCorners ๐ E H) {s : Set M} {y : M},
y โ f.source โ
Filter.map (โ(f.extend I)) (nhdsWithin y s) =
nhdsWithin (โ(f.extend I) y) (โ(f.extend I).symm โปยน' s โฉ Set.range โI)
This theorem states that for any nontrivially normed field `๐`, a normed add commutative group `E`, a normed space `E` over `๐`, and topological spaces `M` and `H`, given a partial homeomorphism `f` from `M` to `H`, a model with corners `I` from `๐`-based `E` to `H`, a set `s` of `M`, and an element `y` of `M` such that `y` is in the source of `f`, the map of the neighborhood filter within `s` at `y` under the extension of `f` by `I` is equal to the neighborhood filter within the preimage of `s` under the inverse of the extension of `f` by `I` and the range of `I` at the image of `y` under the extension of `f` by `I`.
In other words, extending the partial homeomorphism and then mapping the filter of neighborhoods corresponds to first mapping under the extended homeomorphism, and then taking the filter of neighborhoods within the preimage and range. This is a property relating the extension of homeomorphisms, filters, and inverse mappings in a specific topological and normed context.
More concisely: For any nontrivially normed field `๐`, a normed add commutative group `E` over `๐`, and topological spaces `M` and `H`, given a partial homeomorphism `f` from `M` to `H`, a model with corners `I` from `๐`-based `E` to `H`, and an element `y` in `M` with image `z` in `H`, the neighborhood filters of `y` in `s` under `f` by `I` equal the neighborhood filters of `z` in `f(s)` under the inverse of `f` by `I` and the range of `I` at `z`.
|
mem_extChartAt_source
theorem mem_extChartAt_source :
โ {๐ : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField ๐]
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ๐ E] [inst_3 : TopologicalSpace H]
[inst_4 : TopologicalSpace M] (I : ModelWithCorners ๐ E H) [inst_5 : ChartedSpace H M] (x : M),
x โ (extChartAt I x).source
This theorem states that for any point `x` in a charted space `M` with a given model with corners `I`, `x` is an element of the source set of the extended chart at `x`. Here, the necessary conditions include `M` being a topological space that is charted over another topological space `H` with the model with corners `I`, `E` being a normed additive commutative group that is also a normed space over the nontrivially normed field `๐`, and `H` being a topological space.
More concisely: For any point `x` in a charted topological space `M` over `H` with model `I`, `x` lies in the source set of the extended chart at `x`, where `M` is a topological space over `H`, `H` is a topological space, and `I` is a model with corners for a normed additive commutative group `E` over a nontrivially normed field `๐`.
|
PartialHomeomorph.extend_coord_change_source
theorem PartialHomeomorph.extend_coord_change_source :
โ {๐ : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField ๐]
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ๐ E] [inst_3 : TopologicalSpace H]
[inst_4 : TopologicalSpace M] (f f' : PartialHomeomorph M H) (I : ModelWithCorners ๐ E H),
((f.extend I).symm.trans (f'.extend I)).source = โI '' (f.symm.trans f').source
The theorem `PartialHomeomorph.extend_coord_change_source` states that for any nontrivially normed field `๐`, normed add commutative group `E`, any types `M` and `H` both with a topological space structure, any two partial homeomorphisms `f` and `f'` from `M` to `H`, and any model with corners `I` from `๐` to `E` to `H`, the source of the partial equivalence obtained by transforming the extension of `f` through `I` to a partial equivalence, taking the inverse, then composing it with the extension of `f'` through `I`, is the image under `I` of the source of the partial homeomorphism obtained by first taking the inverse of `f` then composing it with `f'`. This theorem is about the compatibility of the extension and inverse operations on partial homeomorphisms and model with corners with the source operation on partial equivalences and homeomorphisms.
More concisely: Given a nontrivially normed field `๐`, normed add commutative group `E`, types `M` and `H` with topological space structures, partial homeomorphisms `f` and `f'` from `M` to `H`, and a model with corners `I` from `๐` to `E` to `H`, the sources of the partial equivalences obtained by transforming and composing the inverses and extensions of `f` and `f'` through `I` are equal.
|
PartialHomeomorph.extend_preimage_mem_nhdsWithin
theorem PartialHomeomorph.extend_preimage_mem_nhdsWithin :
โ {๐ : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField ๐]
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ๐ E] [inst_3 : TopologicalSpace H]
[inst_4 : TopologicalSpace M] (f : PartialHomeomorph M H) (I : ModelWithCorners ๐ E H) {s t : Set M} {x : M},
x โ f.source โ
t โ nhdsWithin x s โ
โ(f.extend I).symm โปยน' t โ nhdsWithin (โ(f.extend I) x) (โ(f.extend I).symm โปยน' s โฉ Set.range โI)
This theorem states that for a nontrivially normed field `๐`, a normed add commutative group `E`, a normed space `E` over `๐`, topological spaces `M` and `H`, a partial homeomorphism `f` from `M` to `H`, and a model with corners `I` from `๐` to `E` to `H`, if `x` is an element of the source of `f` and `t` is a neighborhood within `x` in `s`, then the preimage of `t` under the inverse of the extension of `f` by `I` is a neighborhood within the image of `x` under the extension of `f` by `I`, within the intersection of the preimage of `s` under the inverse of the extension of `f` by `I` and the range of `I`. In simpler terms, it ensures that the preimage of a neighborhood of a point under an extended chart is a neighborhood of the preimage, within a certain set.
More concisely: Given a nontrivially normed field `๐`, a normed add commutative group `E`, a normed space `E` over `๐`, topological spaces `M` and `H`, a partial homeomorphism `f` from `M` to `H`, and a model with corners `I` from `๐` to `E` to `H`, if `x` is an element of `M`, `t` is a neighborhood of `x` in `M`, and `s` is a neighborhood of `I(x)` in `H`, then the preimage of `s` under the inverse of the extension of `f` by `I` is a neighborhood of `I(t)` in `H`, contained in `s` and within the preimage of `t` under the inverse of the extension of `f` by `I`.
|
ModelWithCorners.closed_range
theorem ModelWithCorners.closed_range :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners ๐ E H),
IsClosed (Set.range โI)
This theorem, named `ModelWithCorners.closed_range`, states that for any non-trivially normed field `๐`, any normed additive commutative group `E` modeled over `๐`, and any topological space `H`, if `I` is a `ModelWithCorners` instance for these mathematical structures, then the range of the function `I` (the set of all possible output values of `I`) is a closed set in the topology of the output space.
More concisely: For any non-trivially normed field `๐`, normed additive commutative group `E` over `๐`, and topological space `H`, if `I` is a `ModelWithCorners` instance for these structures, then the range of `I` is a closed set in the output space `H`.
|
modelWithCornersSelf_partialEquiv
theorem modelWithCornersSelf_partialEquiv :
โ (๐ : Type u_1) [inst : NontriviallyNormedField ๐] (E : Type u_2) [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E], (modelWithCornersSelf ๐ E).toPartialEquiv = PartialEquiv.refl E
The theorem `modelWithCornersSelf_partialEquiv` states that in the context of a nontrivial normed field `๐` and a normed space `E` over `๐`, the partial equivalence associated with the trivial model with corners, which is a model of a vector space with some additional structure, is the identity. In less formal terms, this says that in this specific mathematical structure, going from the vector space to this model and back again (or vice versa) leaves us exactly where we started.
More concisely: In the context of a nontrivial normed field and normed space, the partial equivalence between the trivial model with corners and the original vector space is the identity.
|
PartialHomeomorph.mem_interior_extend_target
theorem PartialHomeomorph.mem_interior_extend_target :
โ {๐ : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField ๐]
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ๐ E] [inst_3 : TopologicalSpace H]
[inst_4 : TopologicalSpace M] (f : PartialHomeomorph M H) (I : ModelWithCorners ๐ E H) {y : H},
y โ f.target โ โI y โ interior (Set.range โI) โ โI y โ interior (f.extend I).target
This theorem states that if `y` is in the target set of a partial homeomorphism `f` from a topological space `M` to another topological space `H`, and the image of `y` under a model-with-corners `I` (a tool from differential geometry that maps the topological space `H` into a normed vector space `E`) lies in the interior of the range of `I`, then this image of `y` under `I` is an interior point of the target set of the composition of `f` and `I`.
This theorem is important in the field of differential geometry, specifically in the study of manifolds, where it is used to establish properties of sets of points that are transformed under homeomorphisms and models-with-corners. It essentially states that under certain conditions, the interior properties of a transformed point are preserved.
More concisely: If `y` is in the domain of a partial homeomorphism `f` and `I(f(y))` is an interior point of `I(H)`, then `I(f(y))` is an interior point of `I(M)` and therefore an interior point of the target set of `f โ I`.
|
mem_analyticGroupoid_of_boundaryless
theorem mem_analyticGroupoid_of_boundaryless :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners ๐ E H)
[inst_4 : CompleteSpace E] [inst_5 : I.Boundaryless] (e : PartialHomeomorph H H),
e โ analyticGroupoid I โ
AnalyticOn ๐ (โI โ โe โ โI.symm) (โI '' e.source) โง AnalyticOn ๐ (โI โ โe.symm โ โI.symm) (โI '' e.target)
The theorem `mem_analyticGroupoid_of_boundaryless` states that for any nontrivially normed field `๐`, any normed addition commutative group `E` that is a `๐`-vector space, any topological space `H`, any `ModelWithCorners` `I` from `๐, E` to `H` where `E` is a complete space and `I` is boundaryless, and any partial homeomorphism `e` from `H` to `H`, then `e` belongs to the analytic groupoid `I` if and only if the function that is the composition of `I`, `e`, and the inverse of `I` is analytic on the image of `e.source` under `I`, and the function that is the composition of `I`, the inverse of `e`, and the inverse of `I` is analytic on the image of `e.target` under `I`. Here, a function is said to be analytic on a set if it is analytic at every point of that set.
More concisely: A partial homeomorphism `e` belongs to the analytic groupoid of a boundaryless `ModelWithCorners` `I` from a complete normed vector space `E` to a topological space `H`, if and only if the functions `I โ e โ I^(-1)` and `I โ e^(-1) โ I^(-1)` are analytic on the images of `e.source` and `e.target` under `I`, respectively.
|
PartialHomeomorph.extend_left_inv'
theorem PartialHomeomorph.extend_left_inv' :
โ {๐ : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField ๐]
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ๐ E] [inst_3 : TopologicalSpace H]
[inst_4 : TopologicalSpace M] (f : PartialHomeomorph M H) (I : ModelWithCorners ๐ E H) {t : Set M},
t โ f.source โ โ(f.extend I).symm โ โ(f.extend I) '' t = t
This theorem, `PartialHomeomorph.extend_left_inv'`, states that for any nontrivially normed field `๐`, normed add commutative group `E`, normed space over `๐` and `E`, topological spaces `H` and `M`, a given partial homeomorphism `f` from `M` to `H`, a model with corners `I` from `๐` to `E` and `H`, and a subset `t` of `M` that is contained in the source of `f`, the image of `t` under the composition of the inverses of `f.extend I` is exactly `t`. In other words, the operation of extending `f` with `I`, taking the inverse, and then applying it again, acts as the identity on `t`.
More concisely: For any nontrivially normed field `๐`, normed add commutative group `E`, topological spaces `H` and `M`, a partial homeomorphism `f` from `M` to `H`, and a subset `t` of `M` contained in the domain of `f`, the extension of `f` with a model `I` from `๐` to `E` and `H` and the inverse of this extension map `f.extend I` have the same effect on `t`, i.e., `(f.extend I)โปยนโกโf.extend I(t) = t`.
|
ModelWithCorners.symm_comp_self
theorem ModelWithCorners.symm_comp_self :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners ๐ E H),
โI.symm โ โI = id
The theorem `ModelWithCorners.symm_comp_self` states that for any given `ModelWithCorners` structure `I` for a nontrivially normed field `๐`, a normed additive commutative group `E` and a topological space `H`, the composition of the partial equivalence corresponding to `I` and its inverse (obtained through `ModelWithCorners.symm`) is the identity function. In other words, applying the inverse and then reapplying the original function is equivalent to doing nothing, thus demonstrating that the original function and its inverse are perfect inverses of each other in the context of the `ModelWithCorners` structure.
More concisely: For any `ModelWithCorners` structure `I` over a nontrivially normed field `๐`, the composition of `I` and its symmetric inverse is the identity function.
|
ModelWithCorners.leftInverse
theorem ModelWithCorners.leftInverse :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners ๐ E H),
Function.LeftInverse โI.symm โI
The theorem `ModelWithCorners.leftInverse` states that for any model with corners `I` of types `๐` (a non-trivially normed field), `E` (a normed add commutative group with a normed space over `๐`), and `H` (a topological space), the inverse of `I` is a left inverse function to `I`. In other words, when you apply `I` and then apply the inverse of `I`, you will end up with the original input, for all inputs. This is written mathematically as `g โ f = id`, where `f` represents the function `I` and `g` represents the inverse of `I`.
More concisely: The map `I` and its inverse commute with each other, i.e., `I โ I^โ1 = I^โ1 โ I = id`.
|
ModelWithCorners.range_eq_univ
theorem ModelWithCorners.range_eq_univ :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners ๐ E H)
[inst_4 : I.Boundaryless], Set.range โI = Set.univ
The theorem `ModelWithCorners.range_eq_univ` states that for any non-trivial normed field `๐`, normed additive commutative group `E`, and topological space `H`, if `I` is a model with corners (a mathematical object used to represent a coordinate system in differential geometry) on `๐`, `E`, and `H` such that `I` does not have a boundary (represented by `ModelWithCorners.Boundaryless I`), then the range of `I` (i.e., the set of all possible values that `I` can take) is the entire set `Set.univ` (i.e., the set of all elements in the type). In other words, every possible value in the type of `I` can be achieved by `I` under these conditions.
More concisely: If `I` is a boundaryless model with corners on a non-trivial normed field, normed additive commutative group, and topological space, then the range of `I` equals the universe set.
|
PartialHomeomorph.continuousAt_extend_symm'
theorem PartialHomeomorph.continuousAt_extend_symm' :
โ {๐ : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField ๐]
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ๐ E] [inst_3 : TopologicalSpace H]
[inst_4 : TopologicalSpace M] (f : PartialHomeomorph M H) (I : ModelWithCorners ๐ E H) {x : E},
x โ (f.extend I).target โ ContinuousAt (โ(f.extend I).symm) x
The theorem `PartialHomeomorph.continuousAt_extend_symm'` states that for any nontrivially normed field `๐`, a normed add commutative group `E`, a normed space `E` over `๐`, and topological spaces `H` and `M`, given a partial homeomorphism `f` from `M` to `H` and a model with corners `I` from `๐` to `H` and `E`, if `x` is an element of the target of the extension of the partial homeomorphism `f`, then the function corresponding to the inverse of the extension of the partial homeomorphism `f` is continuous at the point `x`.
More concisely: For a nontrivially normed field `๐`, a normed add commutative group `E` over `๐`, and topological spaces `H` and `M`, if `f` is a partial homeomorphism from `M` to `H`, `I` is a model with corners from `๐` to `H` and `E`, and `x` is in the image of the extension of `f`, then the inverse of the extended function is continuous at `x`.
|
ModelWithCorners.rightInvOn
theorem ModelWithCorners.rightInvOn :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners ๐ E H),
Set.RightInvOn (โI.symm) (โI) (Set.range โI)
This theorem states that for any ModelWithCorners `I` in a nontrivially normed field `๐`, with `E` being a normed additive commutative group over `๐` and `H` being a topological space, the inverse of `I` (obtained through the function `ModelWithCorners.symm`) is a right inverse to `I` on its range. In other words, for any point `x` in the range of `I`, we have `I (ModelWithCorners.symm I x) = x`.
More concisely: For any `ModelWithCorners I` in a nontrivially normed field `๐`, the function `ModelWithCorners.symm I` is a right inverse to `I` on the range of `I`, i.e., `I (ModelWithCorners.symm I x) = x` for all `x` in the range of `I`.
|
SmoothManifoldWithCorners.chart_mem_maximalAtlas
theorem SmoothManifoldWithCorners.chart_mem_maximalAtlas :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners ๐ E H)
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : SmoothManifoldWithCorners I M]
(x : M), chartAt H x โ SmoothManifoldWithCorners.maximalAtlas I M
The theorem `SmoothManifoldWithCorners.chart_mem_maximalAtlas` states that for any non-trivially normed field `๐`, a normed additive commutative group `E`, a normed space `๐ E`, a topological space `H`, a model with corners `I` of `๐ E H`, another topological space `M`, a charted space `H M`, and a smooth manifold with corners `I M`, the preferred chart at any point `x` in the manifold `M` is an element of the maximal atlas of this smooth manifold with corners. The maximal atlas is a collection of charts that are smoothly compatible with each other, meaning they can be transformed into each other through a smooth function.
More concisely: Given a smooth manifold with corners over a non-trivially normed field, any point in the manifold belongs to the preferred chart of some chart in the maximal atlas.
|
symm_trans_mem_contDiffGroupoid
theorem symm_trans_mem_contDiffGroupoid :
โ (n : โโ) {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners ๐ E H)
{M : Type u_4} [inst_4 : TopologicalSpace M] (e : PartialHomeomorph M H), e.symm.trans e โ contDiffGroupoid n I
This theorem states that for any `n` in the set of natural numbers union infinity, and given a non-trivially normed field `๐`, a normed additive commutative group `E` that is a normed space over `๐`, a topological space `H`, a model with corners `I` on `๐`, `E`, and `H`, a topological space `M`, and a partial homeomorphism `e` from `M` to `H`, the composition of the inverse of `e` and `e` itself belongs to the `C^n` groupoid defined by `n` and `I`. This is a statement about the differentiability of the composition of a function and its inverse in the context of differential geometry.
More concisely: Given a normed field `๐`, a normed additive commutative group `E` over `๐`, a topological space `M`, a partial homeomorphism `e: M -> H` from `M` to a topological space `H` with a model of corners `I`, and `E` being a normed space over `H` via `e`, the composition of `e` and its inverse belongs to the `C^n` groupoid on `H` with respect to `I`.
|
ModelWithCorners.continuous_symm
theorem ModelWithCorners.continuous_symm :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners ๐ E H),
Continuous โI.symm
This theorem states that for any ModelWithCorners `I` over a nontrivial normed field `๐`, a normed additive commutative group `E`, and a topological space `H`, the inverse of `I`, denoted `ModelWithCorners.symm I`, is a continuous function. Here, continuity is understood in the topological sense, meaning that the preimage of any open set under `ModelWithCorners.symm I` is also an open set.
More concisely: For any ModelWithCorners `I` over a nontrivial normed field `๐`, the symmetry `ModelWithCorners.symm I` of the normed additive commutative group `E` with respect to `I` is a continuous function in the topological sense.
|
contDiffGroupoid_prod
theorem contDiffGroupoid_prod :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_3} [inst_3 : TopologicalSpace H] {E' : Type u_5} {H' : Type u_6}
[inst_4 : NormedAddCommGroup E'] [inst_5 : NormedSpace ๐ E'] [inst_6 : TopologicalSpace H']
{I : ModelWithCorners ๐ E H} {I' : ModelWithCorners ๐ E' H'} {e : PartialHomeomorph H H}
{e' : PartialHomeomorph H' H'},
e โ contDiffGroupoid โค I โ e' โ contDiffGroupoid โค I' โ e.prod e' โ contDiffGroupoid โค (I.prod I')
This theorem states that for any non-trivially normed field `๐` and normed additive commutative groups `E` and `E'` equipped with their respective normed spaces over `๐`, if `H` and `H'` are topological spaces and `I` and `I'` are the respective models with corners for `H` and `H'`, then for any two partial homeomorphisms `e` from `H` to `H` and `e'` from `H'` to `H'` that are part of the infinitely differentiable (smooth) groupoid, their product is also part of the same smooth groupoid when the models with corners are taken as their product.
More concisely: For any non-trivially normed field `๐`, normed additive commutative groups `E` and `E'`, and their respective models with corners `I` and `I'`, if `e` is an infinitely differentiable partial homeomorphism from `I` to `I` and `e'` is an infinitely differentiable partial homeomorphism from `I'` to `I'`, then their product is an infinitely differentiable partial homeomorphism from `I โค I'` to `I โค I'`, where `I โค I'` denotes the product of `I` and `I'` as models with corners.
|
ModelWithCorners.unique_diff
theorem ModelWithCorners.unique_diff :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners ๐ E H),
UniqueDiffOn ๐ (Set.range โI)
This theorem states that for any Nontrivially Normed Field `๐`, Normed Additive Commutative Group `E`, Normed Space `E` over `๐`, and Topological Space `H`, given a Model With Corners `I` of types `๐`, `E`, and `H`, the set of points (in `๐`) where the function `I` (cast to a function `๐ โ E`) is differentiable is exactly the range of `I`. In other words, the function `I` is uniquely differentiable on its entire range.
Here, the `ModelWithCorners` refers to a mathematical construct used in the formalization of smooth manifolds, providing a link between the manifold and a model Euclidean space. `UniqueDiffOn` is a property that a subset of a Normed Space has if every function which is differentiable on that subset has derivative which is unique.
More concisely: For any nontrivially normed field `๐`, normed additive commutative group `E`, normed space `E` over `๐`, and topological space `H`, the function `I` from `๐` to `E` defined in a Model With Corners `I` of types `๐`, `E`, and `H` is uniquely differentiable on its entire range.
|
extChartAt_preimage_mem_nhdsWithin'
theorem extChartAt_preimage_mem_nhdsWithin' :
โ {๐ : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField ๐]
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ๐ E] [inst_3 : TopologicalSpace H]
[inst_4 : TopologicalSpace M] (I : ModelWithCorners ๐ E H) {s t : Set M} [inst_5 : ChartedSpace H M] {x x' : M},
x' โ (extChartAt I x).source โ
t โ nhdsWithin x' s โ
โ(extChartAt I x).symm โปยน' t โ
nhdsWithin (โ(extChartAt I x) x') (โ(extChartAt I x).symm โปยน' s โฉ Set.range โI)
This theorem, "extChartAt_preimage_mem_nhdsWithin'", states that for a given nontrivially normed field `๐`, Normed Additive Commutative Group `E`, Normed Space `E` over `๐`, and Topological Spaces `M` and `H`, along with a model with corners `I` of type `๐`, `E` and `H`, two sets `s` and `t` of type `M`, a charted space `M` over `H` and two points `x` and `x'` of type `M`. If the point `x'` belongs to the source of the extended chart at `x` with model `I` and if the set `t` is in the "neighborhood within" `s` at `x'`, then the preimage of `t` under the inverse of the extended chart at `x` with model `I` is in the "neighborhood within" the image of `x'` under the extended chart at `x` with model `I` of the intersection of the preimage of `s` under the inverse of the extended chart at `x` with model `I` and the range of the model `I`. In simpler words, it says that the preimage of a neighborhood of a point under an extended chart is a neighborhood of the preimage within a set.
More concisely: Given a nontrivially normed field `๐`, Normed Additive Commutative Group `E`, Normed Space `E` over `๐`, Topological Spaces `M` and `H`, model with corners `I` for `๐`, `E`, and `H`, charted space `M` over `H`, and points `x` and `x'` in `M`, if `x'` is in the extended chart at `x` with model `I` and `t` is in the "neighborhood within" `s` at `x'`, then the inverse image of `t` under the extended chart at `x` with model `I` is in the "neighborhood within" the intersection of the inverse image of `s` and the range of the model `I` at `x`.
|
PartialHomeomorph.extend_source_mem_nhds
theorem PartialHomeomorph.extend_source_mem_nhds :
โ {๐ : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField ๐]
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ๐ E] [inst_3 : TopologicalSpace H]
[inst_4 : TopologicalSpace M] (f : PartialHomeomorph M H) (I : ModelWithCorners ๐ E H) {x : M},
x โ f.source โ (f.extend I).source โ nhds x
The theorem `PartialHomeomorph.extend_source_mem_nhds` states that for any type `๐` which is a nontrivially normed field, any type `E` which is a normed add commutative group, any type `M`, any type `H` which are both topological spaces, a partial homeomorphism `f` from `M` to `H`, a ModelWithCorners `I` with base type `๐`, shape type `E` and model type `H`, and an element `x` of type `M` that is in the source of `f`, the source of the extension of `f` using `I` is a neighborhood of `x`. In other words, the source set of the extended partial homeomorphism contains an open set around `x`.
More concisely: For any nontrivially normed field ๐, normed add commutative group E, topological spaces M and H, a partial homeomorphism f from M to H, and an element x in the domain of f, the source of the extension of f using some ModelWithCorners I containing x is a neighborhood of x.
|
extChartAt_preimage_mem_nhdsWithin
theorem extChartAt_preimage_mem_nhdsWithin :
โ {๐ : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField ๐]
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ๐ E] [inst_3 : TopologicalSpace H]
[inst_4 : TopologicalSpace M] (I : ModelWithCorners ๐ E H) {s t : Set M} [inst_5 : ChartedSpace H M] {x : M},
t โ nhdsWithin x s โ
โ(extChartAt I x).symm โปยน' t โ nhdsWithin (โ(extChartAt I x) x) (โ(extChartAt I x).symm โปยน' s โฉ Set.range โI)
This theorem, named `extChartAt_preimage_mem_nhdsWithin`, is a technical lemma in the field of topology. It asserts that for a given non-trivially normed field `๐`, normed additive commutative group `E`, normed space over `๐` and `E`, topological spaces `H` and `M`, a model with corners `I` on `๐`, `E` and `H`, a charted space structure on `H` and `M`, and sets `s` and `t` in `M`, if `t` is in the neighborhood within `s` of a point `x` in `M`, then the preimage of `t` under the inverse of the extended chart at `x` with respect to `I` is in the neighborhood within the intersection of the preimage of `s` under the same chart and the range of `I`, of the image of `x` under the chart. The concept is related to the continuity of maps in topological spaces and the manipulation of preimages of sets under continuous maps.
More concisely: For a non-trivially normed field `๐`, normed additive commutative groups `E` over `๐`, topological spaces `H` and `M`, model with corners `I`, charted space structures on `H` and `M`, and sets `s` and `t` in `M`, if `t` is in the neighborhood within `s` of a point `x` in `M`, then the preimage of `t` under the inverse of the extended chart at `x` with respect to `I` is in the neighborhood within the intersection of the preimage of `s` and the range of `I`, of the image of `x` under the chart.
|
PartialHomeomorph.contDiffOn_extend_coord_change
theorem PartialHomeomorph.contDiffOn_extend_coord_change :
โ {๐ : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField ๐]
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ๐ E] [inst_3 : TopologicalSpace H]
[inst_4 : TopologicalSpace M] {f f' : PartialHomeomorph M H} (I : ModelWithCorners ๐ E H)
[inst_5 : ChartedSpace H M],
f โ SmoothManifoldWithCorners.maximalAtlas I M โ
f' โ SmoothManifoldWithCorners.maximalAtlas I M โ
ContDiffOn ๐ โค (โ(f.extend I) โ โ(f'.extend I).symm) ((f'.extend I).symm.trans (f.extend I)).source
This theorem, `PartialHomeomorph.contDiffOn_extend_coord_change`, states that for any types ๐, E, M, H, where ๐ is a nontrivially normed field, E is a normed add-commutative group, E is also a normed space over ๐, H and M are topological spaces, and any pair of partial homeomorphisms `f` and `f'` from M to H that are in the maximal atlas of the smooth manifold with corners defined by the model with corners `I`, the composition of the extensions of these homeomorphisms is a continuously differentiable function (of any order) on the source of the transitive closure of the inverses of these extensions. In other words, the composition of the extensions of the partial homeomorphisms behaves smoothly when restricted to the appropriate domain.
More concisely: Given nontrivially normed field ๐, normed add-commutative groups E with the structure of a normed space over ๐, topological spaces H and M, and partial homeomorphisms `f` and `f'` from M to H in the maximal atlas of the smooth manifold with corners defined by `I`, the extension of their composition is continuously differentiable on the source of the transitive closure of the inverses of these extensions.
|
PartialHomeomorph.continuousOn_writtenInExtend_iff
theorem PartialHomeomorph.continuousOn_writtenInExtend_iff :
โ {๐ : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} {E' : Type u_5} {M' : Type u_6} {H' : Type u_7}
[inst : NontriviallyNormedField ๐] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ๐ E]
[inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M] (f : PartialHomeomorph M H)
(I : ModelWithCorners ๐ E H) [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace ๐ E']
[inst_7 : TopologicalSpace H'] [inst_8 : TopologicalSpace M'] (I' : ModelWithCorners ๐ E' H') {s : Set M}
{f' : PartialHomeomorph M' H'} {g : M โ M'},
s โ f.source โ
Set.MapsTo g s f'.source โ
(ContinuousOn (โ(f'.extend I') โ g โ โ(f.extend I).symm) (โ(f.extend I) '' s) โ ContinuousOn g s)
This theorem states that for a given set of mathematical structures and functions, specifically topological spaces, normed fields and spaces, and a model with corners, if the set `s` is a subset of the source of function `f` and for each element `x` in `s`, `g(x)` is in the source of `f'`, then function `g` is continuous on `s` if and only if `g` written in charts `f.extend I` and `f'.extend I'` is continuous on the image of `s` under `f.extend I`.
In other words, it establishes a condition under which the continuity of a function `g` on a set `s` can be concluded from the continuity of the composition of `f'.extend I'`, `g`, and the inverse of `f.extend I` on the image of `s` under `f.extend I`. This theorem is useful in the study of topology and differentiable manifolds, where "charts" are used to map points in a manifold to points in a simpler space, often Euclidean space.
More concisely: Given topological spaces X, Y, Z, normed fields F and G, functions f : X โ Y, f' : Y โ Z, g : X โ G, and a subset s of X such that for all x in s, g(x) is in the domain of f' and f(x) is defined, if g is continuous on s if and only if the composition g โ (f.extend I) is continuous on the image of s under f.extend I.
|
ModelWithCorners.target_eq
theorem ModelWithCorners.target_eq :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners ๐ E H),
I.target = Set.range โI
This theorem states that for any nontrivial normed field `๐`, any normed additive commutative group `E` that is also a normed space over `๐`, any topological space `H`, and any `ModelWithCorners` I with respect to these structures, the target of `I` is equivalent to the set range of `I`. In simpler terms, the theorem says that the set of all possible outputs of the ModelWithCorners `I` is precisely the set of all values it can map to.
More concisely: For any nontrivial normed field `๐`, normed additive commutative group `E` over `๐`, topological space `H`, and `ModelWithCorners` `I` with respect to these structures, the range of `I` is equal to its target.
|
ModelWithCorners.closedEmbedding
theorem ModelWithCorners.closedEmbedding :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners ๐ E H),
ClosedEmbedding โI
This theorem asserts that for any nontrivially normed field `๐`, a normed add commutative group `E` which is also a normed space over `๐`, and any topological space `H`, the model with corners `I` (a mathematical structure used in differential geometry to define manifolds with boundary) is a closed embedding. In other words, the map `I` from the manifold to the Euclidean space `E` is a homeomorphism onto its image, injective, and the image of its closure in the manifold is the closure of the image in `E`, which are the requirements for a closed embedding in topology.
More concisely: Given a nontrivially normed field `๐`, a normed add commutative group `E` over `๐` that is also a topological vector space, and an manifold with boundary `I` as a subspace of `E`, `I` is a closed embedding into `E`.
|
ModelWithCorners.map_nhds_eq
theorem ModelWithCorners.map_nhds_eq :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners ๐ E H) (x : H),
Filter.map (โI) (nhds x) = nhdsWithin (โI x) (Set.range โI)
This theorem, `ModelWithCorners.map_nhds_eq`, states that for any non-trivially normed field `๐`, a normed add commutative group `E` that is also a normed space over `๐`, a topological space `H` and a model `I` with corners relating the field `๐`, the group `E` and the space `H`, the filter generated by mapping the model `I` to the neighborhood filter of any point `x` in `H` is equal to the "neighborhood within" filter at the point `I x` in the range of the model `I`. In other words, it asserts a relationship between the forward map of a filter and the neighborhood filter within a set, in the context of a mathematical model with corners.
More concisely: For any non-trivially normed field `๐`, normed add commutative group `E` over `๐`, topological space `H`, and model `I` with corners relating `๐`, `E`, and `H`, the filter generated by mapping `I` to the neighborhood filter of any point `x` in `H` equals the "neighborhood within" filter at `I x` in the range of `I`.
|
PartialHomeomorph.map_extend_nhds
theorem PartialHomeomorph.map_extend_nhds :
โ {๐ : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField ๐]
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ๐ E] [inst_3 : TopologicalSpace H]
[inst_4 : TopologicalSpace M] (f : PartialHomeomorph M H) (I : ModelWithCorners ๐ E H) {x : M},
x โ f.source โ Filter.map (โ(f.extend I)) (nhds x) = nhdsWithin (โ(f.extend I) x) (Set.range โI)
This theorem states that for any non-trivially normed field `๐`, normed add commutative group `E`, normed space over `๐` and `E`, and topological spaces `H` and `M`, given a partial homeomorphism `f` between `M` and `H`, and a model with corners `I` (which is a structure used in the definition of manifolds), for any point `x` in the source of `f`, the forward map of the neighborhood filter at `x` under the extension of `f` by `I` is equal to the neighborhood within the range of `I` at the image of `x` under the extension of `f` by `I`. In simpler terms, this theorem is about how the neighborhood of a point is transformed under a partial homeomorphism when it is extended using a model with corners.
More concisely: For any partial homeomorphism `f` between topological spaces `M` and `H`, and given a non-trivially normed field `๐`, normed add commutative group `E` over `๐` and `E`, and a model with corners `I`, the forward neighborhood filters of `x` in `M` and `f(x)` in `H`, under the extension of `f` by `I`, are equal.
|
extChartAt_source
theorem extChartAt_source :
โ {๐ : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField ๐]
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ๐ E] [inst_3 : TopologicalSpace H]
[inst_4 : TopologicalSpace M] (I : ModelWithCorners ๐ E H) [inst_5 : ChartedSpace H M] (x : M),
(extChartAt I x).source = (chartAt H x).source
The theorem `extChartAt_source` states that for any nontrivially normed field '๐', normed additive commutative group 'E', topological spaces 'H' and 'M', model with corners 'I', and charted space with model 'H' on 'M', and any point 'x' in 'M', the source set of the extended chart at 'x' is equal to the source set of the preferred chart at 'x'. Here, a chart gives a local homeomorphism between the manifold 'M' and the model space 'H', and an extended chart is a chart that has been extended to the boundary of the model space.
More concisely: For any nontrivially normed field '๐', normed additive commutative group 'E', topological spaces 'H' and 'M', model with corners 'I', charted space with model 'H' on 'M', and point 'x' in 'M' with chart and extended chart, the source sets of the chart and extended chart at 'x' are equal.
|
ModelWithCorners.continuousAt
theorem ModelWithCorners.continuousAt :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners ๐ E H) {x : H},
ContinuousAt (โI) x
The theorem `ModelWithCorners.continuousAt` states that for any non-trivially normed field `๐`, any normed addition commutative group `E` that is also a normed space over `๐`, and any topological space `H`, if `I` is a model with corners based on these types, then the function associated with `I` (obtained by casting `I` to a function) is continuous at any point `x` in `H`. In other words, for any given point `x` in `H`, the function's output values tend towards the function's value at `x` as the input values tend towards `x`.
More concisely: For any non-trivially normed field ๐, normed addition commutative group E over ๐ as a normed space, and topological space H, the function derived from a model with corners I over (๐, E, H) is continuous at any point x in H.
|
PartialHomeomorph.continuousOn_extend
theorem PartialHomeomorph.continuousOn_extend :
โ {๐ : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField ๐]
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ๐ E] [inst_3 : TopologicalSpace H]
[inst_4 : TopologicalSpace M] (f : PartialHomeomorph M H) (I : ModelWithCorners ๐ E H),
ContinuousOn (โ(f.extend I)) (f.extend I).source
The theorem `PartialHomeomorph.continuousOn_extend` states that for any nontrivially normed field `๐`, normed additive commutative group `E`, normed space `E` over `๐`, and topological spaces `M` and `H`, if `f` is a partial homeomorphism from `M` to `H` and `I` is a model with corners on `๐`, `E` and `H`, then the extension of `f` via `I` is continuous on its source set. The extension of `f` via `I` is represented by `PartialHomeomorph.extend f I`, and its source set is given by `(PartialHomeomorph.extend f I).source`. A model with corners is a generalization of the concept of a manifold with boundary in differential geometry.
More concisely: Given a nontrivially normed field `๐`, normed additive commutative groups `E` and `H`, normed space `E` over `๐`, topological spaces `M` and `H`, and a partial homeomorphism `f` from `M` to `H`, the extension of `f` via a model `I` is continuous on its source set.
|