Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
contMDiffAt_one_jet_eucl_bundle'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_5}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace G N]
{V : Type u_7}
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
{f : N → Bundle.TotalSpace (E →L[𝕜] V) fun (b : M) => TangentSpace I b →L[𝕜] Bundle.Trivial M V b}
{x₀ : N}
:
ContMDiffAt J (I.prod (modelWithCornersSelf 𝕜 (E →L[𝕜] V))) (↑⊤) f x₀ ↔ ContMDiffAt J I (↑⊤) (fun (x : N) => (f x).proj) x₀ ∧ ContMDiffAt J (modelWithCornersSelf 𝕜 (E →L[𝕜] V)) (↑⊤)
(fun (x : N) =>
have this :=
(f x).snd ∘SL Bundle.Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) (f x₀).proj) (f x).proj;
this)
x₀
theorem
contMDiffAt_one_jet_eucl_bundle
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_5}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace G N]
{V : Type u_7}
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
{f : N → Bundle.TotalSpace (E →L[𝕜] V) fun (b : M) => TangentSpace I b →L[𝕜] Bundle.Trivial M V b}
{x₀ : N}
:
ContMDiffAt J (I.prod (modelWithCornersSelf 𝕜 (E →L[𝕜] V))) (↑⊤) f x₀ ↔ ContMDiffAt J I (↑⊤) (fun (x : N) => (f x).proj) x₀ ∧ ContMDiffAt J (modelWithCornersSelf 𝕜 (E →L[𝕜] V)) (↑⊤)
(fun (x : N) =>
have this :=
(f x).snd ∘SL Bundle.Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) (f x₀).proj) (f x).proj;
this)
x₀
theorem
ContMDiffAt.one_jet_eucl_bundle_mk'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_5}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace G N]
{V : Type u_7}
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
{f : N → M}
{ϕ : N → E →L[𝕜] V}
{x₀ : N}
(hf : ContMDiffAt J I (↑⊤) f x₀)
(hϕ :
ContMDiffAt J (modelWithCornersSelf 𝕜 (E →L[𝕜] V)) (↑⊤)
(fun (x : N) =>
have this := ϕ x ∘SL Bundle.Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) (f x₀)) (f x);
this)
x₀)
:
ContMDiffAt J (I.prod (modelWithCornersSelf 𝕜 (E →L[𝕜] V))) (↑⊤) (fun (x : N) => ⟨f x, ϕ x⟩) x₀
theorem
ContMDiffAt.one_jet_eucl_bundle_mk
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_5}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace G N]
{V : Type u_7}
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
{f : N → M}
{ϕ : N → E →L[𝕜] V}
{x₀ : N}
(hf : ContMDiffAt J I (↑⊤) f x₀)
(hϕ :
ContMDiffAt J (modelWithCornersSelf 𝕜 (E →L[𝕜] V)) (↑⊤)
(fun (x : N) =>
have this := ϕ x ∘SL Bundle.Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) (f x₀)) (f x);
this)
x₀)
:
ContMDiffAt J (I.prod (modelWithCornersSelf 𝕜 (E →L[𝕜] V))) (↑⊤) (fun (x : N) => ⟨f x, ϕ x⟩) x₀
structure
OneJetEuclSec
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_2}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u_3)
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
(V : Type u_7)
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
:
Type (max (max u u_3) u_7)
A section of a 1-jet bundle seen as a bundle over the source manifold.
- toFun : M → Bundle.TotalSpace (E →L[𝕜] V) fun (b : M) => TangentSpace I b →L[𝕜] Bundle.Trivial M V b
Instances For
theorem
OneJetEuclSec.ext
{𝕜 : Type u_1}
{inst✝ : NontriviallyNormedField 𝕜}
{E : Type u}
{inst✝¹ : NormedAddCommGroup E}
{inst✝² : NormedSpace 𝕜 E}
{H : Type u_2}
{inst✝³ : TopologicalSpace H}
{I : ModelWithCorners 𝕜 E H}
{M : Type u_3}
{inst✝⁴ : TopologicalSpace M}
{inst✝⁵ : ChartedSpace H M}
{inst✝⁶ : IsManifold I (↑⊤) M}
{V : Type u_7}
{inst✝⁷ : NormedAddCommGroup V}
{inst✝⁸ : NormedSpace 𝕜 V}
{x y : OneJetEuclSec I M V}
(toFun : x.toFun = y.toFun)
:
theorem
OneJetEuclSec.ext_iff
{𝕜 : Type u_1}
{inst✝ : NontriviallyNormedField 𝕜}
{E : Type u}
{inst✝¹ : NormedAddCommGroup E}
{inst✝² : NormedSpace 𝕜 E}
{H : Type u_2}
{inst✝³ : TopologicalSpace H}
{I : ModelWithCorners 𝕜 E H}
{M : Type u_3}
{inst✝⁴ : TopologicalSpace M}
{inst✝⁵ : ChartedSpace H M}
{inst✝⁶ : IsManifold I (↑⊤) M}
{V : Type u_7}
{inst✝⁷ : NormedAddCommGroup V}
{inst✝⁸ : NormedSpace 𝕜 V}
{x y : OneJetEuclSec I M V}
:
@[implicit_reducible]
instance
instDFunLikeOneJetEuclSecTotalSpaceContinuousLinearMapIdTangentSpaceTrivial
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
{V : Type u_7}
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
:
DFunLike (OneJetEuclSec I M V) M fun (x : M) =>
Bundle.TotalSpace (E →L[𝕜] V) fun (b : M) => TangentSpace I b →L[𝕜] Bundle.Trivial M V b
Equations
- instDFunLikeOneJetEuclSecTotalSpaceContinuousLinearMapIdTangentSpaceTrivial = { coe := OneJetEuclSec.toFun, coe_injective := ⋯ }
@[simp]
theorem
OneJetEuclSec.is_sec
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
{V : Type u_7}
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
(s : OneJetEuclSec I M V)
(p : M)
:
@[simp]
theorem
OneJetEuclSec.contMDiff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
{V : Type u_7}
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
(s : OneJetEuclSec I M V)
:
@[implicit_reducible]
noncomputable instance
piBugInstanceRestatement
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_2}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u_3)
[TopologicalSpace M]
[ChartedSpace H M]
(V : Type u_7)
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
(x : M)
:
TopologicalSpace (TangentSpace I x →L[𝕜] Bundle.Trivial M V x)
Equations
- piBugInstanceRestatement I M V x = inferInstance
@[implicit_reducible]
instance
piBugInstanceRestatement2
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_2}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u_3)
[TopologicalSpace M]
[ChartedSpace H M]
(V : Type u_7)
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
(x : M × V)
:
TopologicalSpace (OneJetSpace I (modelWithCornersSelf 𝕜 V) x)
Equations
- piBugInstanceRestatement2 I M V x = inferInstance
def
proj
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_2}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u_3)
[TopologicalSpace M]
[ChartedSpace H M]
(V : Type u_7)
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
(v : OneJetBundle I M (modelWithCornersSelf 𝕜 V) V)
:
Bundle.TotalSpace (E →L[𝕜] V) fun (b : M) => TangentSpace I b →L[𝕜] Bundle.Trivial M V b
Instances For
theorem
contMDiff_proj
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_2}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u_3)
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
(V : Type u_7)
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
:
ContMDiff ((I.prod (modelWithCornersSelf 𝕜 V)).prod (modelWithCornersSelf 𝕜 (E →L[𝕜] V)))
(I.prod (modelWithCornersSelf 𝕜 (E →L[𝕜] V))) (↑⊤) (proj I M V)
def
drop
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
{V : Type u_7}
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
(s : OneJetSec I M (modelWithCornersSelf 𝕜 V) V)
:
OneJetEuclSec I M V
Instances For
def
incl
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_2}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u_3)
[TopologicalSpace M]
[ChartedSpace H M]
(V : Type u_7)
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
(v : (Bundle.TotalSpace (E →L[𝕜] V) fun (b : M) => TangentSpace I b →L[𝕜] Bundle.Trivial M V b) × V)
:
OneJetBundle I M (modelWithCornersSelf 𝕜 V) V
Instances For
theorem
contMDiff_incl
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_2}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u_3)
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
(V : Type u_7)
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
:
ContMDiff ((I.prod (modelWithCornersSelf 𝕜 (E →L[𝕜] V))).prod (modelWithCornersSelf 𝕜 V))
((I.prod (modelWithCornersSelf 𝕜 V)).prod (modelWithCornersSelf 𝕜 (E →L[𝕜] V))) (↑⊤) (incl I M V)
@[simp]
theorem
incl_fst_fst
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_2}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u_3)
[TopologicalSpace M]
[ChartedSpace H M]
(V : Type u_7)
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
(v : (Bundle.TotalSpace (E →L[𝕜] V) fun (b : M) => TangentSpace I b →L[𝕜] Bundle.Trivial M V b) × V)
:
@[simp]
theorem
incl_snd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_2}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u_3)
[TopologicalSpace M]
[ChartedSpace H M]
(V : Type u_7)
[NormedAddCommGroup V]
[NormedSpace 𝕜 V]
(v : (Bundle.TotalSpace (E →L[𝕜] V) fun (b : M) => TangentSpace I b →L[𝕜] Bundle.Trivial M V b) × V)
:
structure
FamilyOneJetEuclSec
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
(I : ModelWithCorners ℝ E H)
(M : Type u_3)
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
(V : Type u_4)
[NormedAddCommGroup V]
[NormedSpace ℝ V]
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{G : Type u_7}
[TopologicalSpace G]
(J : ModelWithCorners ℝ F G)
(N : Type u_8)
[TopologicalSpace N]
[ChartedSpace G N]
:
Type (max (max (max u_1 u_3) u_4) u_8)
A section of a 1-jet bundle seen as a bundle over the source manifold.
- toFun : N × M → Bundle.TotalSpace (E →L[ℝ] V) fun (b : M) => TangentSpace I b →L[ℝ] Bundle.Trivial M V b
Instances For
theorem
FamilyOneJetEuclSec.ext_iff
{E : Type u_1}
{inst✝ : NormedAddCommGroup E}
{inst✝¹ : NormedSpace ℝ E}
{H : Type u_2}
{inst✝² : TopologicalSpace H}
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
{inst✝³ : TopologicalSpace M}
{inst✝⁴ : ChartedSpace H M}
{inst✝⁵ : IsManifold I (↑⊤) M}
{V : Type u_4}
{inst✝⁶ : NormedAddCommGroup V}
{inst✝⁷ : NormedSpace ℝ V}
{F : Type u_6}
{inst✝⁸ : NormedAddCommGroup F}
{inst✝⁹ : NormedSpace ℝ F}
{G : Type u_7}
{inst✝¹⁰ : TopologicalSpace G}
{J : ModelWithCorners ℝ F G}
{N : Type u_8}
{inst✝¹¹ : TopologicalSpace N}
{inst✝¹² : ChartedSpace G N}
{x y : FamilyOneJetEuclSec I M V J N}
:
theorem
FamilyOneJetEuclSec.ext
{E : Type u_1}
{inst✝ : NormedAddCommGroup E}
{inst✝¹ : NormedSpace ℝ E}
{H : Type u_2}
{inst✝² : TopologicalSpace H}
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
{inst✝³ : TopologicalSpace M}
{inst✝⁴ : ChartedSpace H M}
{inst✝⁵ : IsManifold I (↑⊤) M}
{V : Type u_4}
{inst✝⁶ : NormedAddCommGroup V}
{inst✝⁷ : NormedSpace ℝ V}
{F : Type u_6}
{inst✝⁸ : NormedAddCommGroup F}
{inst✝⁹ : NormedSpace ℝ F}
{G : Type u_7}
{inst✝¹⁰ : TopologicalSpace G}
{J : ModelWithCorners ℝ F G}
{N : Type u_8}
{inst✝¹¹ : TopologicalSpace N}
{inst✝¹² : ChartedSpace G N}
{x y : FamilyOneJetEuclSec I M V J N}
(toFun : x.toFun = y.toFun)
:
@[implicit_reducible]
instance
instFunLikeFamilyOneJetEuclSecProdTotalSpaceContinuousLinearMapRealIdTangentSpaceTrivial
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
(I : ModelWithCorners ℝ E H)
(M : Type u_3)
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
(V : Type u_4)
[NormedAddCommGroup V]
[NormedSpace ℝ V]
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{G : Type u_7}
[TopologicalSpace G]
(J : ModelWithCorners ℝ F G)
(N : Type u_8)
[TopologicalSpace N]
[ChartedSpace G N]
:
FunLike (FamilyOneJetEuclSec I M V J N) (N × M)
(Bundle.TotalSpace (E →L[ℝ] V) fun (b : M) => TangentSpace I b →L[ℝ] Bundle.Trivial M V b)
Equations
- instFunLikeFamilyOneJetEuclSecProdTotalSpaceContinuousLinearMapRealIdTangentSpaceTrivial I M V J N = { coe := FamilyOneJetEuclSec.toFun, coe_injective := ⋯ }
@[simp]
theorem
FamilyOneJetEuclSec.is_sec
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
{V : Type u_4}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{G : Type u_7}
[TopologicalSpace G]
{J : ModelWithCorners ℝ F G}
{N : Type u_8}
[TopologicalSpace N]
[ChartedSpace G N]
(s : FamilyOneJetEuclSec I M V J N)
(p : N × M)
:
@[simp]
theorem
FamilyOneJetEuclSec.contMDiff
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
{V : Type u_4}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{G : Type u_7}
[TopologicalSpace G]
{J : ModelWithCorners ℝ F G}
{N : Type u_8}
[TopologicalSpace N]
[ChartedSpace G N]
(s : FamilyOneJetEuclSec I M V J N)
:
noncomputable def
familyJoin
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
{V : Type u_4}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{G : Type u_7}
[TopologicalSpace G]
{J : ModelWithCorners ℝ F G}
{N : Type u_8}
[TopologicalSpace N]
[ChartedSpace G N]
{f : N × M → V}
(hf : ContMDiff (J.prod I) (modelWithCornersSelf ℝ V) (↑⊤) f)
(s : FamilyOneJetEuclSec I M V J N)
:
FamilyOneJetSec I M (modelWithCornersSelf ℝ V) V J N
Equations
Instances For
noncomputable def
familyTwist
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
{V : Type u_4}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
{V' : Type u_5}
[NormedAddCommGroup V']
[NormedSpace ℝ V']
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{G : Type u_7}
[TopologicalSpace G]
{J : ModelWithCorners ℝ F G}
{N : Type u_8}
[TopologicalSpace N]
[ChartedSpace G N]
(s : OneJetEuclSec I M V)
(i : N × M → V →L[ℝ] V')
(hi : ∀ (x₀ : N × M), ContMDiffAt (J.prod I) (modelWithCornersSelf ℝ (V →L[ℝ] V')) (↑⊤) i x₀)
:
FamilyOneJetEuclSec I M V' J N