structure
OpenSmoothEmbedding
{𝕜 : 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']
:
Type (max u_4 u_7)
- toFun : M → M'
- invFun : M' → M
- contMDiffOn_inv : ContMDiffOn I' I (↑⊤) self.invFun (Set.range ↑self)
Instances For
instance
instCoeFunOpenSmoothEmbeddingForall
{𝕜 : 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']
:
CoeFun (OpenSmoothEmbedding I M I' M') fun (x : OpenSmoothEmbedding I M I' M') => M → M'
Equations
- instCoeFunOpenSmoothEmbeddingForall I M I' M' = { coe := OpenSmoothEmbedding.toFun }
@[simp]
theorem
OpenSmoothEmbedding.coe_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 : M → M')
(g : M' → M)
(h₁ : ∀ {x : M}, g (f x) = x)
(h₂ : IsOpen (Set.range f))
(h₃ : ContMDiff I I' (↑⊤) f)
(h₄ : ContMDiffOn I' I (↑⊤) g (Set.range f))
:
↑{ toFun := f, invFun := g, left_inv' := h₁, isOpen_range := h₂, contMDiff_to := h₃, contMDiffOn_inv := h₄ } = f
@[simp]
theorem
OpenSmoothEmbedding.left_inv
{𝕜 : 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 : OpenSmoothEmbedding I M I' M')
(x : M)
:
@[simp]
theorem
OpenSmoothEmbedding.invFun_comp_coe
{𝕜 : 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 : OpenSmoothEmbedding I M I' M')
:
@[simp]
theorem
OpenSmoothEmbedding.right_inv
{𝕜 : 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 : OpenSmoothEmbedding I M I' M')
{y : M'}
(hy : y ∈ Set.range ↑f)
:
theorem
OpenSmoothEmbedding.contMDiffAt_inv
{𝕜 : 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 : OpenSmoothEmbedding I M I' M')
{y : M'}
(hy : y ∈ Set.range ↑f)
:
ContMDiffAt I' I (↑⊤) f.invFun y
theorem
OpenSmoothEmbedding.contMDiffAt_inv'
{𝕜 : 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 : OpenSmoothEmbedding I M I' M')
{x : M}
:
ContMDiffAt I' I (↑⊤) f.invFun (↑f x)
theorem
OpenSmoothEmbedding.leftInverse
{𝕜 : 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 : OpenSmoothEmbedding I M I' M')
:
theorem
OpenSmoothEmbedding.injective
{𝕜 : 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 : OpenSmoothEmbedding I M I' M')
:
theorem
OpenSmoothEmbedding.continuous
{𝕜 : 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 : OpenSmoothEmbedding I M I' M')
:
Continuous ↑f
theorem
OpenSmoothEmbedding.isOpenMap
{𝕜 : 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 : OpenSmoothEmbedding I M I' M')
:
IsOpenMap ↑f
theorem
OpenSmoothEmbedding.coe_comp_invFun_eventuallyEq
{𝕜 : 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 : OpenSmoothEmbedding I M I' M')
(x : M)
:
def
OpenSmoothEmbedding.fderiv
{𝕜 : 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 : OpenSmoothEmbedding I M I' M')
(x : M)
:
Equations
Instances For
@[simp]
theorem
OpenSmoothEmbedding.fderiv_coe
{𝕜 : 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 : OpenSmoothEmbedding I M I' M')
(x : M)
:
@[simp]
theorem
OpenSmoothEmbedding.fderiv_symm_coe
{𝕜 : 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 : OpenSmoothEmbedding I M I' M')
(x : M)
:
theorem
OpenSmoothEmbedding.fderiv_symm_coe'
{𝕜 : 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 : OpenSmoothEmbedding I M I' M')
{x : M'}
(hx : x ∈ Set.range ↑f)
:
theorem
OpenSmoothEmbedding.isOpenEmbedding
{𝕜 : 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 : OpenSmoothEmbedding I M I' M')
:
theorem
OpenSmoothEmbedding.isInducing
{𝕜 : 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 : OpenSmoothEmbedding I M I' M')
:
theorem
OpenSmoothEmbedding.forall_near'
{𝕜 : 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 : OpenSmoothEmbedding I M I' M')
{P : M → Prop}
{A : Set M'}
(h : ∀ᶠ (m : M) in nhdsSet (↑f ⁻¹' A), P m)
:
theorem
OpenSmoothEmbedding.forall_near
{𝕜 : 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 : OpenSmoothEmbedding I M I' M')
[T2Space M']
{P : M → Prop}
{P' : M' → Prop}
{K : Set M}
(hK : IsCompact K)
{A : Set M'}
(hP : ∀ᶠ (m : M) in nhdsSet (↑f ⁻¹' A), P m)
(hP' : ∀ᶠ (m' : M') in nhdsSet A, m' ∉ ↑f '' K → P' m')
(hPP' : ∀ (m : M), P m → P' (↑f m))
:
def
OpenSmoothEmbedding.id
{𝕜 : 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]
:
OpenSmoothEmbedding I M I M
The identity map is a smooth open embedding.
Equations
- OpenSmoothEmbedding.id I M = { toFun := id, invFun := id, left_inv' := ⋯, isOpen_range := ⋯, contMDiff_to := ⋯, contMDiffOn_inv := ⋯ }
Instances For
@[simp]
theorem
OpenSmoothEmbedding.id_invFun
{𝕜 : 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]
(a : M)
:
@[simp]
theorem
OpenSmoothEmbedding.id_toFun
{𝕜 : 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]
(a : M)
:
def
ContinuousLinearEquiv.toOpenSmoothEmbedding
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(e : E ≃L[𝕜] E')
:
OpenSmoothEmbedding (modelWithCornersSelf 𝕜 E) E (modelWithCornersSelf 𝕜 E') E'
Equations
- e.toOpenSmoothEmbedding = { toFun := ⇑e, invFun := ⇑e.symm, left_inv' := ⋯, isOpen_range := ⋯, contMDiff_to := ⋯, contMDiffOn_inv := ⋯ }
Instances For
@[simp]
theorem
ContinuousLinearEquiv.toOpenSmoothEmbedding_invFun
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(e : E ≃L[𝕜] E')
(a : E')
:
@[simp]
theorem
ContinuousLinearEquiv.toOpenSmoothEmbedding_toFun
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(e : E ≃L[𝕜] E')
(a : E)
:
def
openSmoothEmbOfDiffeoSubsetChartTarget
{F : Type u_1}
{H : Type u_2}
(M : Type u)
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
(IF : ModelWithCorners ℝ F H)
[IsManifold IF (↑⊤) M]
(x : M)
{f : PartialHomeomorph F F}
(hf₁ : f.source = Set.univ)
(hf₂ : 𝒞 ↑⊤ ↑f)
(hf₃ : ContDiffOn ℝ (↑⊤) (↑f.symm) f.target)
(hf₄ : Set.range ↑f ⊆ ↑IF '' (chartAt H x).target)
:
OpenSmoothEmbedding (modelWithCornersSelf ℝ F) F IF M
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
coe_openSmoothEmbOfDiffeoSubsetChartTarget
{F : Type u_1}
{H : Type u_2}
(M : Type u)
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
(IF : ModelWithCorners ℝ F H)
[IsManifold IF (↑⊤) M]
(x : M)
{f : PartialHomeomorph F F}
(hf₁ : f.source = Set.univ)
(hf₂ : 𝒞 ↑⊤ ↑f)
(hf₃ : ContDiffOn ℝ (↑⊤) (↑f.symm) f.target)
(hf₄ : Set.range ↑f ⊆ ↑IF '' (chartAt H x).target)
:
theorem
range_openSmoothEmbOfDiffeoSubsetChartTarget
{F : Type u_1}
{H : Type u_2}
(M : Type u)
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
(IF : ModelWithCorners ℝ F H)
[IsManifold IF (↑⊤) M]
(x : M)
{f : PartialHomeomorph F F}
(hf₁ : f.source = Set.univ)
(hf₂ : 𝒞 ↑⊤ ↑f)
(hf₃ : ContDiffOn ℝ (↑⊤) (↑f.symm) f.target)
(hf₄ : Set.range ↑f ⊆ ↑IF '' (chartAt H x).target)
:
Set.range ↑(openSmoothEmbOfDiffeoSubsetChartTarget M IF x hf₁ hf₂ hf₃ hf₄) = ↑(extChartAt IF x).symm '' Set.range ↑f
theorem
nice_atlas'
(F : Type u_1)
{H : Type u_2}
{M : Type u}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
(IF : ModelWithCorners ℝ F H)
[IsManifold IF (↑⊤) M]
[IF.Boundaryless]
[FiniteDimensional ℝ F]
[T2Space M]
[LocallyCompactSpace M]
[SigmaCompactSpace M]
{ι : Type u_3}
{s : ι → Set M}
(s_op : ∀ (j : ι), IsOpen (s j))
(cov : ⋃ (j : ι), s j = Set.univ)
(U : Set F)
(hU₁ : 0 ∈ U)
(hU₂ : IsOpen U)
:
theorem
nice_atlas
(F : Type u_1)
{H : Type u_2}
{M : Type u}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
(IF : ModelWithCorners ℝ F H)
[IsManifold IF (↑⊤) M]
[IF.Boundaryless]
[FiniteDimensional ℝ F]
[T2Space M]
[LocallyCompactSpace M]
[SigmaCompactSpace M]
[Nonempty M]
{ι : Type u_3}
{s : ι → Set M}
(s_op : ∀ (j : ι), IsOpen (s j))
(cov : ⋃ (j : ι), s j = Set.univ)
:
∃ (n : ℕ) (φ : IndexType n → OpenSmoothEmbedding (modelWithCornersSelf ℝ F) F IF M),
(∀ (i : IndexType n), ∃ (j : ι), Set.range ↑(φ i) ⊆ s j) ∧ (LocallyFinite fun (i : IndexType n) => Set.range ↑(φ i)) ∧ ⋃ (i : IndexType n), ↑(φ i) '' Metric.ball 0 1 = Set.univ
def
OpenSmoothEmbedding.update
{𝕜 : Type u_1}
{EX : Type u_2}
{EM : Type u_3}
{EY : Type u_4}
{EN : Type u_5}
{X : Type u_7}
{M : Type u_8}
{Y : Type u_9}
{N : Type u_10}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup EX]
[NormedSpace 𝕜 EX]
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
[NormedAddCommGroup EY]
[NormedSpace 𝕜 EY]
[NormedAddCommGroup EN]
[NormedSpace 𝕜 EN]
{HX : Type u_12}
[TopologicalSpace HX]
{IX : ModelWithCorners 𝕜 EX HX}
{HY : Type u_13}
[TopologicalSpace HY]
{IY : ModelWithCorners 𝕜 EY HY}
{HM : Type u_14}
[TopologicalSpace HM]
{IM : ModelWithCorners 𝕜 EM HM}
{HN : Type u_16}
[TopologicalSpace HN]
{IN : ModelWithCorners 𝕜 EN HN}
[TopologicalSpace X]
[ChartedSpace HX X]
[TopologicalSpace M]
[ChartedSpace HM M]
[TopologicalSpace Y]
[ChartedSpace HY Y]
[TopologicalSpace N]
[ChartedSpace HN N]
(φ : OpenSmoothEmbedding IX X IM M)
(ψ : OpenSmoothEmbedding IY Y IN N)
(f : M → N)
(g : X → Y)
(m : M)
:
N
This is definition def:update in the blueprint.
Instances For
@[simp]
theorem
OpenSmoothEmbedding.update_of_nmem_range
{𝕜 : Type u_1}
{EX : Type u_2}
{EM : Type u_3}
{EY : Type u_4}
{EN : Type u_5}
{X : Type u_7}
{M : Type u_8}
{Y : Type u_9}
{N : Type u_10}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup EX]
[NormedSpace 𝕜 EX]
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
[NormedAddCommGroup EY]
[NormedSpace 𝕜 EY]
[NormedAddCommGroup EN]
[NormedSpace 𝕜 EN]
{HX : Type u_12}
[TopologicalSpace HX]
{IX : ModelWithCorners 𝕜 EX HX}
{HY : Type u_13}
[TopologicalSpace HY]
{IY : ModelWithCorners 𝕜 EY HY}
{HM : Type u_14}
[TopologicalSpace HM]
{IM : ModelWithCorners 𝕜 EM HM}
{HN : Type u_16}
[TopologicalSpace HN]
{IN : ModelWithCorners 𝕜 EN HN}
[TopologicalSpace X]
[ChartedSpace HX X]
[TopologicalSpace M]
[ChartedSpace HM M]
[TopologicalSpace Y]
[ChartedSpace HY Y]
[TopologicalSpace N]
[ChartedSpace HN N]
(φ : OpenSmoothEmbedding IX X IM M)
(ψ : OpenSmoothEmbedding IY Y IN N)
(f : M → N)
(g : X → Y)
{m : M}
(hm : m ∉ Set.range ↑φ)
:
@[simp]
theorem
OpenSmoothEmbedding.update_of_mem_range
{𝕜 : Type u_1}
{EX : Type u_2}
{EM : Type u_3}
{EY : Type u_4}
{EN : Type u_5}
{X : Type u_7}
{M : Type u_8}
{Y : Type u_9}
{N : Type u_10}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup EX]
[NormedSpace 𝕜 EX]
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
[NormedAddCommGroup EY]
[NormedSpace 𝕜 EY]
[NormedAddCommGroup EN]
[NormedSpace 𝕜 EN]
{HX : Type u_12}
[TopologicalSpace HX]
{IX : ModelWithCorners 𝕜 EX HX}
{HY : Type u_13}
[TopologicalSpace HY]
{IY : ModelWithCorners 𝕜 EY HY}
{HM : Type u_14}
[TopologicalSpace HM]
{IM : ModelWithCorners 𝕜 EM HM}
{HN : Type u_16}
[TopologicalSpace HN]
{IN : ModelWithCorners 𝕜 EN HN}
[TopologicalSpace X]
[ChartedSpace HX X]
[TopologicalSpace M]
[ChartedSpace HM M]
[TopologicalSpace Y]
[ChartedSpace HY Y]
[TopologicalSpace N]
[ChartedSpace HN N]
(φ : OpenSmoothEmbedding IX X IM M)
(ψ : OpenSmoothEmbedding IY Y IN N)
(f : M → N)
(g : X → Y)
{m : M}
(hm : m ∈ Set.range ↑φ)
:
theorem
OpenSmoothEmbedding.update_apply_embedding
{𝕜 : Type u_1}
{EX : Type u_2}
{EM : Type u_3}
{EY : Type u_4}
{EN : Type u_5}
{X : Type u_7}
{M : Type u_8}
{Y : Type u_9}
{N : Type u_10}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup EX]
[NormedSpace 𝕜 EX]
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
[NormedAddCommGroup EY]
[NormedSpace 𝕜 EY]
[NormedAddCommGroup EN]
[NormedSpace 𝕜 EN]
{HX : Type u_12}
[TopologicalSpace HX]
{IX : ModelWithCorners 𝕜 EX HX}
{HY : Type u_13}
[TopologicalSpace HY]
{IY : ModelWithCorners 𝕜 EY HY}
{HM : Type u_14}
[TopologicalSpace HM]
{IM : ModelWithCorners 𝕜 EM HM}
{HN : Type u_16}
[TopologicalSpace HN]
{IN : ModelWithCorners 𝕜 EN HN}
[TopologicalSpace X]
[ChartedSpace HX X]
[TopologicalSpace M]
[ChartedSpace HM M]
[TopologicalSpace Y]
[ChartedSpace HY Y]
[TopologicalSpace N]
[ChartedSpace HN N]
(φ : OpenSmoothEmbedding IX X IM M)
(ψ : OpenSmoothEmbedding IY Y IN N)
(f : M → N)
(g : X → Y)
(x : X)
:
theorem
OpenSmoothEmbedding.nice_update_of_eq_outside_compact_aux
{𝕜 : Type u_1}
{EX : Type u_2}
{EM : Type u_3}
{EY : Type u_4}
{EN : Type u_5}
{X : Type u_7}
{M : Type u_8}
{Y : Type u_9}
{N : Type u_10}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup EX]
[NormedSpace 𝕜 EX]
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
[NormedAddCommGroup EY]
[NormedSpace 𝕜 EY]
[NormedAddCommGroup EN]
[NormedSpace 𝕜 EN]
{HX : Type u_12}
[TopologicalSpace HX]
{IX : ModelWithCorners 𝕜 EX HX}
{HY : Type u_13}
[TopologicalSpace HY]
{IY : ModelWithCorners 𝕜 EY HY}
{HM : Type u_14}
[TopologicalSpace HM]
{IM : ModelWithCorners 𝕜 EM HM}
{HN : Type u_16}
[TopologicalSpace HN]
{IN : ModelWithCorners 𝕜 EN HN}
[TopologicalSpace X]
[ChartedSpace HX X]
[TopologicalSpace M]
[ChartedSpace HM M]
[TopologicalSpace Y]
[ChartedSpace HY Y]
[TopologicalSpace N]
[ChartedSpace HN N]
(φ : OpenSmoothEmbedding IX X IM M)
(ψ : OpenSmoothEmbedding IY Y IN N)
(f : M → N)
{K : Set X}
(g : X → Y)
(hg : ∀ x ∉ K, f (↑φ x) = ↑ψ (g x))
{m : M}
(hm : m ∉ ↑φ '' K)
:
theorem
OpenSmoothEmbedding.smooth_update
{𝕜 : Type u_1}
{EX : Type u_2}
{EM : Type u_3}
{EY : Type u_4}
{EN : Type u_5}
{EM' : Type u_6}
{X : Type u_7}
{M : Type u_8}
{Y : Type u_9}
{N : Type u_10}
{M' : Type u_11}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup EX]
[NormedSpace 𝕜 EX]
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
[NormedAddCommGroup EM']
[NormedSpace 𝕜 EM']
[NormedAddCommGroup EY]
[NormedSpace 𝕜 EY]
[NormedAddCommGroup EN]
[NormedSpace 𝕜 EN]
{HX : Type u_12}
[TopologicalSpace HX]
{IX : ModelWithCorners 𝕜 EX HX}
{HY : Type u_13}
[TopologicalSpace HY]
{IY : ModelWithCorners 𝕜 EY HY}
{HM : Type u_14}
[TopologicalSpace HM]
{IM : ModelWithCorners 𝕜 EM HM}
{HM' : Type u_15}
[TopologicalSpace HM']
{IM' : ModelWithCorners 𝕜 EM' HM'}
{HN : Type u_16}
[TopologicalSpace HN]
{IN : ModelWithCorners 𝕜 EN HN}
[TopologicalSpace X]
[ChartedSpace HX X]
[TopologicalSpace M]
[ChartedSpace HM M]
[TopologicalSpace M']
[ChartedSpace HM' M']
[TopologicalSpace Y]
[ChartedSpace HY Y]
[TopologicalSpace N]
[ChartedSpace HN N]
(φ : OpenSmoothEmbedding IX X IM M)
(ψ : OpenSmoothEmbedding IY Y IN N)
(f : M' → M → N)
(g : M' → X → Y)
{k : M' → M}
{K : Set X}
(hK : IsClosed (↑φ '' K))
(hf : ContMDiff (IM'.prod IM) IN (↑⊤) (Function.uncurry f))
(hg : ContMDiff (IM'.prod IX) IY (↑⊤) (Function.uncurry g))
(hk : ContMDiff IM' IM (↑⊤) k)
(hg' : ∀ (y : M'), ∀ x ∉ K, f y (↑φ x) = ↑ψ (g y x))
:
This is lemma lem:smooth_updating in the blueprint.
theorem
OpenSmoothEmbedding.dist_update
{𝕜 : Type u_1}
{EX : Type u_2}
{EM : Type u_3}
{EY : Type u_4}
{EN : Type u_5}
{X : Type u_7}
{M : Type u_8}
{Y : Type u_9}
{N : Type u_10}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup EX]
[NormedSpace 𝕜 EX]
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
[NormedAddCommGroup EY]
[NormedSpace 𝕜 EY]
[NormedAddCommGroup EN]
[NormedSpace 𝕜 EN]
{HX : Type u_12}
[TopologicalSpace HX]
{IX : ModelWithCorners 𝕜 EX HX}
{HY : Type u_13}
[TopologicalSpace HY]
{IY : ModelWithCorners 𝕜 EY HY}
{HM : Type u_14}
[TopologicalSpace HM]
{IM : ModelWithCorners 𝕜 EM HM}
{HN : Type u_16}
[TopologicalSpace HN]
{IN : ModelWithCorners 𝕜 EN HN}
[TopologicalSpace X]
[ChartedSpace HX X]
[TopologicalSpace M]
[ChartedSpace HM M]
[MetricSpace Y]
[ChartedSpace HY Y]
[MetricSpace N]
[ChartedSpace HN N]
(φ : OpenSmoothEmbedding IX X IM M)
(ψ : OpenSmoothEmbedding IY Y IN N)
[ProperSpace Y]
{K : Set X}
(hK : IsCompact K)
{P : Type u_17}
[MetricSpace P]
{KP : Set P}
(hKP : IsCompact KP)
(f : P → M → N)
(hf : Continuous ↿f)
(hf' : ∀ (p : P), f p '' Set.range ↑φ ⊆ Set.range ↑ψ)
{ε : M → ℝ}
(hε : ∀ (m : M), 0 < ε m)
(hε' : Continuous ε)
:
This is lem:dist_updating in the blueprint.