Fundamental definitions #
def
RelMfld.relativize
{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]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
{EP : Type u_7}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_8}
[TopologicalSpace HP]
(IP : ModelWithCorners ℝ EP HP)
(P : Type u_9)
[TopologicalSpace P]
[ChartedSpace HP P]
(R : RelMfld I M I' M')
:
The relation 𝓡 ^ P
Equations
- RelMfld.relativize IP P R = bundleSnd ⁻¹' R
Instances For
theorem
RelMfld.mem_relativize
{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]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
{EP : Type u_7}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_8}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_9}
[TopologicalSpace P]
[ChartedSpace HP P]
(R : RelMfld I M I' M')
(w : OneJetBundle (IP.prod I) (P × M) I' M')
:
w ∈ relativize IP P R ↔ OneJetBundle.mk w.proj.1.2 w.proj.2 (w.snd ∘SL ContinuousLinearMap.inr ℝ EP E) ∈ R
theorem
RelMfld.isOpen_relativize
{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]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{EP : Type u_7}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_8}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_9}
[TopologicalSpace P]
[ChartedSpace HP P]
[IsManifold IP (↑⊤) P]
(R : RelMfld I M I' M')
(h2 : IsOpen R)
:
IsOpen (relativize IP P R)
theorem
relativize_slice
{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]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
{EP : Type u_7}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_8}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_9}
[TopologicalSpace P]
[ChartedSpace HP P]
{R : RelMfld I M I' M'}
{σ : OneJetBundle (IP.prod I) (P × M) I' M'}
{p : DualPair (TangentSpace (IP.prod I) σ.proj.1)}
(q : DualPair (TangentSpace I σ.proj.1.2))
(hpq : p.π ∘SL ContinuousLinearMap.inr ℝ EP E = q.π)
:
theorem
relativize_slice_eq_univ
{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]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
{EP : Type u_7}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_8}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_9}
[TopologicalSpace P]
[ChartedSpace HP P]
{R : RelMfld I M I' M'}
{σ : OneJetBundle (IP.prod I) (P × M) I' M'}
{p : DualPair (TangentSpace (IP.prod I) σ.proj.1)}
(hp : p.π ∘SL ContinuousLinearMap.inr ℝ EP E = 0)
:
theorem
RelMfld.Ample.relativize
{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]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
{EP : Type u_7}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_8}
[TopologicalSpace HP]
(IP : ModelWithCorners ℝ EP HP)
(P : Type u_9)
[TopologicalSpace P]
[ChartedSpace HP P]
{R : RelMfld I M I' M'}
(hR : R.Ample)
:
(RelMfld.relativize IP P R).Ample
theorem
FamilyOneJetSec.uncurry_mem_relativize
{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]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{EP : Type u_7}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_8}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_9}
[TopologicalSpace P]
[ChartedSpace HP P]
[IsManifold IP (↑⊤) P]
{R : RelMfld I M I' M'}
(S : FamilyOneJetSec I M I' M' IP P)
{s : P}
{x : M}
:
noncomputable def
FamilyFormalSol.uncurry
{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]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{EP : Type u_7}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_8}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_9}
[TopologicalSpace P]
[ChartedSpace HP P]
[IsManifold IP (↑⊤) P]
{R : RelMfld I M I' M'}
(S : FamilyFormalSol IP P R)
:
FormalSol (RelMfld.relativize IP P R)
Instances For
theorem
FamilyFormalSol.uncurry_ϕ'
{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]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{EP : Type u_7}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_8}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_9}
[TopologicalSpace P]
[ChartedSpace HP P]
[IsManifold IP (↑⊤) P]
{R : RelMfld I M I' M'}
(S : FamilyFormalSol IP P R)
(p : P × M)
:
noncomputable def
FamilyOneJetSec.curry
{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]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{EP : Type u_7}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_8}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_9}
[TopologicalSpace P]
[ChartedSpace HP P]
[IsManifold IP (↑⊤) P]
{F : Type u_10}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{G : Type u_11}
[TopologicalSpace G]
{J : ModelWithCorners ℝ F G}
{N : Type u_12}
[TopologicalSpace N]
[ChartedSpace G N]
[IsManifold J (↑⊤) N]
(S : FamilyOneJetSec (IP.prod I) (P × M) I' M' J N)
:
FamilyOneJetSec I M I' M' (J.prod IP) (N × P)
Equations
Instances For
theorem
FamilyOneJetSec.curry_bs
{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]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{EP : Type u_7}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_8}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_9}
[TopologicalSpace P]
[ChartedSpace HP P]
[IsManifold IP (↑⊤) P]
{F : Type u_10}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{G : Type u_11}
[TopologicalSpace G]
{J : ModelWithCorners ℝ F G}
{N : Type u_12}
[TopologicalSpace N]
[ChartedSpace G N]
[IsManifold J (↑⊤) N]
(S : FamilyOneJetSec (IP.prod I) (P × M) I' M' J N)
(p : N × P)
(x : M)
:
theorem
FamilyOneJetSec.curry_ϕ
{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]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{EP : Type u_7}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_8}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_9}
[TopologicalSpace P]
[ChartedSpace HP P]
[IsManifold IP (↑⊤) P]
{F : Type u_10}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{G : Type u_11}
[TopologicalSpace G]
{J : ModelWithCorners ℝ F G}
{N : Type u_12}
[TopologicalSpace N]
[ChartedSpace G N]
[IsManifold J (↑⊤) N]
(S : FamilyOneJetSec (IP.prod I) (P × M) I' M' J N)
(p : N × P)
(x : M)
:
theorem
FamilyOneJetSec.curry_ϕ'
{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]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{EP : Type u_7}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_8}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_9}
[TopologicalSpace P]
[ChartedSpace HP P]
[IsManifold IP (↑⊤) P]
{F : Type u_10}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{G : Type u_11}
[TopologicalSpace G]
{J : ModelWithCorners ℝ F G}
{N : Type u_12}
[TopologicalSpace N]
[ChartedSpace G N]
[IsManifold J (↑⊤) N]
(S : FamilyOneJetSec (IP.prod I) (P × M) I' M' J N)
(p : N × P)
(x : M)
:
theorem
FormalSol.eq_iff
{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]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{R : RelMfld I M I' M'}
{F₁ F₂ : FormalSol R}
{x : M}
:
theorem
FamilyOneJetSec.isHolonomicAt_curry
{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]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{EP : Type u_7}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_8}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_9}
[TopologicalSpace P]
[ChartedSpace HP P]
[IsManifold IP (↑⊤) P]
{F : Type u_10}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{G : Type u_11}
[TopologicalSpace G]
{J : ModelWithCorners ℝ F G}
{N : Type u_12}
[TopologicalSpace N]
[ChartedSpace G N]
[IsManifold J (↑⊤) N]
(S : FamilyOneJetSec (IP.prod I) (P × M) I' M' J N)
{t : N}
{s : P}
{x : M}
(hS : (S t).IsHolonomicAt (s, x))
:
(S.curry (t, s)).IsHolonomicAt x
theorem
FamilyOneJetSec.curry_mem
{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]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{EP : Type u_7}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_8}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_9}
[TopologicalSpace P]
[ChartedSpace HP P]
[IsManifold IP (↑⊤) P]
{F : Type u_10}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{G : Type u_11}
[TopologicalSpace G]
{J : ModelWithCorners ℝ F G}
{N : Type u_12}
[TopologicalSpace N]
[ChartedSpace G N]
[IsManifold J (↑⊤) N]
{R : RelMfld I M I' M'}
(S : FamilyOneJetSec (IP.prod I) (P × M) I' M' J N)
{p : N × P}
{x : M}
(hR : (S p.1) (p.2, x) ∈ RelMfld.relativize IP P R)
:
noncomputable def
FamilyFormalSol.curry
{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]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{EP : Type u_7}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_8}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_9}
[TopologicalSpace P]
[ChartedSpace HP P]
[IsManifold IP (↑⊤) P]
{F : Type u_10}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{G : Type u_11}
[TopologicalSpace G]
{J : ModelWithCorners ℝ F G}
{N : Type u_12}
[TopologicalSpace N]
[ChartedSpace G N]
[IsManifold J (↑⊤) N]
{R : RelMfld I M I' M'}
(S : FamilyFormalSol J N (RelMfld.relativize IP P R))
:
FamilyFormalSol (J.prod IP) (N × P) R
Instances For
theorem
FamilyFormalSol.curry_ϕ'
{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]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{EP : Type u_7}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_8}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_9}
[TopologicalSpace P]
[ChartedSpace HP P]
[IsManifold IP (↑⊤) P]
{F : Type u_10}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{G : Type u_11}
[TopologicalSpace G]
{J : ModelWithCorners ℝ F G}
{N : Type u_12}
[TopologicalSpace N]
[ChartedSpace G N]
[IsManifold J (↑⊤) N]
{R : RelMfld I M I' M'}
(S : FamilyFormalSol J N (RelMfld.relativize IP P R))
(p : N × P)
(x : M)
:
theorem
curry_eq_iff_eq_uncurry
{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]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{EP : Type u_7}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_8}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_9}
[TopologicalSpace P]
[ChartedSpace HP P]
[IsManifold IP (↑⊤) P]
{F : Type u_10}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{G : Type u_11}
[TopologicalSpace G]
{J : ModelWithCorners ℝ F G}
{N : Type u_12}
[TopologicalSpace N]
[ChartedSpace G N]
[IsManifold J (↑⊤) N]
{R : RelMfld I M I' M'}
{𝓕 : FamilyFormalSol J N (RelMfld.relativize IP P R)}
{𝓕₀ : FamilyFormalSol IP P R}
{t : N}
{x : M}
{s : P}
(h : (𝓕 t) (s, x) = 𝓕₀.uncurry (s, x))
:
theorem
RelMfld.SatisfiesHPrinciple.satisfiesHPrincipleWith
{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]
{EP : Type u_7}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_8}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_9}
[TopologicalSpace P]
[ChartedSpace HP P]
[IsManifold IP (↑⊤) P]
{EX : Type u_13}
[NormedAddCommGroup EX]
[NormedSpace ℝ EX]
{HX : Type u_14}
[TopologicalSpace HX]
{IX : ModelWithCorners ℝ EX HX}
{X : Type u_15}
[MetricSpace X]
[ChartedSpace HX X]
[IsManifold IX (↑⊤) X]
(R : RelMfld I M IX X)
{C : Set (P × M)}
(ε : M → ℝ)
(h : (relativize IP P R).SatisfiesHPrinciple C fun (x : P × M) => ε x.2)
:
SatisfiesHPrincipleWith IP R C ε