Smoothness of standard maps associated to the product of manifolds #
This file contains results about smoothness of standard maps associated to products and sums (disjoint unions) of smooth manifolds:
- if
fandgareC^n, so is their point-wise product. - the component projections from a product of manifolds are smooth.
- functions into a product (pi type) are
C^niff their components are - if
MandNare manifolds modelled over the same space,Sum.inlandSum.inrareC^n, as areSum.elim,Sum.mapandSum.swap.
theorem
ContMDiffWithinAt.prodMk
{𝕜 : 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 : WithTop ℕ∞}
{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
@[deprecated ContMDiffWithinAt.prodMk (since := "2025-03-08")]
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 : WithTop ℕ∞}
{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.prodMk.
theorem
ContMDiffWithinAt.prodMk_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 : WithTop ℕ∞}
{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
@[deprecated ContMDiffWithinAt.prodMk_space (since := "2025-03-08")]
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 : WithTop ℕ∞}
{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.prodMk_space.
theorem
ContMDiffAt.prodMk
{𝕜 : 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 : WithTop ℕ∞}
{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
@[deprecated ContMDiffAt.prodMk (since := "2025-03-08")]
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 : WithTop ℕ∞}
{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.prodMk.
theorem
ContMDiffAt.prodMk_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 : WithTop ℕ∞}
{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
@[deprecated ContMDiffAt.prodMk_space (since := "2025-03-08")]
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 : WithTop ℕ∞}
{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.prodMk_space.
theorem
ContMDiffOn.prodMk
{𝕜 : 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 : WithTop ℕ∞}
{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
@[deprecated ContMDiffOn.prodMk (since := "2025-03-08")]
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 : WithTop ℕ∞}
{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.prodMk.
theorem
ContMDiffOn.prodMk_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 : WithTop ℕ∞}
{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
@[deprecated ContMDiffOn.prodMk_space (since := "2025-03-08")]
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 : WithTop ℕ∞}
{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.prodMk_space.
theorem
ContMDiff.prodMk
{𝕜 : 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 : WithTop ℕ∞}
{f : M → M'}
{g : M → N'}
(hf : ContMDiff I I' n f)
(hg : ContMDiff I J' n g)
:
@[deprecated ContMDiff.prodMk (since := "2025-03-08")]
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 : WithTop ℕ∞}
{f : M → M'}
{g : M → N'}
(hf : ContMDiff I I' n f)
(hg : ContMDiff I J' n g)
:
Alias of ContMDiff.prodMk.
theorem
ContMDiff.prodMk_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 : WithTop ℕ∞}
{f : M → E'}
{g : M → F'}
(hf : ContMDiff I (modelWithCornersSelf 𝕜 E') n f)
(hg : ContMDiff I (modelWithCornersSelf 𝕜 F') n g)
:
@[deprecated ContMDiff.prodMk_space (since := "2025-03-08")]
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 : WithTop ℕ∞}
{f : M → E'}
{g : M → F'}
(hf : ContMDiff I (modelWithCornersSelf 𝕜 E') n f)
(hg : ContMDiff I (modelWithCornersSelf 𝕜 F') n g)
:
Alias of ContMDiff.prodMk_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 : WithTop ℕ∞}
{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 : WithTop ℕ∞}
{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 : WithTop ℕ∞}
{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 : WithTop ℕ∞}
{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 : WithTop ℕ∞}
:
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 : WithTop ℕ∞}
{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 : WithTop ℕ∞}
{f : N → M × M'}
(hf : ContMDiff J (I.prod I') n f)
:
ContMDiff J I n 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 : WithTop ℕ∞}
{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 : WithTop ℕ∞}
{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 : WithTop ℕ∞}
{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 : WithTop ℕ∞}
{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 : WithTop ℕ∞}
:
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 : WithTop ℕ∞}
{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 : WithTop ℕ∞}
{f : N → M × M'}
(hf : ContMDiff J (I.prod I') n f)
:
ContMDiff J I' n 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']
{s : Set M}
{x : M}
{n : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(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 : WithTop ℕ∞}
:
theorem
ContMDiffWithinAt.comp₂
{𝕜 : 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']
{s : Set M}
{n : WithTop ℕ∞}
{h : M' × N' → N}
{f : M → M'}
{g : M → N'}
{x : M}
{t : Set (M' × N')}
(ha : ContMDiffWithinAt (I'.prod J') J n h t (f x, g x))
(fa : ContMDiffWithinAt I I' n f s x)
(ga : ContMDiffWithinAt I J' n g s x)
(st : Set.MapsTo (fun (x : M) => (f x, g x)) s t)
:
ContMDiffWithinAt I J n (fun (x : M) => h (f x, g x)) s x
ContMDiffWithinAt.comp for a function of two arguments.
theorem
ContMDiffWithinAt.comp₂_of_eq
{𝕜 : 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']
{s : Set M}
{n : WithTop ℕ∞}
{h : M' × N' → N}
{f : M → M'}
{g : M → N'}
{x : M}
{y : M' × N'}
{t : Set (M' × N')}
(ha : ContMDiffWithinAt (I'.prod J') J n h t y)
(fa : ContMDiffWithinAt I I' n f s x)
(ga : ContMDiffWithinAt I J' n g s x)
(e : (f x, g x) = y)
(st : Set.MapsTo (fun (x : M) => (f x, g x)) s t)
:
ContMDiffWithinAt I J n (fun (x : M) => h (f x, g x)) s x
ContMDiffWithinAt.comp₂, with a separate argument for point equality.
theorem
ContMDiffAt.comp₂
{𝕜 : 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']
{n : WithTop ℕ∞}
{h : M' × N' → N}
{f : M → M'}
{g : M → N'}
{x : M}
(ha : ContMDiffAt (I'.prod J') J n h (f x, g x))
(fa : ContMDiffAt I I' n f x)
(ga : ContMDiffAt I J' n g x)
:
ContMDiffAt I J n (fun (x : M) => h (f x, g x)) x
ContMDiffAt.comp for a function of two arguments.
theorem
ContMDiffAt.comp₂_of_eq
{𝕜 : 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']
{n : WithTop ℕ∞}
{h : M' × N' → N}
{f : M → M'}
{g : M → N'}
{x : M}
{y : M' × N'}
(ha : ContMDiffAt (I'.prod J') J n h y)
(fa : ContMDiffAt I I' n f x)
(ga : ContMDiffAt I J' n g x)
(e : (f x, g x) = y)
:
ContMDiffAt I J n (fun (x : M) => h (f x, g x)) x
ContMDiffAt.comp₂, with a separate argument for point equality.
theorem
ContMDiffWithinAt.curry_left
{𝕜 : 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 : WithTop ℕ∞}
{f : M → M' → N}
{x : M}
{y : M'}
{s : Set (M × M')}
(fa : ContMDiffWithinAt (I.prod I') J n (Function.uncurry f) s (x, y))
:
Curried C^n functions are C^n in the first coordinate.
theorem
ContMDiffWithinAt.along_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 : WithTop ℕ∞}
{f : M → M' → N}
{x : M}
{y : M'}
{s : Set (M × M')}
(fa : ContMDiffWithinAt (I.prod I') J n (Function.uncurry f) s (x, y))
:
Alias of ContMDiffWithinAt.curry_left.
Curried C^n functions are C^n in the first coordinate.
theorem
ContMDiffWithinAt.curry_right
{𝕜 : 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 : WithTop ℕ∞}
{f : M → M' → N}
{x : M}
{y : M'}
{s : Set (M × M')}
(fa : ContMDiffWithinAt (I.prod I') J n (Function.uncurry f) s (x, y))
:
Curried C^n functions are C^n in the second coordinate.
theorem
ContMDiffWithinAt.along_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 : WithTop ℕ∞}
{f : M → M' → N}
{x : M}
{y : M'}
{s : Set (M × M')}
(fa : ContMDiffWithinAt (I.prod I') J n (Function.uncurry f) s (x, y))
:
Alias of ContMDiffWithinAt.curry_right.
Curried C^n functions are C^n in the second coordinate.
theorem
ContMDiffAt.curry_left
{𝕜 : 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 : WithTop ℕ∞}
{f : M → M' → N}
{x : M}
{y : M'}
(fa : ContMDiffAt (I.prod I') J n (Function.uncurry f) (x, y))
:
ContMDiffAt I J n (fun (x : M) => f x y) x
Curried C^n functions are C^n in the first coordinate.
theorem
ContMDiffAt.along_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 : WithTop ℕ∞}
{f : M → M' → N}
{x : M}
{y : M'}
(fa : ContMDiffAt (I.prod I') J n (Function.uncurry f) (x, y))
:
ContMDiffAt I J n (fun (x : M) => f x y) x
Alias of ContMDiffAt.curry_left.
Curried C^n functions are C^n in the first coordinate.
theorem
ContMDiffAt.curry_right
{𝕜 : 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 : WithTop ℕ∞}
{f : M → M' → N}
{x : M}
{y : M'}
(fa : ContMDiffAt (I.prod I') J n (Function.uncurry f) (x, y))
:
ContMDiffAt I' J n (fun (y : M') => f x y) y
Curried C^n functions are C^n in the second coordinate.
theorem
ContMDiffAt.along_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 : WithTop ℕ∞}
{f : M → M' → N}
{x : M}
{y : M'}
(fa : ContMDiffAt (I.prod I') J n (Function.uncurry f) (x, y))
:
ContMDiffAt I' J n (fun (y : M') => f x y) y
Alias of ContMDiffAt.curry_right.
Curried C^n functions are C^n in the second coordinate.
theorem
ContMDiffOn.curry_left
{𝕜 : 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 : WithTop ℕ∞}
{f : M → M' → N}
{s : Set (M × M')}
(fa : ContMDiffOn (I.prod I') J n (Function.uncurry f) s)
{y : M'}
:
Curried C^n functions are C^n in the first coordinate.
theorem
ContMDiffOn.along_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 : WithTop ℕ∞}
{f : M → M' → N}
{s : Set (M × M')}
(fa : ContMDiffOn (I.prod I') J n (Function.uncurry f) s)
{y : M'}
:
Alias of ContMDiffOn.curry_left.
Curried C^n functions are C^n in the first coordinate.
theorem
ContMDiffOn.curry_right
{𝕜 : 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 : WithTop ℕ∞}
{f : M → M' → N}
{x : M}
{s : Set (M × M')}
(fa : ContMDiffOn (I.prod I') J n (Function.uncurry f) s)
:
Curried C^n functions are C^n in the second coordinate.
theorem
ContMDiffOn.along_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 : WithTop ℕ∞}
{f : M → M' → N}
{x : M}
{s : Set (M × M')}
(fa : ContMDiffOn (I.prod I') J n (Function.uncurry f) s)
:
Alias of ContMDiffOn.curry_right.
Curried C^n functions are C^n in the second coordinate.
theorem
ContMDiff.curry_left
{𝕜 : 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 : WithTop ℕ∞}
{f : M → M' → N}
(fa : ContMDiff (I.prod I') J n (Function.uncurry f))
{y : M'}
:
ContMDiff I J n fun (x : M) => f x y
Curried C^n functions are C^n in the first coordinate.
theorem
ContMDiff.along_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 : WithTop ℕ∞}
{f : M → M' → N}
(fa : ContMDiff (I.prod I') J n (Function.uncurry f))
{y : M'}
:
ContMDiff I J n fun (x : M) => f x y
Alias of ContMDiff.curry_left.
Curried C^n functions are C^n in the first coordinate.
theorem
ContMDiff.curry_right
{𝕜 : 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 : WithTop ℕ∞}
{f : M → M' → N}
{x : M}
(fa : ContMDiff (I.prod I') J n (Function.uncurry f))
:
ContMDiff I' J n fun (y : M') => f x y
Curried C^n functions are C^n in the second coordinate.
theorem
ContMDiff.along_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 : WithTop ℕ∞}
{f : M → M' → N}
{x : M}
(fa : ContMDiff (I.prod I') J n (Function.uncurry f))
:
ContMDiff I' J n fun (y : M') => f x y
Alias of ContMDiff.curry_right.
Curried C^n functions are C^n in the second coordinate.
theorem
ContMDiffWithinAt.prodMap'
{𝕜 : 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 : WithTop ℕ∞}
{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.
@[deprecated ContMDiffWithinAt.prodMap' (since := "2025-03-08")]
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 : WithTop ℕ∞}
{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
Alias of ContMDiffWithinAt.prodMap'.
The product map of two C^n functions within a set at a point is C^n
within the product set at the product point.
theorem
ContMDiffWithinAt.prodMap
{𝕜 : 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 : WithTop ℕ∞}
{g : N → N'}
{r : Set N}
{y : N}
(hf : ContMDiffWithinAt I I' n f s x)
(hg : ContMDiffWithinAt J J' n g r y)
:
@[deprecated ContMDiffWithinAt.prodMap (since := "2025-03-08")]
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 : WithTop ℕ∞}
{g : N → N'}
{r : Set N}
{y : N}
(hf : ContMDiffWithinAt I I' n f s x)
(hg : ContMDiffWithinAt J J' n g r y)
:
Alias of ContMDiffWithinAt.prodMap.
theorem
ContMDiffAt.prodMap
{𝕜 : 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 : WithTop ℕ∞}
{g : N → N'}
{y : N}
(hf : ContMDiffAt I I' n f x)
(hg : ContMDiffAt J J' n g y)
:
@[deprecated ContMDiffAt.prodMap (since := "2025-03-08")]
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 : WithTop ℕ∞}
{g : N → N'}
{y : N}
(hf : ContMDiffAt I I' n f x)
(hg : ContMDiffAt J J' n g y)
:
Alias of ContMDiffAt.prodMap.
theorem
ContMDiffAt.prodMap'
{𝕜 : 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 : WithTop ℕ∞}
{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
@[deprecated ContMDiffAt.prodMap' (since := "2025-03-08")]
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 : WithTop ℕ∞}
{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
Alias of ContMDiffAt.prodMap'.
theorem
ContMDiffOn.prodMap
{𝕜 : 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 : WithTop ℕ∞}
{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)
@[deprecated ContMDiffOn.prodMap (since := "2025-03-08")]
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 : WithTop ℕ∞}
{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.prodMap.
theorem
ContMDiff.prodMap
{𝕜 : 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 : WithTop ℕ∞}
{g : N → N'}
(hf : ContMDiff I I' n f)
(hg : ContMDiff J J' n g)
:
@[deprecated ContMDiff.prodMap (since := "2025-03-08")]
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 : WithTop ℕ∞}
{g : N → N'}
(hf : ContMDiff I I' n f)
(hg : ContMDiff J J' n g)
:
Alias of ContMDiff.prodMap.
Regularity of functions with codomain Π i, F i #
We have no ModelWithCorners.pi yet, so we prove lemmas about functions f : M → Π i, F i and
use 𝓘(𝕜, Π i, F i) as the model space.
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 : WithTop ℕ∞}
{ι : 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 : WithTop ℕ∞}
{ι : 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 : WithTop ℕ∞}
{ι : 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 : WithTop ℕ∞}
{ι : 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
theorem
ContMDiff.inl
{𝕜 : 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]
{M' : Type u_16}
[TopologicalSpace M']
[ChartedSpace H M']
{n : WithTop ℕ∞}
:
theorem
ContMDiff.inr
{𝕜 : 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]
{M' : Type u_16}
[TopologicalSpace M']
[ChartedSpace H M']
{n : WithTop ℕ∞}
:
theorem
extChartAt_inl_apply
{𝕜 : 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]
{M' : Type u_16}
[TopologicalSpace M']
[ChartedSpace H M']
{x y : M}
:
theorem
extChartAt_inr_apply
{𝕜 : 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]
{M' : Type u_16}
[TopologicalSpace M']
[ChartedSpace H M']
{x y : M'}
:
theorem
ContMDiff.sumElim
{𝕜 : 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]
{M' : Type u_16}
[TopologicalSpace M']
[ChartedSpace H M']
{n : WithTop ℕ∞}
{E' : Type u_17}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_18}
[TopologicalSpace H']
{J : ModelWithCorners 𝕜 E' H'}
{N : Type u_20}
[TopologicalSpace N]
[ChartedSpace H' N]
{f : M → N}
{g : M' → N}
(hf : ContMDiff I J n f)
(hg : ContMDiff I J n g)
:
theorem
ContMDiff.sumMap
{𝕜 : 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]
{M' : Type u_16}
[TopologicalSpace M']
[ChartedSpace H M']
{n : WithTop ℕ∞}
{E' : Type u_17}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_18}
[TopologicalSpace H']
{J : ModelWithCorners 𝕜 E' H'}
{N : Type u_20}
{N' : Type u_21}
[TopologicalSpace N]
[TopologicalSpace N']
[ChartedSpace H' N]
[ChartedSpace H' N']
{f : M → N}
{g : M' → N'}
(hf : ContMDiff I J n f)
(hg : ContMDiff I J n g)
:
theorem
contMDiff_of_contMDiff_inl
{𝕜 : 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 : WithTop ℕ∞}
{E' : Type u_17}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_18}
[TopologicalSpace H']
{J : ModelWithCorners 𝕜 E' H'}
{N : Type u_20}
{N' : Type u_21}
[TopologicalSpace N]
[TopologicalSpace N']
[ChartedSpace H' N]
[ChartedSpace H' N']
{f : M → N}
(h : ContMDiff I J n (Sum.inl ∘ f))
:
ContMDiff I J n f
theorem
contMDiff_of_contMDiff_inr
{𝕜 : 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_16}
[TopologicalSpace M']
[ChartedSpace H M']
{n : WithTop ℕ∞}
{E' : Type u_17}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_18}
[TopologicalSpace H']
{J : ModelWithCorners 𝕜 E' H'}
{N : Type u_20}
{N' : Type u_21}
[TopologicalSpace N]
[TopologicalSpace N']
[ChartedSpace H' N]
[ChartedSpace H' N']
{g : M' → N'}
(h : ContMDiff I J n (Sum.inr ∘ g))
:
ContMDiff I J n g
theorem
contMDiff_sum_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]
{M' : Type u_16}
[TopologicalSpace M']
[ChartedSpace H M']
{n : WithTop ℕ∞}
{E' : Type u_17}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_18}
[TopologicalSpace H']
{J : ModelWithCorners 𝕜 E' H'}
{N : Type u_20}
{N' : Type u_21}
[TopologicalSpace N]
[TopologicalSpace N']
[ChartedSpace H' N]
[ChartedSpace H' N']
{f : M → N}
{g : M' → N'}
:
theorem
ContMDiff.swap
{𝕜 : 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]
{M' : Type u_16}
[TopologicalSpace M']
[ChartedSpace H M']
{n : WithTop ℕ∞}
: