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.
@[deprecated ContMDiffWithinAt.prod_mk (since := "2024-11-20")]
theorem
SmoothWithinAt.prod_mk
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{s : Set M}
{x : M}
{n : 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.
Alias of ContMDiffWithinAt.prodMk.
@[deprecated ContMDiffWithinAt.prod_mk_space (since := "2024-11-20")]
theorem
SmoothWithinAt.prod_mk_space
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{s : Set M}
{x : M}
{n : 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.
Alias of ContMDiffWithinAt.prodMk_space.
@[deprecated ContMDiffAt.prod_mk (since := "2024-11-20")]
theorem
SmoothAt.prod_mk
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{x : M}
{n : 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.
Alias of ContMDiffAt.prodMk.
@[deprecated ContMDiffAt.prod_mk_space (since := "2024-11-20")]
theorem
SmoothAt.prod_mk_space
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{x : M}
{n : 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.
Alias of ContMDiffAt.prodMk_space.
@[deprecated ContMDiffOn.prod_mk (since := "2024-11-20")]
theorem
SmoothOn.prod_mk
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{s : Set M}
{n : 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.
Alias of ContMDiffOn.prodMk.
@[deprecated ContMDiffOn.prod_mk_space (since := "2024-11-20")]
theorem
SmoothOn.prod_mk_space
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{s : Set M}
{n : 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.
Alias of ContMDiffOn.prodMk_space.
@[deprecated ContMDiff.prod_mk (since := "2024-11-20")]
theorem
Smooth.prod_mk
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{n : WithTop ℕ∞}
{f : M → M'}
{g : M → N'}
(hf : ContMDiff I I' n f)
(hg : ContMDiff I J' n g)
:
Alias of ContMDiff.prodMk.
Alias of ContMDiff.prodMk.
@[deprecated ContMDiff.prod_mk_space (since := "2024-11-20")]
theorem
Smooth.prod_mk_space
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{n : 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.
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 ℕ∞}
:
@[deprecated contMDiffWithinAt_fst (since := "2024-11-20")]
theorem
smoothWithinAt_fst
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{s : Set (M × N)}
{p : M × N}
:
ContMDiffWithinAt (I.prod J) I n Prod.fst s p
Alias of contMDiffWithinAt_fst.
@[deprecated contMDiffAt_fst (since := "2024-11-20")]
theorem
smoothAt_fst
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{p : M × N}
:
ContMDiffAt (I.prod J) I n Prod.fst p
Alias of contMDiffAt_fst.
@[deprecated contMDiffOn_fst (since := "2024-11-20")]
theorem
smoothOn_fst
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{s : Set (M × N)}
:
ContMDiffOn (I.prod J) I n Prod.fst s
Alias of contMDiffOn_fst.
@[deprecated contMDiff_fst (since := "2024-11-20")]
theorem
smooth_fst
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
:
Alias of contMDiff_fst.
theorem
ContMDiffAt.fst
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : 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
@[deprecated ContMDiffAt.fst (since := "2024-11-20")]
theorem
SmoothAt.fst
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : 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
Alias of ContMDiffAt.fst.
@[deprecated ContMDiff.fst (since := "2024-11-20")]
theorem
Smooth.fst
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : N → M × M'}
(hf : ContMDiff J (I.prod I') n f)
:
ContMDiff J I n fun (x : N) => (f x).1
Alias of ContMDiff.fst.
theorem
contMDiffWithinAt_snd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : 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 ℕ∞}
:
@[deprecated contMDiffWithinAt_snd (since := "2024-11-20")]
theorem
smoothWithinAt_snd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{s : Set (M × N)}
{p : M × N}
:
ContMDiffWithinAt (I.prod J) J n Prod.snd s p
Alias of contMDiffWithinAt_snd.
@[deprecated contMDiffAt_snd (since := "2024-11-20")]
theorem
smoothAt_snd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{p : M × N}
:
ContMDiffAt (I.prod J) J n Prod.snd p
Alias of contMDiffAt_snd.
@[deprecated contMDiffOn_snd (since := "2024-11-20")]
theorem
smoothOn_snd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{s : Set (M × N)}
:
ContMDiffOn (I.prod J) J n Prod.snd s
Alias of contMDiffOn_snd.
@[deprecated contMDiff_snd (since := "2024-11-20")]
theorem
smooth_snd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
:
Alias of contMDiff_snd.
theorem
ContMDiffAt.snd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : 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
@[deprecated ContMDiffAt.snd (since := "2024-11-20")]
theorem
SmoothAt.snd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : 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
Alias of ContMDiffAt.snd.
@[deprecated ContMDiff.snd (since := "2024-11-20")]
theorem
Smooth.snd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : N → M × M'}
(hf : ContMDiff J (I.prod I') n f)
:
ContMDiff J I' n fun (x : N) => (f x).2
Alias of ContMDiff.snd.
theorem
contMDiffWithinAt_prod_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{s : Set M}
{x : M}
{n : 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 ℕ∞}
:
@[deprecated contMDiffAt_prod_iff (since := "2024-11-20")]
theorem
smoothAt_prod_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{x : M}
{n : 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
Alias of contMDiffAt_prod_iff.
@[deprecated contMDiff_prod_iff (since := "2024-11-20")]
theorem
smooth_prod_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{n : WithTop ℕ∞}
(f : M → M' × N')
:
Alias of contMDiff_prod_iff.
@[deprecated contMDiff_prod_assoc (since := "2024-11-20")]
theorem
smooth_prod_assoc
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
:
Alias of contMDiff_prod_assoc.
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.
@[deprecated ContMDiffWithinAt.prod_map (since := "2024-11-20")]
theorem
SmoothWithinAt.prod_map
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{f : M → M'}
{s : Set M}
{x : M}
{n : 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.
Alias of ContMDiffWithinAt.prodMap.
@[deprecated ContMDiffAt.prod_map (since := "2024-11-20")]
theorem
SmoothAt.prod_map
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{f : M → M'}
{x : M}
{n : WithTop ℕ∞}
{g : N → N'}
{y : N}
(hf : ContMDiffAt I I' n f x)
(hg : ContMDiffAt J J' n g y)
:
Alias of ContMDiffAt.prodMap.
Alias of ContMDiffAt.prodMap.
@[deprecated ContMDiffOn.prod_map (since := "2024-11-20")]
theorem
SmoothOn.prod_map
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{f : M → M'}
{s : Set M}
{n : 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.
Alias of ContMDiffOn.prodMap.
@[deprecated ContMDiff.prod_map (since := "2024-11-20")]
theorem
Smooth.prod_map
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_9}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace G N]
{F' : Type u_11}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{G' : Type u_12}
[TopologicalSpace G']
{J' : ModelWithCorners 𝕜 F' G'}
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{f : M → M'}
{n : WithTop ℕ∞}
{g : N → N'}
(hf : ContMDiff I I' n f)
(hg : ContMDiff J J' n g)
:
Alias of ContMDiff.prodMap.
Alias of ContMDiff.prodMap.
Regularity of functions with codomain Π i, F i #
We have no ModelWithCorners.pi yet, so we prove lemmas about functions f : M → Π i, F i and
use 𝓘(𝕜, Π i, F i) as the model space.
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
@[deprecated contMDiffWithinAt_pi_space (since := "2024-11-20")]
theorem
smoothWithinAt_pi_space
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{n : 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
Alias of contMDiffWithinAt_pi_space.
@[deprecated contMDiffAt_pi_space (since := "2024-11-20")]
theorem
smoothAt_pi_space
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{x : M}
{n : 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
Alias of contMDiffAt_pi_space.
@[deprecated contMDiffOn_pi_space (since := "2024-11-20")]
theorem
smoothOn_pi_space
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{n : 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
Alias of contMDiffOn_pi_space.
@[deprecated contMDiff_pi_space (since := "2024-11-20")]
theorem
smooth_pi_space
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{n : 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
Alias of contMDiff_pi_space.
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)
:
@[deprecated ContMDiff.sumElim (since := "2025-02-20")]
theorem
ContMDiff.sum_elim
{𝕜 : 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)
:
Alias of ContMDiff.sumElim.
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)
:
@[deprecated ContMDiff.sumMap (since := "2025-02-20")]
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'}
(hf : ContMDiff I J n f)
(hg : ContMDiff I J n g)
:
Alias of ContMDiff.sumMap.
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 ℕ∞}
: