Smoothness of standard maps associated to the product of manifolds #
This file contains results about smoothness of standard maps associated to products of manifolds
- if
fandgare smooth, so is their point-wise product. - the component projections from a product of manifolds are smooth.
- functions into a product (pi type) are smooth iff their components are
theorem
ContMDiffWithinAt.prod_mk
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{s : Set M}
{x : M}
{n : ℕ∞}
{f : M → M'}
{g : M → N'}
(hf : ContMDiffWithinAt I I' n f s x)
(hg : ContMDiffWithinAt I J' n g s x)
:
ContMDiffWithinAt I (I'.prod J') n (fun (x : M) => (f x, g x)) s x
theorem
ContMDiffWithinAt.prod_mk_space
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{s : Set M}
{x : M}
{n : ℕ∞}
{f : M → E'}
{g : M → F'}
(hf : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 E') n f s x)
(hg : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 F') n g s x)
:
ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (E' × F')) n (fun (x : M) => (f x, g x)) s x
theorem
ContMDiffAt.prod_mk
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{x : M}
{n : ℕ∞}
{f : M → M'}
{g : M → N'}
(hf : ContMDiffAt I I' n f x)
(hg : ContMDiffAt I J' n g x)
:
ContMDiffAt I (I'.prod J') n (fun (x : M) => (f x, g x)) x
theorem
ContMDiffAt.prod_mk_space
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{x : M}
{n : ℕ∞}
{f : M → E'}
{g : M → F'}
(hf : ContMDiffAt I (modelWithCornersSelf 𝕜 E') n f x)
(hg : ContMDiffAt I (modelWithCornersSelf 𝕜 F') n g x)
:
ContMDiffAt I (modelWithCornersSelf 𝕜 (E' × F')) n (fun (x : M) => (f x, g x)) x
theorem
ContMDiffOn.prod_mk
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{s : Set M}
{n : ℕ∞}
{f : M → M'}
{g : M → N'}
(hf : ContMDiffOn I I' n f s)
(hg : ContMDiffOn I J' n g s)
:
ContMDiffOn I (I'.prod J') n (fun (x : M) => (f x, g x)) s
theorem
ContMDiffOn.prod_mk_space
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{s : Set M}
{n : ℕ∞}
{f : M → E'}
{g : M → F'}
(hf : ContMDiffOn I (modelWithCornersSelf 𝕜 E') n f s)
(hg : ContMDiffOn I (modelWithCornersSelf 𝕜 F') n g s)
:
ContMDiffOn I (modelWithCornersSelf 𝕜 (E' × F')) n (fun (x : M) => (f x, g x)) s
theorem
ContMDiff.prod_mk
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{n : ℕ∞}
{f : M → M'}
{g : M → N'}
(hf : ContMDiff I I' n f)
(hg : ContMDiff I J' n g)
:
ContMDiff I (I'.prod J') n fun (x : M) => (f x, g x)
theorem
ContMDiff.prod_mk_space
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{n : ℕ∞}
{f : M → E'}
{g : M → F'}
(hf : ContMDiff I (modelWithCornersSelf 𝕜 E') n f)
(hg : ContMDiff I (modelWithCornersSelf 𝕜 F') n g)
:
ContMDiff I (modelWithCornersSelf 𝕜 (E' × F')) n fun (x : M) => (f x, g x)
@[deprecated ContMDiffWithinAt.prod_mk (since := "2024-11-20")]
theorem
SmoothWithinAt.prod_mk
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{s : Set M}
{x : M}
{n : ℕ∞}
{f : M → M'}
{g : M → N'}
(hf : ContMDiffWithinAt I I' n f s x)
(hg : ContMDiffWithinAt I J' n g s x)
:
ContMDiffWithinAt I (I'.prod J') n (fun (x : M) => (f x, g x)) s x
Alias of ContMDiffWithinAt.prod_mk.
@[deprecated ContMDiffWithinAt.prod_mk_space (since := "2024-11-20")]
theorem
SmoothWithinAt.prod_mk_space
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{s : Set M}
{x : M}
{n : ℕ∞}
{f : M → E'}
{g : M → F'}
(hf : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 E') n f s x)
(hg : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 F') n g s x)
:
ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (E' × F')) n (fun (x : M) => (f x, g x)) s x
Alias of ContMDiffWithinAt.prod_mk_space.
@[deprecated ContMDiffAt.prod_mk (since := "2024-11-20")]
theorem
SmoothAt.prod_mk
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{x : M}
{n : ℕ∞}
{f : M → M'}
{g : M → N'}
(hf : ContMDiffAt I I' n f x)
(hg : ContMDiffAt I J' n g x)
:
ContMDiffAt I (I'.prod J') n (fun (x : M) => (f x, g x)) x
Alias of ContMDiffAt.prod_mk.
@[deprecated ContMDiffAt.prod_mk_space (since := "2024-11-20")]
theorem
SmoothAt.prod_mk_space
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{x : M}
{n : ℕ∞}
{f : M → E'}
{g : M → F'}
(hf : ContMDiffAt I (modelWithCornersSelf 𝕜 E') n f x)
(hg : ContMDiffAt I (modelWithCornersSelf 𝕜 F') n g x)
:
ContMDiffAt I (modelWithCornersSelf 𝕜 (E' × F')) n (fun (x : M) => (f x, g x)) x
Alias of ContMDiffAt.prod_mk_space.
@[deprecated ContMDiffOn.prod_mk (since := "2024-11-20")]
theorem
SmoothOn.prod_mk
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{s : Set M}
{n : ℕ∞}
{f : M → M'}
{g : M → N'}
(hf : ContMDiffOn I I' n f s)
(hg : ContMDiffOn I J' n g s)
:
ContMDiffOn I (I'.prod J') n (fun (x : M) => (f x, g x)) s
Alias of ContMDiffOn.prod_mk.
@[deprecated ContMDiffOn.prod_mk_space (since := "2024-11-20")]
theorem
SmoothOn.prod_mk_space
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{s : Set M}
{n : ℕ∞}
{f : M → E'}
{g : M → F'}
(hf : ContMDiffOn I (modelWithCornersSelf 𝕜 E') n f s)
(hg : ContMDiffOn I (modelWithCornersSelf 𝕜 F') n g s)
:
ContMDiffOn I (modelWithCornersSelf 𝕜 (E' × F')) n (fun (x : M) => (f x, g x)) s
Alias of ContMDiffOn.prod_mk_space.
@[deprecated ContMDiff.prod_mk (since := "2024-11-20")]
theorem
Smooth.prod_mk
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{n : ℕ∞}
{f : M → M'}
{g : M → N'}
(hf : ContMDiff I I' n f)
(hg : ContMDiff I J' n g)
:
ContMDiff I (I'.prod J') n fun (x : M) => (f x, g x)
Alias of ContMDiff.prod_mk.
@[deprecated ContMDiff.prod_mk_space (since := "2024-11-20")]
theorem
Smooth.prod_mk_space
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{n : ℕ∞}
{f : M → E'}
{g : M → F'}
(hf : ContMDiff I (modelWithCornersSelf 𝕜 E') n f)
(hg : ContMDiff I (modelWithCornersSelf 𝕜 F') n g)
:
ContMDiff I (modelWithCornersSelf 𝕜 (E' × F')) n fun (x : M) => (f x, g x)
Alias of ContMDiff.prod_mk_space.
theorem
contMDiffWithinAt_fst
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{s : Set (M × N)}
{p : M × N}
:
ContMDiffWithinAt (I.prod J) I n Prod.fst s p
theorem
ContMDiffWithinAt.fst
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{f : N → M × M'}
{s : Set N}
{x : N}
(hf : ContMDiffWithinAt J (I.prod I') n f s x)
:
ContMDiffWithinAt J I n (fun (x : N) => (f x).1) s x
theorem
contMDiffAt_fst
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{p : M × N}
:
ContMDiffAt (I.prod J) I n Prod.fst p
theorem
contMDiffOn_fst
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{s : Set (M × N)}
:
ContMDiffOn (I.prod J) I n Prod.fst s
theorem
contMDiff_fst
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
:
ContMDiff (I.prod J) I n Prod.fst
@[deprecated contMDiffWithinAt_fst (since := "2024-11-20")]
theorem
smoothWithinAt_fst
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{s : Set (M × N)}
{p : M × N}
:
ContMDiffWithinAt (I.prod J) I n Prod.fst s p
Alias of contMDiffWithinAt_fst.
@[deprecated contMDiffAt_fst (since := "2024-11-20")]
theorem
smoothAt_fst
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{p : M × N}
:
ContMDiffAt (I.prod J) I n Prod.fst p
Alias of contMDiffAt_fst.
@[deprecated contMDiffOn_fst (since := "2024-11-20")]
theorem
smoothOn_fst
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{s : Set (M × N)}
:
ContMDiffOn (I.prod J) I n Prod.fst s
Alias of contMDiffOn_fst.
@[deprecated contMDiff_fst (since := "2024-11-20")]
theorem
smooth_fst
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
:
ContMDiff (I.prod J) I n Prod.fst
Alias of contMDiff_fst.
theorem
ContMDiffAt.fst
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{f : N → M × M'}
{x : N}
(hf : ContMDiffAt J (I.prod I') n f x)
:
ContMDiffAt J I n (fun (x : N) => (f x).1) x
theorem
ContMDiff.fst
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{f : N → M × M'}
(hf : ContMDiff J (I.prod I') n f)
:
ContMDiff J I n fun (x : N) => (f x).1
@[deprecated ContMDiffAt.fst (since := "2024-11-20")]
theorem
SmoothAt.fst
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{f : N → M × M'}
{x : N}
(hf : ContMDiffAt J (I.prod I') n f x)
:
ContMDiffAt J I n (fun (x : N) => (f x).1) x
Alias of ContMDiffAt.fst.
@[deprecated ContMDiff.fst (since := "2024-11-20")]
theorem
Smooth.fst
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{f : N → M × M'}
(hf : ContMDiff J (I.prod I') n f)
:
ContMDiff J I n fun (x : N) => (f x).1
Alias of ContMDiff.fst.
theorem
contMDiffWithinAt_snd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{s : Set (M × N)}
{p : M × N}
:
ContMDiffWithinAt (I.prod J) J n Prod.snd s p
theorem
ContMDiffWithinAt.snd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{f : N → M × M'}
{s : Set N}
{x : N}
(hf : ContMDiffWithinAt J (I.prod I') n f s x)
:
ContMDiffWithinAt J I' n (fun (x : N) => (f x).2) s x
theorem
contMDiffAt_snd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{p : M × N}
:
ContMDiffAt (I.prod J) J n Prod.snd p
theorem
contMDiffOn_snd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{s : Set (M × N)}
:
ContMDiffOn (I.prod J) J n Prod.snd s
theorem
contMDiff_snd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
:
ContMDiff (I.prod J) J n Prod.snd
@[deprecated contMDiffWithinAt_snd (since := "2024-11-20")]
theorem
smoothWithinAt_snd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{s : Set (M × N)}
{p : M × N}
:
ContMDiffWithinAt (I.prod J) J n Prod.snd s p
Alias of contMDiffWithinAt_snd.
@[deprecated contMDiffAt_snd (since := "2024-11-20")]
theorem
smoothAt_snd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{p : M × N}
:
ContMDiffAt (I.prod J) J n Prod.snd p
Alias of contMDiffAt_snd.
@[deprecated contMDiffOn_snd (since := "2024-11-20")]
theorem
smoothOn_snd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{s : Set (M × N)}
:
ContMDiffOn (I.prod J) J n Prod.snd s
Alias of contMDiffOn_snd.
@[deprecated contMDiff_snd (since := "2024-11-20")]
theorem
smooth_snd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
:
ContMDiff (I.prod J) J n Prod.snd
Alias of contMDiff_snd.
theorem
ContMDiffAt.snd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{f : N → M × M'}
{x : N}
(hf : ContMDiffAt J (I.prod I') n f x)
:
ContMDiffAt J I' n (fun (x : N) => (f x).2) x
theorem
ContMDiff.snd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{f : N → M × M'}
(hf : ContMDiff J (I.prod I') n f)
:
ContMDiff J I' n fun (x : N) => (f x).2
@[deprecated ContMDiffAt.snd (since := "2024-11-20")]
theorem
SmoothAt.snd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{f : N → M × M'}
{x : N}
(hf : ContMDiffAt J (I.prod I') n f x)
:
ContMDiffAt J I' n (fun (x : N) => (f x).2) x
Alias of ContMDiffAt.snd.
@[deprecated ContMDiff.snd (since := "2024-11-20")]
theorem
Smooth.snd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{f : N → M × M'}
(hf : ContMDiff J (I.prod I') n f)
:
ContMDiff J I' n fun (x : N) => (f x).2
Alias of ContMDiff.snd.
theorem
contMDiffWithinAt_prod_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{s : Set M}
{x : M}
{n : ℕ∞}
(f : M → M' × N')
:
ContMDiffWithinAt I (I'.prod J') n f s x ↔ ContMDiffWithinAt I I' n (Prod.fst ∘ f) s x ∧ ContMDiffWithinAt I J' n (Prod.snd ∘ f) s x
theorem
contMDiffWithinAt_prod_module_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F₁ : Type u_14}
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
{F₂ : Type u_15}
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{s : Set M}
{x : M}
{n : ℕ∞}
(f : M → F₁ × F₂)
:
ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (F₁ × F₂)) n f s x ↔ ContMDiffWithinAt I (modelWithCornersSelf 𝕜 F₁) n (Prod.fst ∘ f) s x ∧ ContMDiffWithinAt I (modelWithCornersSelf 𝕜 F₂) n (Prod.snd ∘ f) s x
theorem
contMDiffAt_prod_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{x : M}
{n : ℕ∞}
(f : M → M' × N')
:
ContMDiffAt I (I'.prod J') n f x ↔ ContMDiffAt I I' n (Prod.fst ∘ f) x ∧ ContMDiffAt I J' n (Prod.snd ∘ f) x
theorem
contMDiffAt_prod_module_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F₁ : Type u_14}
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
{F₂ : Type u_15}
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{x : M}
{n : ℕ∞}
(f : M → F₁ × F₂)
:
ContMDiffAt I (modelWithCornersSelf 𝕜 (F₁ × F₂)) n f x ↔ ContMDiffAt I (modelWithCornersSelf 𝕜 F₁) n (Prod.fst ∘ f) x ∧ ContMDiffAt I (modelWithCornersSelf 𝕜 F₂) n (Prod.snd ∘ f) x
theorem
contMDiffOn_prod_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{s : Set M}
{n : ℕ∞}
(f : M → M' × N')
:
ContMDiffOn I (I'.prod J') n f s ↔ ContMDiffOn I I' n (Prod.fst ∘ f) s ∧ ContMDiffOn I J' n (Prod.snd ∘ f) s
theorem
contMDiffOn_prod_module_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F₁ : Type u_14}
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
{F₂ : Type u_15}
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{s : Set M}
{n : ℕ∞}
(f : M → F₁ × F₂)
:
ContMDiffOn I (modelWithCornersSelf 𝕜 (F₁ × F₂)) n f s ↔ ContMDiffOn I (modelWithCornersSelf 𝕜 F₁) n (Prod.fst ∘ f) s ∧ ContMDiffOn I (modelWithCornersSelf 𝕜 F₂) n (Prod.snd ∘ f) s
theorem
contMDiff_prod_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{n : ℕ∞}
(f : M → M' × N')
:
theorem
contMDiff_prod_module_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F₁ : Type u_14}
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
{F₂ : Type u_15}
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{n : ℕ∞}
(f : M → F₁ × F₂)
:
ContMDiff I (modelWithCornersSelf 𝕜 (F₁ × F₂)) n f ↔ ContMDiff I (modelWithCornersSelf 𝕜 F₁) n (Prod.fst ∘ f) ∧ ContMDiff I (modelWithCornersSelf 𝕜 F₂) n (Prod.snd ∘ f)
theorem
contMDiff_prod_assoc
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
:
@[deprecated contMDiffAt_prod_iff (since := "2024-11-20")]
theorem
smoothAt_prod_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{x : M}
{n : ℕ∞}
(f : M → M' × N')
:
ContMDiffAt I (I'.prod J') n f x ↔ ContMDiffAt I I' n (Prod.fst ∘ f) x ∧ ContMDiffAt I J' n (Prod.snd ∘ f) x
Alias of contMDiffAt_prod_iff.
@[deprecated contMDiff_prod_iff (since := "2024-11-20")]
theorem
smooth_prod_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{n : ℕ∞}
(f : M → M' × N')
:
Alias of contMDiff_prod_iff.
@[deprecated contMDiff_prod_assoc (since := "2024-11-20")]
theorem
smooth_prod_assoc
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
:
Alias of contMDiff_prod_assoc.
theorem
ContMDiffWithinAt.prod_map'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{f : M → M'}
{s : Set M}
{n : ℕ∞}
{g : N → N'}
{r : Set N}
{p : M × N}
(hf : ContMDiffWithinAt I I' n f s p.1)
(hg : ContMDiffWithinAt J J' n g r p.2)
:
ContMDiffWithinAt (I.prod J) (I'.prod J') n (Prod.map f g) (s ×ˢ r) p
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.
theorem
ContMDiffWithinAt.prod_map
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{f : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
{g : N → N'}
{r : Set N}
{y : N}
(hf : ContMDiffWithinAt I I' n f s x)
(hg : ContMDiffWithinAt J J' n g r y)
:
ContMDiffWithinAt (I.prod J) (I'.prod J') n (Prod.map f g) (s ×ˢ r) (x, y)
theorem
ContMDiffAt.prod_map
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{f : M → M'}
{x : M}
{n : ℕ∞}
{g : N → N'}
{y : N}
(hf : ContMDiffAt I I' n f x)
(hg : ContMDiffAt J J' n g y)
:
ContMDiffAt (I.prod J) (I'.prod J') n (Prod.map f g) (x, y)
theorem
ContMDiffAt.prod_map'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{f : M → M'}
{n : ℕ∞}
{g : N → N'}
{p : M × N}
(hf : ContMDiffAt I I' n f p.1)
(hg : ContMDiffAt J J' n g p.2)
:
ContMDiffAt (I.prod J) (I'.prod J') n (Prod.map f g) p
theorem
ContMDiffOn.prod_map
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{f : M → M'}
{s : Set M}
{n : ℕ∞}
{g : N → N'}
{r : Set N}
(hf : ContMDiffOn I I' n f s)
(hg : ContMDiffOn J J' n g r)
:
ContMDiffOn (I.prod J) (I'.prod J') n (Prod.map f g) (s ×ˢ r)
theorem
ContMDiff.prod_map
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{f : M → M'}
{n : ℕ∞}
{g : N → N'}
(hf : ContMDiff I I' n f)
(hg : ContMDiff J J' n g)
:
@[deprecated ContMDiffWithinAt.prod_map (since := "2024-11-20")]
theorem
SmoothWithinAt.prod_map
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{f : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
{g : N → N'}
{r : Set N}
{y : N}
(hf : ContMDiffWithinAt I I' n f s x)
(hg : ContMDiffWithinAt J J' n g r y)
:
ContMDiffWithinAt (I.prod J) (I'.prod J') n (Prod.map f g) (s ×ˢ r) (x, y)
Alias of ContMDiffWithinAt.prod_map.
@[deprecated ContMDiffAt.prod_map (since := "2024-11-20")]
theorem
SmoothAt.prod_map
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{f : M → M'}
{x : M}
{n : ℕ∞}
{g : N → N'}
{y : N}
(hf : ContMDiffAt I I' n f x)
(hg : ContMDiffAt J J' n g y)
:
ContMDiffAt (I.prod J) (I'.prod J') n (Prod.map f g) (x, y)
Alias of ContMDiffAt.prod_map.
@[deprecated ContMDiffOn.prod_map (since := "2024-11-20")]
theorem
SmoothOn.prod_map
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{f : M → M'}
{s : Set M}
{n : ℕ∞}
{g : N → N'}
{r : Set N}
(hf : ContMDiffOn I I' n f s)
(hg : ContMDiffOn J J' n g r)
:
ContMDiffOn (I.prod J) (I'.prod J') n (Prod.map f g) (s ×ˢ r)
Alias of ContMDiffOn.prod_map.
@[deprecated ContMDiff.prod_map (since := "2024-11-20")]
theorem
Smooth.prod_map
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{f : M → M'}
{n : ℕ∞}
{g : N → N'}
(hf : ContMDiff I I' n f)
(hg : ContMDiff J J' n g)
:
Alias of ContMDiff.prod_map.
Smoothness 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.
theorem
contMDiffWithinAt_pi_space
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{n : ℕ∞}
{ι : Type u_16}
[Fintype ι]
{Fi : ι → Type u_17}
[(i : ι) → NormedAddCommGroup (Fi i)]
[(i : ι) → NormedSpace 𝕜 (Fi i)]
{φ : M → (i : ι) → Fi i}
:
ContMDiffWithinAt I (modelWithCornersSelf 𝕜 ((i : ι) → Fi i)) n φ s x ↔ ∀ (i : ι), ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (Fi i)) n (fun (x : M) => φ x i) s x
theorem
contMDiffOn_pi_space
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{n : ℕ∞}
{ι : Type u_16}
[Fintype ι]
{Fi : ι → Type u_17}
[(i : ι) → NormedAddCommGroup (Fi i)]
[(i : ι) → NormedSpace 𝕜 (Fi i)]
{φ : M → (i : ι) → Fi i}
:
ContMDiffOn I (modelWithCornersSelf 𝕜 ((i : ι) → Fi i)) n φ s ↔ ∀ (i : ι), ContMDiffOn I (modelWithCornersSelf 𝕜 (Fi i)) n (fun (x : M) => φ x i) s
theorem
contMDiffAt_pi_space
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{x : M}
{n : ℕ∞}
{ι : Type u_16}
[Fintype ι]
{Fi : ι → Type u_17}
[(i : ι) → NormedAddCommGroup (Fi i)]
[(i : ι) → NormedSpace 𝕜 (Fi i)]
{φ : M → (i : ι) → Fi i}
:
ContMDiffAt I (modelWithCornersSelf 𝕜 ((i : ι) → Fi i)) n φ x ↔ ∀ (i : ι), ContMDiffAt I (modelWithCornersSelf 𝕜 (Fi i)) n (fun (x : M) => φ x i) x
theorem
contMDiff_pi_space
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{n : ℕ∞}
{ι : Type u_16}
[Fintype ι]
{Fi : ι → Type u_17}
[(i : ι) → NormedAddCommGroup (Fi i)]
[(i : ι) → NormedSpace 𝕜 (Fi i)]
{φ : M → (i : ι) → Fi i}
:
ContMDiff I (modelWithCornersSelf 𝕜 ((i : ι) → Fi i)) n φ ↔ ∀ (i : ι), ContMDiff I (modelWithCornersSelf 𝕜 (Fi i)) n fun (x : M) => φ x i
@[deprecated contMDiffWithinAt_pi_space (since := "2024-11-20")]
theorem
smoothWithinAt_pi_space
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{n : ℕ∞}
{ι : Type u_16}
[Fintype ι]
{Fi : ι → Type u_17}
[(i : ι) → NormedAddCommGroup (Fi i)]
[(i : ι) → NormedSpace 𝕜 (Fi i)]
{φ : M → (i : ι) → Fi i}
:
ContMDiffWithinAt I (modelWithCornersSelf 𝕜 ((i : ι) → Fi i)) n φ s x ↔ ∀ (i : ι), ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (Fi i)) n (fun (x : M) => φ x i) s x
Alias of contMDiffWithinAt_pi_space.
@[deprecated contMDiffAt_pi_space (since := "2024-11-20")]
theorem
smoothAt_pi_space
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{x : M}
{n : ℕ∞}
{ι : Type u_16}
[Fintype ι]
{Fi : ι → Type u_17}
[(i : ι) → NormedAddCommGroup (Fi i)]
[(i : ι) → NormedSpace 𝕜 (Fi i)]
{φ : M → (i : ι) → Fi i}
:
ContMDiffAt I (modelWithCornersSelf 𝕜 ((i : ι) → Fi i)) n φ x ↔ ∀ (i : ι), ContMDiffAt I (modelWithCornersSelf 𝕜 (Fi i)) n (fun (x : M) => φ x i) x
Alias of contMDiffAt_pi_space.
@[deprecated contMDiffOn_pi_space (since := "2024-11-20")]
theorem
smoothOn_pi_space
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{n : ℕ∞}
{ι : Type u_16}
[Fintype ι]
{Fi : ι → Type u_17}
[(i : ι) → NormedAddCommGroup (Fi i)]
[(i : ι) → NormedSpace 𝕜 (Fi i)]
{φ : M → (i : ι) → Fi i}
:
ContMDiffOn I (modelWithCornersSelf 𝕜 ((i : ι) → Fi i)) n φ s ↔ ∀ (i : ι), ContMDiffOn I (modelWithCornersSelf 𝕜 (Fi i)) n (fun (x : M) => φ x i) s
Alias of contMDiffOn_pi_space.
@[deprecated contMDiff_pi_space (since := "2024-11-20")]
theorem
smooth_pi_space
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{n : ℕ∞}
{ι : Type u_16}
[Fintype ι]
{Fi : ι → Type u_17}
[(i : ι) → NormedAddCommGroup (Fi i)]
[(i : ι) → NormedSpace 𝕜 (Fi i)]
{φ : M → (i : ι) → Fi i}
:
ContMDiff I (modelWithCornersSelf 𝕜 ((i : ι) → Fi i)) n φ ↔ ∀ (i : ι), ContMDiff I (modelWithCornersSelf 𝕜 (Fi i)) n fun (x : M) => φ x i
Alias of contMDiff_pi_space.