Smoothness of standard maps associated to the product of manifolds #
This file contains results about smoothness of standard maps associated to products and sums (disjoint unions) of smooth manifolds:
- if
f
andg
areC^n
, so is their point-wise product. - the component projections from a product of manifolds are smooth.
- functions into a product (pi type) are
C^n
iff their components are - if
M
andN
are manifolds modelled over the same space,Sum.inl
andSum.inr
areC^n
, as areSum.elim
,Sum.map
andSum.swap
.
Alias of ContMDiffWithinAt.prodMk
.
Alias of ContMDiffWithinAt.prodMk_space
.
Alias of ContMDiffAt.prodMk
.
Alias of ContMDiffAt.prodMk_space
.
Alias of ContMDiffOn.prodMk
.
Alias of ContMDiffOn.prodMk_space
.
Alias of ContMDiff.prodMk
.
Alias of ContMDiff.prodMk_space
.
ContMDiffWithinAt.comp
for a function of two arguments.
ContMDiffWithinAt.comp₂
, with a separate argument for point equality.
ContMDiffAt.comp
for a function of two arguments.
ContMDiffAt.comp₂
, with a separate argument for point equality.
Curried C^n
functions are C^n
in the first coordinate.
Alias of ContMDiffWithinAt.curry_left
.
Curried C^n
functions are C^n
in the first coordinate.
Curried C^n
functions are C^n
in the second coordinate.
Alias of ContMDiffWithinAt.curry_right
.
Curried C^n
functions are C^n
in the second coordinate.
Curried C^n
functions are C^n
in the first coordinate.
Alias of ContMDiffAt.curry_left
.
Curried C^n
functions are C^n
in the first coordinate.
Curried C^n
functions are C^n
in the second coordinate.
Alias of ContMDiffAt.curry_right
.
Curried C^n
functions are C^n
in the second coordinate.
Curried C^n
functions are C^n
in the first coordinate.
Alias of ContMDiffOn.curry_left
.
Curried C^n
functions are C^n
in the first coordinate.
Curried C^n
functions are C^n
in the second coordinate.
Alias of ContMDiffOn.curry_right
.
Curried C^n
functions are C^n
in the second coordinate.
Curried C^n
functions are C^n
in the first coordinate.
Alias of ContMDiff.curry_left
.
Curried C^n
functions are C^n
in the first coordinate.
Curried C^n
functions are C^n
in the second coordinate.
Alias of ContMDiff.curry_right
.
Curried C^n
functions are C^n
in the second coordinate.
The product map of two C^n
functions within a set at a point is C^n
within the product set at the product point.
Alias of ContMDiffWithinAt.prodMap'
.
The product map of two C^n
functions within a set at a point is C^n
within the product set at the product point.
Alias of ContMDiffWithinAt.prodMap
.
Alias of ContMDiffAt.prodMap
.
Alias of ContMDiffAt.prodMap'
.
Alias of ContMDiffOn.prodMap
.
Alias of ContMDiff.prodMap
.
Regularity of functions with codomain Π i, F i
#
We have no ModelWithCorners.pi
yet, so we prove lemmas about functions f : M → Π i, F i
and
use 𝓘(𝕜, Π i, F i)
as the model space.