Smooth.comp
theorem Smooth.comp :
โ {๐ : 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] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace ๐ E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{E'' : Type u_8} [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace ๐ E''] {H'' : Type u_9}
[inst_13 : TopologicalSpace H''] {I'' : ModelWithCorners ๐ E'' H''} {M'' : Type u_10}
[inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M''] {f : M โ M'} {g : M' โ M''},
Smooth I' I'' g โ Smooth I I' f โ Smooth I I'' (g โ f)
This theorem states that the composition of infinitely differentiable (denoted as `C^โ`) functions is also infinitely differentiable. More specifically, given two functions `f` and `g` where `f` maps from a manifold `M` to a manifold `M'` and `g` maps from `M'` to a third manifold `M''` under specific conditions (including the spaces being topological and normed), if `g` is infinitely differentiable between `M'` and `M''` and `f` is infinitely differentiable between `M` and `M'`, then the composition of `g` and `f` (denoted as `g โ f`) is also infinitely differentiable between `M` and `M''`.
More concisely: If `f` is a `C^โ` function from manifold `M` to `M'` and `g` is a `C^โ` function from `M'` to `M''`, then their composition `g โ f` is a `C^โ` function from `M` to `M''`.
|
SmoothAt.comp
theorem SmoothAt.comp :
โ {๐ : 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] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace ๐ E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{E'' : Type u_8} [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace ๐ E''] {H'' : Type u_9}
[inst_13 : TopologicalSpace H''] {I'' : ModelWithCorners ๐ E'' H''} {M'' : Type u_10}
[inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M''] {f : M โ M'} {g : M' โ M''} (x : M),
SmoothAt I' I'' g (f x) โ SmoothAt I I' f x โ SmoothAt I I'' (g โ f) x
This theorem states that if you have two functions `f` and `g` in a smooth (continuously differentiable) context, and `g` is smooth at the point `f(x)`, and `f` is smooth at the point `x`, then their composition `g โ f` is also smooth at the point `x`. More formally, the smoothness is defined in the context of a non-trivial normed field `๐`, normed additive commutative groups `E`, `E'` and `E''`, topological spaces `H`, `H'` and `H''`, models with corners `I`, `I'` and `I''`, and charted spaces `M`, `M'` and `M''`.
More concisely: If `f` and `g` are smooth functions in a smooth context, and `g` is smooth at `f(x)` and `f` is smooth at `x`, then their composition `g โ f` is smooth at `x`.
|
contMDiff_of_support
theorem contMDiff_of_support :
โ {๐ : 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] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace ๐ E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{n : โโ} [inst_11 : Zero M'] {f : M โ M'}, (โ x โ tsupport f, ContMDiffAt I I' n f x) โ ContMDiff I I' n f
The theorem `contMDiff_of_support` states that for a function `f` mapping from a topological space `M` to another topological space `M'`, if `f` is continuously differentiable at all points `x` in the topological support of `f` (i.e., the closure of the set of all elements where the function is nonzero), then `f` is continuously differentiable everywhere. This applies under certain conditions: `M` and `M'` are both topological spaces modeled on topological vector spaces `E` and `E'` respectively, with `E` and `E'` being normed additive commutative groups. The field `๐` of scalars is a normed field.
More concisely: If a function `f` from a topological space `M` to another topological space `M'`, modeled on normed additive commutative groups `E` and `E'` respectively over a normed field `๐`, is continuously differentiable at all points in the closure of `f`'s support, then `f` is continuously differentiable everywhere.
|
smooth_const
theorem smooth_const :
โ {๐ : 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] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace ๐ E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{c : M'}, Smooth I I' fun x => c
The theorem `smooth_const` states that for any non-trivial normed field `๐`, normed additive commutative group structures `E` and `E'`, normed spaces over `๐` for `E` and `E'`, topological spaces `H`, `M`, `H'`, and `M'`, a manifold `M` with corners `I` modeled on `(E, H)`, a manifold `M'` with corners `I'` modeled on `(E', H')`, and a constant value `c` in `M'`, the function that maps every point in `M` to the constant `c` is a smooth function from `M` to `M'`. In other words, the theorem says that constant functions are smooth.
More concisely: Given normed fields `๐`, normed spaces `E` and `E'`, and manifolds `M` modeled on `(E, H)` and `M'` modeled on `(E', H')`, the constant function from `M` to `M'` is smooth.
|
ContMDiffAt.comp_of_eq
theorem ContMDiffAt.comp_of_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}
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace ๐ E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{E'' : Type u_8} [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace ๐ E''] {H'' : Type u_9}
[inst_13 : TopologicalSpace H''] {I'' : ModelWithCorners ๐ E'' H''} {M'' : Type u_10}
[inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M''] {f : M โ M'} {n : โโ} {g : M' โ M''} {x : M}
{y : M'}, ContMDiffAt I' I'' n g y โ ContMDiffAt I I' n f x โ f x = y โ ContMDiffAt I I'' n (g โ f) x
The theorem `ContMDiffAt.comp_of_eq` states that for any non-trivial normed field `๐`, normed additive commutative groups `E`, `E'`, `E''`, topological spaces `H`, `H'`, `H''`, `M`, `M'`, `M''`, model with corners `I`, `I'`, `I''`, and charted spaces on `M`, `M'`, `M''` respectively, if a function `g : M' โ M''` is continuously differentiable at a point `y` from `M'` and a function `f : M โ M'` is continuously differentiable at a point `x` from `M` such that `f(x) = y`, then the composition of `g` and `f` (i.e., `g โ f`) is also continuously differentiable at the point `x` from `M`.
More concisely: If `f : M โ M'` and `g : M' โ M''` are continuously differentiable functions with `f(x) = y` and `x โ M`, then the composition `g โ f : M โ M''` is continuously differentiable at `x`.
|
SmoothOn.comp
theorem SmoothOn.comp :
โ {๐ : 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] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace ๐ E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{E'' : Type u_8} [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace ๐ E''] {H'' : Type u_9}
[inst_13 : TopologicalSpace H''] {I'' : ModelWithCorners ๐ E'' H''} {M'' : Type u_10}
[inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M''] {f : M โ M'} {s : Set M} {t : Set M'}
{g : M' โ M''}, SmoothOn I' I'' g t โ SmoothOn I I' f s โ s โ f โปยน' t โ SmoothOn I I'' (g โ f) s
This theorem states that the composition of infinitely differentiable (C^โ) functions over certain domains is also infinitely differentiable. Given a nontrivially normed field and multiple topological spaces with corresponding normed additive commutative groups and normed spaces, as well as functions `f` from `M` to `M'` and `g` from `M'` to `M''` that are smooth on sets `s` and `t` respectively, if the set `s` is a subset of the preimage of `t` under `f`, then the composition function `(g โ f)` is smooth on `s`.
More concisely: If `f: M -> M'` and `g: M' -> M''` are infinitely differentiable functions with domains `s` and `t` respectively, such that `s` is a subset of `f^(โ1)(t)`, then the composition `g โ f` is an infinitely differentiable function on `s`.
|
ContMDiff.of_comp_openEmbedding
theorem ContMDiff.of_comp_openEmbedding :
โ {๐ : 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] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace ๐ E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : Nonempty M']
{e' : M' โ H'} (h' : OpenEmbedding e') {n : WithTop โ} {f : M โ M'},
ContMDiff I I' n (e' โ f) โ ContMDiff I I' n f
The theorem `ContMDiff.of_comp_openEmbedding` states that for a given manifolds `M` and `M'` modelled on topological spaces `H` and `H'` respectively with their geometric structure given by `ModelWithCorners` `I` and `I'`, and for a map `f` from `M` to `M'`, if the composition of `f` with an open embedding `e'` from `M'` to `H'` is a continuous differentiable (smooth), then `f` itself is also smooth. This is particularly useful in situations where the composition of `f` with `e'` is equivalent to the composition of a smooth map `e` from `M` to another space `X` and a smooth map `g` from `X` to `H'`.
More concisely: If the composition of a smooth map from one manifold to another and an open embedding is smooth, then the original map is smooth.
|
SmoothWithinAt.comp
theorem SmoothWithinAt.comp :
โ {๐ : 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] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace ๐ E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{E'' : Type u_8} [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace ๐ E''] {H'' : Type u_9}
[inst_13 : TopologicalSpace H''] {I'' : ModelWithCorners ๐ E'' H''} {M'' : Type u_10}
[inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M''] {f : M โ M'} {s : Set M} {t : Set M'}
{g : M' โ M''} (x : M),
SmoothWithinAt I' I'' g t (f x) โ
SmoothWithinAt I I' f s x โ Set.MapsTo f s t โ SmoothWithinAt I I'' (g โ f) s x
This theorem states that, given a set of mathematical structures (including fields, vector spaces, topological spaces, manifolds, and differentiable maps), if function `g` is infinitely differentiable at the point `f(x)` within the set `t`, and function `f` is infinitely differentiable at the point `x` within the set `s`, and if `f` maps `s` into `t`, then the composition of `g` and `f` is also infinitely differentiable at point `x` within the set `s`. In essence, it says that the composition of infinitely differentiable functions remains infinitely differentiable.
More concisely: If `f` is an infinitely differentiable map from set `s` to set `t`, and `g` is an infinitely differentiable function at `f(x)` in `t`, then their composition `g โ f` is an infinitely differentiable function at `x` in `s`.
|
ContMDiffOn.comp'
theorem ContMDiffOn.comp' :
โ {๐ : 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] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace ๐ E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{E'' : Type u_8} [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace ๐ E''] {H'' : Type u_9}
[inst_13 : TopologicalSpace H''] {I'' : ModelWithCorners ๐ E'' H''} {M'' : Type u_10}
[inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M''] {f : M โ M'} {s : Set M} {n : โโ} {t : Set M'}
{g : M' โ M''}, ContMDiffOn I' I'' n g t โ ContMDiffOn I I' n f s โ ContMDiffOn I I'' n (g โ f) (s โฉ f โปยน' t)
This theorem states that for any non-trivially normed field `๐`, and spaces `E`, `E'`, `E''` that are normed commutative add groups over `๐` and also normed spaces over `๐`, and topological spaces `H`, `H'`, `H''` with given model-with-corners `I`, `I'`, `I''` respectively, and `M`, `M'`, `M''` which are topological spaces and charted spaces modeled on `H`, `H'`, `H''` respectively; if you have a function `f : M โ M'` that is `C^n` continously differentiable on a set `s` and another function `g : M' โ M''` that is `C^n` continuously differentiable on a set `t`, then the composition `(g โ f)` is also `C^n` continuously differentiable on the intersection of the set `s` and the preimage of the set `t` under the function `f`, denoted as `(s โฉ f โปยน' t)`.
More concisely: Given non-trivially normed fields `๐`, normed commutative add groups and normed spaces `E`, `E'`, `E''` over `๐`, and topological spaces `H`, `H'`, `H''` with model-with-corners `I`, `I'`, `I''`, if `f : H โ H'` is `C^n` continuously differentiable on a set `s` and `g : H' โ H''` is `C^n` continuously differentiable on a set `t`, then their composition `g โ f` is `C^n` continuously differentiable on the intersection of `s` and the preimage of `t` under `f`.
|
contMDiffOn_openEmbedding_symm
theorem contMDiffOn_openEmbedding_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}
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : Nonempty M] {e : M โ H} (h : OpenEmbedding e)
{n : WithTop โ}, ContMDiffOn I I n (โ(OpenEmbedding.toPartialHomeomorph e h).symm) (Set.range e)
This theorem asserts that if the structure of a charted space on a manifold `M` is given by an open embedding `e` from `M` to another space `H`, then the inverse of `e` is continuously differentiable. The conditions are as follows: `๐` is a nontrivially normed field, `E` is a normed abelian addable group over `๐`, `H` is a topological space, and `I` is a model with corners from `E` to `H`. `M` is also a nonempty topological space. The theorem states that for any `n` of type `WithTop โ`, the inverse of the partial homeomorphism created by the open embedding `e` is continuously `n` times differentiable on the range of `e`.
More concisely: If `e` is an open embedding of a manifold `M` into a topological space `H` over a nontrivially normed field `๐`, then the inverse of `e` is continuously differentiable of arbitrary order on the range of `e`.
|
contMDiff_of_mulTSupport
theorem contMDiff_of_mulTSupport :
โ {๐ : 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] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace ๐ E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{n : โโ} [inst_11 : One M'] {f : M โ M'}, (โ x โ mulTSupport f, ContMDiffAt I I' n f x) โ ContMDiff I I' n f
The theorem `contMDiff_of_mulTSupport` states that for any function `f` mapping from a manifold `M` to another manifold `M'`, if the function `f` is continuously differentiable at each point `x` in the topological support of `f`, then the function `f` is continuously differentiable.
Here, the topological support of `f` is defined as the closure of the set of all points where the function `f` is not equal to `1`. The manifolds `M` and `M'` are embedded in topological spaces `H` and `H'`, respectively, with corresponding model with corners `I` and `I'`. The function `f` is said to be continuously differentiable of order `n` if it is continuously differentiable at all points up to order `n`.
More concisely: If a continuously differentiable function `f` from manifold `M` to manifold `M'` has its topological support equal to the closure of its points where it's not equal to `1`, then `f` is continuously differentiable.
|
SmoothWithinAt.comp'
theorem SmoothWithinAt.comp' :
โ {๐ : 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] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace ๐ E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{E'' : Type u_8} [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace ๐ E''] {H'' : Type u_9}
[inst_13 : TopologicalSpace H''] {I'' : ModelWithCorners ๐ E'' H''} {M'' : Type u_10}
[inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M''] {f : M โ M'} {s : Set M} {t : Set M'}
{g : M' โ M''} (x : M),
SmoothWithinAt I' I'' g t (f x) โ SmoothWithinAt I I' f s x โ SmoothWithinAt I I'' (g โ f) (s โฉ f โปยน' t) x
The theorem `SmoothWithinAt.comp'` states that for any nontrivially normed field `๐`, normed additive commutative groups `E`, `E'` and `E''`, topological spaces `H`, `H'`, `H''`, `M`, `M'` and `M''`, models with corners `I`, `I'` and `I''`, and charted spaces `M`, `M'` and `M''` with respect to `H`, `H'` and `H''` respectively, if `f` is a `C^โ` (infinitely differentiable) function within a set `s` at a point `x` and `g` is a `C^โ` function within a set `t` at the point `f(x)`, then the composition of `g` and `f` is also a `C^โ` function within the intersection of `s` and the pre-image of `t` under `f` at the point `x`. Here the sets `s` and `t` are subsets of `M` and `M'` respectively. This theorem formalizes the fact that the composition of infinitely differentiable functions remains infinitely differentiable.
More concisely: If `f: M โ M'` and `g: M' โ M''` are infinitely differentiable functions, then their composition `g โ f: M โ M''` is also infinitely differentiable on the subset of `M` where both `f` and `g` are defined.
|
smooth_id
theorem smooth_id :
โ {๐ : 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], Smooth I I id
The theorem `smooth_id` states that for any nontrivially normed field `๐`, normed additive commutative group `E`, topological space `H`, `M`, model with corners `I` from `๐`, `E` to `H`, and `M` being a charted space modeled on `H` under `I`, the identity function is a smooth function from this manifolds to itself under the given structures. This is a common concept in differential geometry where properties of smooth functions (infinitely differentiable functions) are studied on manifolds.
More concisely: For any nontrivially normed field `๐`, normed additive commutative group `E`, topological space `H`, and charted space `M` modeled on `H` under an `I`-chart from `๐` to `H`, the identity function is a smooth function from `M` to itself.
|
ContMDiff.comp
theorem ContMDiff.comp :
โ {๐ : 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] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace ๐ E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{E'' : Type u_8} [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace ๐ E''] {H'' : Type u_9}
[inst_13 : TopologicalSpace H''] {I'' : ModelWithCorners ๐ E'' H''} {M'' : Type u_10}
[inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M''] {f : M โ M'} {n : โโ} {g : M' โ M''},
ContMDiff I' I'' n g โ ContMDiff I I' n f โ ContMDiff I I'' n (g โ f)
This theorem states that the composition of `C^n` functions is also a `C^n` function. More specifically, given a nontrivially normed field `๐`, two normed add commutative groups `E` and `E'`, and any three topological spaces `M`, `M'`, `M''`, with their respective charted spaces and their model with corners `I`, `I'`, `I''`. If we have two functions `f` and `g`, where `f` maps `M` to `M'` and `g` maps `M'` to `M''`, and both of these functions are `C^n` (continuously differentiable up to the n-th derivative), then the composition of these two functions `(g โ f)` is also `C^n`.
More concisely: Given two continuously differentiable functions `f: M โ E'` and `g: M' โ M''` between nontrivially normed fields and charted spaces, their composition `g โ f: M โ M''` is also continuously differentiable up to order `n`.
|
ContMDiffAt.comp
theorem ContMDiffAt.comp :
โ {๐ : 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] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace ๐ E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{E'' : Type u_8} [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace ๐ E''] {H'' : Type u_9}
[inst_13 : TopologicalSpace H''] {I'' : ModelWithCorners ๐ E'' H''} {M'' : Type u_10}
[inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M''] {f : M โ M'} {n : โโ} {g : M' โ M''} (x : M),
ContMDiffAt I' I'' n g (f x) โ ContMDiffAt I I' n f x โ ContMDiffAt I I'' n (g โ f) x
The theorem `ContMDiffAt.comp` states that for any non-trivially normed field, given a set of types and spaces (that satisfy certain properties such as being topological spaces, charted spaces, or normed spaces), if we have two functions, `f` and `g`, and a point `x`, then if `g` is `C^n` continuous (i.e., all derivatives up to the `n`th order of `g` exist and are continuous) at the image of `x` under `f`, and `f` is `C^n` continuous at `x`, then their composition `g โ f` is also `C^n` continuous at `x`.
In simpler terms, if `f` and `g` are suitably smooth functions, then their composition is also smoothly differentiable. This is a formalized version in Lean 4 of the standard result in real analysis and differential geometry that the composition of differentiable functions is differentiable.
More concisely: If `f` is `C^n` continuous at `x` and `g` is `C^n` continuous at `f(x)`, then their composition `g โ f` is `C^n` continuous at `x`.
|
contMDiffAt_const
theorem contMDiffAt_const :
โ {๐ : 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] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace ๐ E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{x : M} {n : โโ} {c : M'}, ContMDiffAt I I' n (fun x => c) x
This theorem, `contMDiffAt_const`, states that for any nontrivially normed field `๐`, a normed additive commutative group `E`, a normed space `๐ E`, a topological space `H`, a model with corners `I` with respect to `๐, E, H`, a topological space `M`, a charted space `H M`, a normed additive commutative group `E'`, a normed space `๐ E'`, a topological space `H'`, a model with corners `I'` with respect to `๐, E', H'`, a topological space `M'`, a charted space `H' M'`, an element `x` of `M`, an infinite natural number `n`, and a constant `c` of `M'`, the function that maps every element to the constant `c` is continuously differentiable at `x` with respect to the models with corners `I` and `I'`. Similarly, this theorem could be stated as "a constant function is continuously differentiable at any point".
More concisely: Given nontrivially normed fields ๐, normed additive commutative groups E, and continuous functions f : M -> M' between topological spaces with charts H M and H' M' respectively, where f maps each point x in M to a constant c in M', the function f is continuously differentiable at x with respect to the models with corners I and I'.
|
contMDiffAt_of_not_mem_mulTSupport
theorem contMDiffAt_of_not_mem_mulTSupport :
โ {๐ : 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] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace ๐ E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{f : M โ M'} [inst_11 : One M'] {x : M}, x โ mulTSupport f โ โ (n : โโ), ContMDiffAt I I' n f x
The theorem `contMDiffAt_of_not_mem_mulTSupport` states that for a function `f` from a manifold `M` to another manifold `M'`, if a point `x` is not in the topological support of `f` (i.e., `x` is not in the closure of the set of points where `f` is not equal to 1), then `f` is continuously differentiable at `x` for any order of differentiation `n`. The manifolds `M` and `M'` are equipped with various structures such as topological space, normed group, and normed space, and the field `๐` is a nontrivially normed field. The differentiability is defined with respect to given model space structures `I` and `I'` on `M` and `M'`, respectively.
More concisely: If a point `x` in a manifold `M` with given model space structures `I` is not in the closure of the set of points where a function `f : M -> M'` with given model space structures `I'` is not equal to 1, then `f` is continuously differentiable at `x` for all orders of differentiation.
|
ContMDiffOn.comp
theorem ContMDiffOn.comp :
โ {๐ : 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] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace ๐ E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{E'' : Type u_8} [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace ๐ E''] {H'' : Type u_9}
[inst_13 : TopologicalSpace H''] {I'' : ModelWithCorners ๐ E'' H''} {M'' : Type u_10}
[inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M''] {f : M โ M'} {s : Set M} {n : โโ} {t : Set M'}
{g : M' โ M''}, ContMDiffOn I' I'' n g t โ ContMDiffOn I I' n f s โ s โ f โปยน' t โ ContMDiffOn I I'' n (g โ f) s
This theorem states that for any nontrivially normed field `๐` and any types `E`, `H`, `M`, `E'`, `H'`, `M'`, `E''`, `H''`, `M''` that satisfy certain conditions (such as `E` and `E'` being normed additive commutative groups and `H` and `H'` being topological spaces), if we have two functions `f : M โ M'` and `g : M' โ M''` such that `f` is continuously differentiable of any order `n` on a set `s`, and `g` is continuously differentiable of the same order `n` on a set `t`, and the set `s` is a subset of the preimage of `t` under `f`, then the composition of `g` and `f` (i.e., `g โ f`) is also continuously differentiable of order `n` on the set `s`. This theorem is a statement about the preservation of continuous differentiability under function composition.
More concisely: If `f : M โ M'` and `g : M' โ M''` are continuously differentiable functions of order `n` on sets `s` and `t`, respectively, where `s` is a subset of the preimage of `t` under `f`, then the composition `g โ f` is continuously differentiable of order `n` on `s`.
|
SmoothAt.comp_smoothWithinAt
theorem SmoothAt.comp_smoothWithinAt :
โ {๐ : 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] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace ๐ E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{E'' : Type u_8} [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace ๐ E''] {H'' : Type u_9}
[inst_13 : TopologicalSpace H''] {I'' : ModelWithCorners ๐ E'' H''} {M'' : Type u_10}
[inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M''] {f : M โ M'} {s : Set M} {g : M' โ M''} (x : M),
SmoothAt I' I'' g (f x) โ SmoothWithinAt I I' f s x โ SmoothWithinAt I I'' (g โ f) s x
This is a theorem about the composition of two smooth functions, and it's stated in the context of manifolds with corners. The theorem says that if we have a function `g` that is infinitely differentiable at the point `f(x)`, and another function `f` that is infinitely differentiable within a set `s` at the point `x`, then the composition of `g` and `f` is also infinitely differentiable within the set `s` at the point `x`.
More technically, the theorem is stated in the setting of differential geometry. Here `๐` is an (implicitly real) normed field, `E`, `E'` and `E''` are normed vector spaces over `๐`, `H`, `H'` and `H''` are topological spaces, `I`, `I'` and `I''` are models with corners (which are generalizations of charts used in manifolds) on `E`, `E'` and `E''` respectively, `M`, `M'` and `M''` are manifolds modeled on `(E, H)`, `(E', H')` and `(E'', H'')` respectively, `f` is a map from `M` to `M'`, `g` is a map from `M'` to `M''`, `s` is a subset of `M`, and `x` is a point in `M`.
More concisely: If `f` is an infinitely differentiable map from a manifold `M` to another manifold `M'`, `g` is an infinitely differentiable map from `M'` to a manifold `M''`, and `s` is an open subset of `M` containing the point `x`, then the composition `g โ f` is an infinitely differentiable map from `s` to `M''` at `x`.
|
contMDiff_of_tsupport
theorem contMDiff_of_tsupport :
โ {๐ : 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] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace ๐ E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{n : โโ} [inst_11 : Zero M'] {f : M โ M'}, (โ x โ tsupport f, ContMDiffAt I I' n f x) โ ContMDiff I I' n f
The theorem `contMDiff_of_tsupport` states that a function `f` from a manifold `M` to another manifold `M'` is continuously differentiable (denoted as `ContMDiff`) if it is continuously differentiable at each point `x` in the topological support of `f` (denoted as `tsupport f`). Here, the topological support of a function is the closure of the set of its nonzero points. The level of differentiability is denoted by `n`, which can be any natural number or infinity (`โโ`). The spaces `M` and `M'` are modeled on the normed vector spaces `E` and `E'` respectively, via the model with corners `I` and `I'`.
More concisely: A function `f` from a manifold `M` to another manifold `M'` is continuously differentiable of class `C^n` if it is continuously differentiable at each point in the closure of the set of its nonzero values.
|
contMDiff_id
theorem contMDiff_id :
โ {๐ : 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] {n : โโ}, ContMDiff I I n id
This theorem, `contMDiff_id`, states that for any nontrivially normed field `๐`, normed additive commutative group `E`, topological space `H`, model with corners `I` (mapping `H` into `E`), and charted space `M` with chart modelled on `H`, the identity function is continuously differentiable to any order `n` in the manifold `M` with corners `I`. Here, `n` could be any natural number or infinity (`โโ`).
More concisely: For any nontrivially normed field `๐`, normed additive commutative group `E`, topological space `H`, model with corners `I` mapping `H` into `E`, and charted space `M` with chart modelled on `H`, the identity function on `M` with corners `I` is continuously differentiable to any order `n` in the manifold `M`.
|
contMDiffAt_id
theorem contMDiffAt_id :
โ {๐ : 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] {x : M} {n : โโ},
ContMDiffAt I I n id x
This theorem, `contMDiffAt_id`, states that the identity function is continuously differentiable at any point `x` in a charted space `M` that is modeled on a normed space `E` over a nontrivially normed field `๐`, with the model being provided by a model with corners `I`. This holds for all degrees of differentiability `n`, where `n` is a natural number or infinity (`โโ`).
More concisely: The identity function is continuously differentiable up to order `n` at any point `x` in the charted space `M` modeled on the normed space `E` over the nontrivially normed field `๐`, for all natural numbers `n` or infinity.
|
SmoothOn.comp'
theorem SmoothOn.comp' :
โ {๐ : 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] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace ๐ E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{E'' : Type u_8} [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace ๐ E''] {H'' : Type u_9}
[inst_13 : TopologicalSpace H''] {I'' : ModelWithCorners ๐ E'' H''} {M'' : Type u_10}
[inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M''] {f : M โ M'} {s : Set M} {t : Set M'}
{g : M' โ M''}, SmoothOn I' I'' g t โ SmoothOn I I' f s โ SmoothOn I I'' (g โ f) (s โฉ f โปยน' t)
This theorem states that given a nontrivially normed field ๐, two normed additive commutative groups E and E', two normed spaces ๐ E and ๐ E', two topological spaces H and H', two models with corners I and I' where I is a model with corners ๐ E H and I' is a model with corners ๐ E' H', and two charted spaces M and M' where M is a topological space with charted space H M and M' is a topological space with charted space H' M'. Also given is a function f from M to M', and two sets s of M and t of M'. Now, if we have another normed additive commutative group E'', normed space ๐ E'', topological space H'', model with corner I'' (a model with corners ๐ E'' H''), and charted space M'' (a topological space with charted space H'' M''), and a function g from M' to M''. The theorem asserts that if the function g is smooth on t and the function f is smooth on s, then the composition of g and f (g โ f) is smooth on the intersection of s and the preimage of t under f.
In simpler terms, this theorem assures us that we can compose smooth functions to get another smooth function under certain conditions.
More concisely: Given smooth functions between charted spaces with compatible domain intersections and images, their composition is smooth on the intersection of the domains.
|
contMDiff_openEmbedding
theorem contMDiff_openEmbedding :
โ {๐ : 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 : Nonempty M] {e : M โ H} (h : OpenEmbedding e)
{n : WithTop โ}, ContMDiff I I n e
This theorem states that if a manifold `M` is given a `ChartedSpace` structure through an open embedding `e : M โ H`, then `e` is continuously differentiable. More specifically, for any non-trivial normed field `๐`, any normed additive commutative group `E` over `๐`, any topological space `H`, any model with corners `I : ModelWithCorners ๐ E H`, and any topological space `M` that is nonempty, if `e : M โ H` is an open embedding, then `e` is `n`-times continuously differentiable where `n` is an option type wrapping natural numbers or the top element, depending on the definition of `WithTop` type.
More concisely: If a manifold `M` is given a `ChartedSpace` structure through an open embedding `e : M โ H` into a topological space `H`, then `e` is `n`-times continuously differentiable for some `n`.
|
ContMDiffAt.comp_contMDiffWithinAt
theorem ContMDiffAt.comp_contMDiffWithinAt :
โ {๐ : 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] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace ๐ E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{E'' : Type u_8} [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace ๐ E''] {H'' : Type u_9}
[inst_13 : TopologicalSpace H''] {I'' : ModelWithCorners ๐ E'' H''} {M'' : Type u_10}
[inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M''] {f : M โ M'} {s : Set M} {n : โโ} {g : M' โ M''}
(x : M), ContMDiffAt I' I'' n g (f x) โ ContMDiffWithinAt I I' n f s x โ ContMDiffWithinAt I I'' n (g โ f) s x
The theorem `ContMDiffAt.comp_contMDiffWithinAt` states that if a function `g` is continuously differentiable `n` times at `f(x)`, and a function `f` is continuously differentiable `n` times within a set `s`, at `x`, then their composite function `(g โ f)` is also continuously differentiable `n` times within the set `s` at `x`.
This theorem is established in the context of a rich structure of topological and differentiable spaces. Here, `๐` is a nontrivial normed field, `E`, `E'`, and `E''` are normed additive commutative groups over `๐` and also `๐`-vector spaces, `H`, `H'`, and `H''` are topological spaces, `I`, `I'`, and `I''` are model with corners structures over these spaces, and `M`, `M'`, and `M''` are topological spaces with a charted space structure in relation to `H`, `H'`, and `H''` respectively. The function `f` maps `M` to `M'`, `g` maps `M'` to `M''`, and `n` is a natural number indicating the order of differentiability.
More concisely: If functions `f : M โ M'` and `g : M' โ M''` are continuously differentiable of order `n` at `x` with `x โ M` and `f` is continuously differentiable of order `n` within set `s โ I` at `x`, then their composite function `g โ f` is continuously differentiable of order `n` within `s` at `x`.
|
contMDiff_const
theorem contMDiff_const :
โ {๐ : 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] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace ๐ E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{n : โโ} {c : M'}, ContMDiff I I' n fun x => c
This theorem, `contMDiff_const`, states that for every nontrivially normed field `๐`, normed additive commutative group `E`, normed space `๐ E`, topological space `H`, model with corners `I` over `๐`, `E` and `H`, topological space `M`, and charted space `H M`; and similarly for `E'`, `H'`, `I'`, and `M'`; and for any `n` in the set of natural numbers extended with infinity `โโ` and any constant `c` in `M'`, the function which maps every element of `M` to `c` is continuously differentiable `n` times. In mathematical terms, it says that constant functions are infinitely differentiable.
More concisely: For any nontrivially normed field `๐`, normed additive commutative group `E`, and topological spaces `H`, `M`, the constant function from `M` to `๐` is infinitely differentiable.
|