Documentation

Mathlib.Geometry.Manifold.ContMDiff.Product

Smoothness of standard maps associated to the product of manifolds #

This file contains results about smoothness of standard maps associated to products of manifolds

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 : MM'} {g : MN'} (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 : ME'} {g : MF'} (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 : MM'} {g : MN'} (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 : ME'} {g : MF'} (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 : MM'} {g : MN'} (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 : ME'} {g : MF'} (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 : MM'} {g : MN'} (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 : ME'} {g : MF'} (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)
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} {f : MM'} {g : MN'} (hf : SmoothWithinAt I I' f s x) (hg : SmoothWithinAt I J' g s x) :
SmoothWithinAt I (I'.prod J') (fun (x : M) => (f x, g x)) s x
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} {f : ME'} {g : MF'} (hf : SmoothWithinAt I (modelWithCornersSelf 𝕜 E') f s x) (hg : SmoothWithinAt I (modelWithCornersSelf 𝕜 F') g s x) :
SmoothWithinAt I (modelWithCornersSelf 𝕜 (E' × F')) (fun (x : M) => (f x, g x)) s x
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} {f : MM'} {g : MN'} (hf : SmoothAt I I' f x) (hg : SmoothAt I J' g x) :
SmoothAt I (I'.prod J') (fun (x : M) => (f x, g x)) x
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} {f : ME'} {g : MF'} (hf : SmoothAt I (modelWithCornersSelf 𝕜 E') f x) (hg : SmoothAt I (modelWithCornersSelf 𝕜 F') g x) :
SmoothAt I (modelWithCornersSelf 𝕜 (E' × F')) (fun (x : M) => (f x, g x)) x
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} {f : MM'} {g : MN'} (hf : SmoothOn I I' f s) (hg : SmoothOn I J' g s) :
SmoothOn I (I'.prod J') (fun (x : M) => (f x, g x)) s
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} {f : ME'} {g : MF'} (hf : SmoothOn I (modelWithCornersSelf 𝕜 E') f s) (hg : SmoothOn I (modelWithCornersSelf 𝕜 F') g s) :
SmoothOn I (modelWithCornersSelf 𝕜 (E' × F')) (fun (x : M) => (f x, g x)) s
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'] {f : MM'} {g : MN'} (hf : Smooth I I' f) (hg : Smooth I J' g) :
Smooth I (I'.prod J') fun (x : M) => (f x, g x)
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'] {f : ME'} {g : MF'} (hf : Smooth I (modelWithCornersSelf 𝕜 E') f) (hg : Smooth I (modelWithCornersSelf 𝕜 F') g) :
Smooth I (modelWithCornersSelf 𝕜 (E' × F')) fun (x : M) => (f x, g x)
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 : NM × 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
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] {s : Set (M × N)} {p : M × N} :
SmoothWithinAt (I.prod J) I Prod.fst s p
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] {p : M × N} :
SmoothAt (I.prod J) I Prod.fst p
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] {s : Set (M × N)} :
SmoothOn (I.prod J) I Prod.fst s
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] :
Smooth (I.prod J) I Prod.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 : NM × 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 : NM × M'} (hf : ContMDiff J (I.prod I') n f) :
ContMDiff J I n fun (x : N) => (f x).1
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] {f : NM × M'} {x : N} (hf : SmoothAt J (I.prod I') f x) :
SmoothAt J I (fun (x : N) => (f x).1) x
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] {f : NM × M'} (hf : Smooth J (I.prod I') f) :
Smooth J I fun (x : N) => (f x).1
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 : NM × 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
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] {s : Set (M × N)} {p : M × N} :
SmoothWithinAt (I.prod J) J Prod.snd s p
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] {p : M × N} :
SmoothAt (I.prod J) J Prod.snd p
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] {s : Set (M × N)} :
SmoothOn (I.prod J) J Prod.snd s
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] :
Smooth (I.prod J) J Prod.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 : NM × 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 : NM × M'} (hf : ContMDiff J (I.prod I') n f) :
ContMDiff J I' n fun (x : N) => (f x).2
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] {f : NM × M'} {x : N} (hf : SmoothAt J (I.prod I') f x) :
SmoothAt J I' (fun (x : N) => (f x).2) x
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] {f : NM × M'} (hf : Smooth J (I.prod I') f) :
Smooth J I' fun (x : N) => (f x).2
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'] {n : ℕ∞} (f : MM' × N') {s : Set M} {x : M} :
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 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'] {n : ℕ∞} (f : MM' × N') {x : M} :
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 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 : MM' × N') :
ContMDiff I (I'.prod J') n f ContMDiff I I' n (Prod.fst f) ContMDiff I J' n (Prod.snd f)
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'] (f : MM' × N') {x : M} :
SmoothAt I (I'.prod J') f x SmoothAt I I' (Prod.fst f) x SmoothAt I J' (Prod.snd f) x
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'] (f : MM' × N') :
Smooth I (I'.prod J') f Smooth I I' (Prod.fst f) Smooth I J' (Prod.snd f)
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] :
Smooth ((I.prod I').prod J) (I.prod (I'.prod J)) fun (x : (M × M') × N) => (x.1.1, x.1.2, x.2)
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 : MM'} {s : Set M} {n : ℕ∞} {g : NN'} {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 : MM'} {s : Set M} {x : M} {n : ℕ∞} {g : NN'} {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 : MM'} {x : M} {n : ℕ∞} {g : NN'} {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 : MM'} {n : ℕ∞} {g : NN'} {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 : MM'} {s : Set M} {n : ℕ∞} {g : NN'} {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 : MM'} {n : ℕ∞} {g : NN'} (hf : ContMDiff I I' n f) (hg : ContMDiff J J' n g) :
ContMDiff (I.prod J) (I'.prod J') n (Prod.map f g)
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 : MM'} {s : Set M} {x : M} {g : NN'} {r : Set N} {y : N} (hf : SmoothWithinAt I I' f s x) (hg : SmoothWithinAt J J' g r y) :
SmoothWithinAt (I.prod J) (I'.prod J') (Prod.map f g) (s ×ˢ r) (x, y)
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 : MM'} {x : M} {g : NN'} {y : N} (hf : SmoothAt I I' f x) (hg : SmoothAt J J' g y) :
SmoothAt (I.prod J) (I'.prod J') (Prod.map f g) (x, y)
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 : MM'} {s : Set M} {g : NN'} {r : Set N} (hf : SmoothOn I I' f s) (hg : SmoothOn J J' g r) :
SmoothOn (I.prod J) (I'.prod J') (Prod.map f g) (s ×ˢ r)
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 : MM'} {g : NN'} (hf : Smooth I I' f) (hg : Smooth J J' g) :
Smooth (I.prod J) (I'.prod J') (Prod.map f g)

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_18} [Fintype ι] {Fi : ιType u_19} [(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_18} [Fintype ι] {Fi : ιType u_19} [(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_18} [Fintype ι] {Fi : ιType u_19} [(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_18} [Fintype ι] {Fi : ιType u_19} [(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
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} {ι : Type u_18} [Fintype ι] {Fi : ιType u_19} [(i : ι) → NormedAddCommGroup (Fi i)] [(i : ι) → NormedSpace 𝕜 (Fi i)] {φ : M(i : ι) → Fi i} :
SmoothWithinAt I (modelWithCornersSelf 𝕜 ((i : ι) → Fi i)) φ s x ∀ (i : ι), SmoothWithinAt I (modelWithCornersSelf 𝕜 (Fi i)) (fun (x : M) => φ x i) s x
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} {ι : Type u_18} [Fintype ι] {Fi : ιType u_19} [(i : ι) → NormedAddCommGroup (Fi i)] [(i : ι) → NormedSpace 𝕜 (Fi i)] {φ : M(i : ι) → Fi i} :
SmoothOn I (modelWithCornersSelf 𝕜 ((i : ι) → Fi i)) φ s ∀ (i : ι), SmoothOn I (modelWithCornersSelf 𝕜 (Fi i)) (fun (x : M) => φ x i) s
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} {ι : Type u_18} [Fintype ι] {Fi : ιType u_19} [(i : ι) → NormedAddCommGroup (Fi i)] [(i : ι) → NormedSpace 𝕜 (Fi i)] {φ : M(i : ι) → Fi i} :
SmoothAt I (modelWithCornersSelf 𝕜 ((i : ι) → Fi i)) φ x ∀ (i : ι), SmoothAt I (modelWithCornersSelf 𝕜 (Fi i)) (fun (x : M) => φ x i) x
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] {ι : Type u_18} [Fintype ι] {Fi : ιType u_19} [(i : ι) → NormedAddCommGroup (Fi i)] [(i : ι) → NormedSpace 𝕜 (Fi i)] {φ : M(i : ι) → Fi i} :
Smooth I (modelWithCornersSelf 𝕜 ((i : ι) → Fi i)) φ ∀ (i : ι), Smooth I (modelWithCornersSelf 𝕜 (Fi i)) fun (x : M) => φ x i