Gromov's theorem #
We prove the h-principle for open and ample first order differential relations.
theorem
RelMfld.Ample.satisfiesHPrinciple
{EM : Type u_1}
[NormedAddCommGroup EM]
[NormedSpace ℝ EM]
[FiniteDimensional ℝ EM]
{HM : Type u_2}
[TopologicalSpace HM]
{IM : ModelWithCorners ℝ EM HM}
[IM.Boundaryless]
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace HM M]
[IsManifold IM (↑⊤) M]
[T2Space M]
[SigmaCompactSpace M]
{EX : Type u_4}
[NormedAddCommGroup EX]
[NormedSpace ℝ EX]
[FiniteDimensional ℝ EX]
{HX : Type u_5}
[TopologicalSpace HX]
{IX : ModelWithCorners ℝ EX HX}
[IX.Boundaryless]
{X : Type u_6}
[MetricSpace X]
[ChartedSpace HX X]
[IsManifold IX (↑⊤) X]
[SigmaCompactSpace X]
{R : RelMfld IM M IX X}
{A : Set M}
{δ : M → ℝ}
(hRample : R.Ample)
(hRopen : IsOpen R)
(hA : IsClosed A)
(hδ_pos : ∀ (x : M), 0 < δ x)
(hδ_cont : Continuous δ)
:
R.SatisfiesHPrinciple A δ
theorem
RelMfld.Ample.satisfiesHPrincipleWith
{EM : Type u_1}
[NormedAddCommGroup EM]
[NormedSpace ℝ EM]
[FiniteDimensional ℝ EM]
{HM : Type u_2}
[TopologicalSpace HM]
{IM : ModelWithCorners ℝ EM HM}
[IM.Boundaryless]
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace HM M]
[IsManifold IM (↑⊤) M]
[T2Space M]
[SigmaCompactSpace M]
{EX : Type u_4}
[NormedAddCommGroup EX]
[NormedSpace ℝ EX]
[FiniteDimensional ℝ EX]
{HX : Type u_5}
[TopologicalSpace HX]
{IX : ModelWithCorners ℝ EX HX}
[IX.Boundaryless]
{X : Type u_6}
[MetricSpace X]
[ChartedSpace HX X]
[IsManifold IX (↑⊤) X]
[SigmaCompactSpace X]
{R : RelMfld IM M IX X}
{δ : M → ℝ}
{EP : Type u_7}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
[FiniteDimensional ℝ EP]
{HP : Type u_8}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
[IP.Boundaryless]
{P : Type u_9}
[TopologicalSpace P]
[ChartedSpace HP P]
[IsManifold IP (↑⊤) P]
[SigmaCompactSpace P]
[T2Space P]
{C : Set (P × M)}
(hRample : R.Ample)
(hRopen : IsOpen R)
(hC : IsClosed C)
(hδ_pos : ∀ (x : M), 0 < δ x)
(hδ_cont : Continuous δ)
:
SatisfiesHPrincipleWith IP R C δ
Gromov's Theorem
theorem
RelMfld.Ample.satisfiesHPrincipleWith'
{EM : Type u_1}
[NormedAddCommGroup EM]
[NormedSpace ℝ EM]
[FiniteDimensional ℝ EM]
{HM : Type u_2}
[TopologicalSpace HM]
{IM : ModelWithCorners ℝ EM HM}
[IM.Boundaryless]
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace HM M]
[IsManifold IM (↑⊤) M]
[T2Space M]
[SigmaCompactSpace M]
{δ : M → ℝ}
{EP : Type u_7}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
[FiniteDimensional ℝ EP]
{HP : Type u_8}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
[IP.Boundaryless]
{P : Type u_9}
[TopologicalSpace P]
[ChartedSpace HP P]
[IsManifold IP (↑⊤) P]
[SigmaCompactSpace P]
[T2Space P]
{C : Set (P × M)}
{E' : Type u_10}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[FiniteDimensional ℝ E']
{H' : Type u_11}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[I'.Boundaryless]
{M' : Type u_12}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
[SigmaCompactSpace M']
[T2Space M']
{R : RelMfld IM M I' M'}
(hRample : R.Ample)
(hRopen : IsOpen R)
(hC : IsClosed C)
(hδ_pos : ∀ (x : M), 0 < δ x)
(hδ_cont : Continuous δ)
:
SatisfiesHPrincipleWith IP R C δ
Gromov's Theorem without metric space assumption