continuousMul_of_smooth
theorem continuousMul_of_smooth :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
[inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {G : Type u_4}
[inst_4 : Mul G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [inst : SmoothMul I G],
ContinuousMul G
This theorem states that if multiplication on a type `G` is smooth, then it is also continuous. Here, `𝕜` signifies a nontrivial normed field, `H` a topological space, and `E` a normed additive commutative group that forms a normed space over `𝕜`. `I` indicates a model with corners over `𝕜`, `E`, and `H`. `G` is a type with multiplication operation and a topological structure, which is also a charted space over `H`. The theorem does not serve as an instance due to certain technical details related to design choices about smooth algebraic structures.
More concisely: If `G` is a smooth multiplication on a charted space over a topological space `H` with values in a normed additive commutative group `E` over a nontrivial normed field `𝕜`, then `G` is continuous.
|
continuousAdd_of_smooth
theorem continuousAdd_of_smooth :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
[inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {G : Type u_4}
[inst_4 : Add G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [inst : SmoothAdd I G],
ContinuousAdd G
This theorem states that if addition operation is smooth over a certain space, then it is also continuous over that space. Here, the smoothness and continuity of addition are defined within the context of differential geometry, where we consider fields, topological spaces, and normed spaces. The theorem applies to a non-trivially normed field `𝕜`, a topological space `H`, a normed add commutative group `E` which is also a normed space over `𝕜`, and another topological space `G` equipped with an addition operation and a charted space structure over `H`. The smoothness of addition on `G` is described in the context of a model with corners `I` from `𝕜` and `E` to `H`. For such a setup, if the addition on `G` is smooth with respect to `I`, then it is also continuous.
More concisely: If addition on a charted space `G` over a topological space `H`, equipped with a normed add commutative group `E` and a model with corners from a non-trivially normed field `𝕜`, is smooth, then it is also continuous.
|
Smooth.mul
theorem Smooth.mul :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
[inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
[inst_4 : Mul G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [inst_7 : SmoothMul I G]
{E' : Type u_5} [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_6}
[inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_11 : TopologicalSpace M]
[inst_12 : ChartedSpace H' M] {f g : M → G}, Smooth I' I f → Smooth I' I g → Smooth I' I (f * g)
The theorem `Smooth.mul` expresses that, given a nontrivially normed field `𝕜`, two topological spaces `H` and `H'`, a normed additive commutative group `E` and `E'` over `𝕜`, a model with corners `I` and `I'` over `𝕜` and `H` and `H'` respectively, multiply `G` with a smooth structure, and a topological space `M` with a smooth structure, if two functions `f` and `g` from `M` to `G` are smooth (differentiable to any degree), then their product `f * g` is also smooth.
More concisely: Given a nontrivially normed field `𝕜`, if `f` and `g` are smooth functions from a topological space `M` to a smooth manifold `G` over `𝕜`, then their product `f * g` is also a smooth function from `M` to `G`.
|