internlm/Lean-Github huggingface dataset:
Theorem: diffeoOn_differential_bijective
Proof state before:
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✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr✝ : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this✝ : f '' s = t
this : g '' t = s
hopen : IsOpen (g '' t)
hx2 : x ∈ g '' t
A' : TangentSpace J y →L[ℝ] TangentSpace I (g y) := mfderiv J I g y
hr : 1 ≤ ↑r
hgat : MDifferentiableAt J I g y
hfat : MDifferentiableAt I J f x
inv1 : A'.comp A = ContinuousLinearMap.id ℝ (TangentSpace I x)
⊢ A.comp A' = mfderiv J J (f ∘ g) y
Tactic:
rw [← (hleft_inv x hx)] at hfat
Proof state after:
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✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr✝ : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this✝ : f '' s = t
this : g '' t = s
hopen : IsOpen (g '' t)
hx2 : x ∈ g '' t
A' : TangentSpace J y →L[ℝ] TangentSpace I (g y) := mfderiv J I g y
hr : 1 ≤ ↑r
hgat : MDifferentiableAt J I g y
hfat : MDifferentiableAt I J f (g (f x))
inv1 : A'.comp A = ContinuousLinearMap.id ℝ (TangentSpace I x)
⊢ A.comp A' = mfderiv J J (f ∘ g) y
Theorem: diffeoOn_differential_bijective
Proof state before:
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✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
f : M → N
g : N → M
r : ℕ
hr✝ : 1 ≤ r
s : Set M
hs : IsOpen s
t : Set N
ht : IsOpen t
x : M
hx : x ∈ s
hst : MapsTo f s t
hts : MapsTo g t s
hleft_inv : ∀ x ∈ s, g (f x) = x
hright_inv : ∀ y ∈ t, f (g y) = y
hf : ContMDiffOn I J (↑r) f s
hg : ContMDiffOn J I (↑r) g t
A : TangentSpace I x →L[ℝ] TangentSpace J (f x) := mfderiv I J f x
y : N := f x
hyx : g y = x
hysource : y ∈ t
this✝ : f '' s = t
this : g '' t = s
hopen : IsOpen (g '' t)
hx2 : x ∈ g '' t
A' : TangentSpace J y →L[ℝ] TangentSpace I (g y) := mfderiv J I g y
hr : 1 ≤ ↑r
hgat : MDifferentiableAt J I g y
hfat : MDifferentiableAt I J f (g (f x))
inv1 : A'.comp A = ContinuousLinearMap.id ℝ (TangentSpace I x)
⊢ A.comp A' = mfderiv J J (f ∘ g) y
Tactic:
exact (hyx ▸ (mfderiv_comp (f x) hfat hgat)).symm
Proof state after:
no goals
Theorem: diffeo_differential_bijective
Proof state before:
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✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
r : ℕ
hr : 1 ≤ r
f : M ≃ₘ^↑r⟮I, J⟯ N
x : M
⊢ Bijective ⇑(mfderiv I J (⇑f) x)
Tactic:
refine diffeoOn_differential_bijective I J hr isOpen_univ isOpen_univ trivial (mapsTo_univ f.toFun univ) (mapsTo_univ f.invFun univ) ?_ ?_ ?_ ?_
Proof state after:
case refine_1
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✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
r : ℕ
hr : 1 ≤ r
f : M ≃ₘ^↑r⟮I, J⟯ N
x : M
⊢ ∀ x ∈ univ, f.invFun (f x) = x

case refine_2
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✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
r : ℕ
hr : 1 ≤ r
f : M ≃ₘ^↑r⟮I, J⟯ N
x : M
⊢ ∀ y ∈ univ, f (f.invFun y) = y

case refine_3
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✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
r : ℕ
hr : 1 ≤ r
f : M ≃ₘ^↑r⟮I, J⟯ N
x : M
⊢ ContMDiffOn I J (↑r) (⇑f) univ

case refine_4
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✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
r : ℕ
hr : 1 ≤ r
f : M ≃ₘ^↑r⟮I, J⟯ N
x : M
⊢ ContMDiffOn J I (↑r) f.invFun univ
Theorem: diffeo_differential_bijective
Proof state before:
case refine_1
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✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
r : ℕ
hr : 1 ≤ r
f : M ≃ₘ^↑r⟮I, J⟯ N
x : M
⊢ ∀ x ∈ univ, f.invFun (f x) = x
Tactic:
exact fun _ hx ↦ f.toPartialEquiv.left_inv' hx
Proof state after:
no goals
Theorem: diffeo_differential_bijective
Proof state before:
case refine_2
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✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
r : ℕ
hr : 1 ≤ r
f : M ≃ₘ^↑r⟮I, J⟯ N
x : M
⊢ ∀ y ∈ univ, f (f.invFun y) = y
Tactic:
exact fun _ hy ↦ f.toPartialEquiv.right_inv' hy
Proof state after:
no goals
Theorem: diffeo_differential_bijective
Proof state before:
case refine_3
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✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
r : ℕ
hr : 1 ≤ r
f : M ≃ₘ^↑r⟮I, J⟯ N
x : M
⊢ ContMDiffOn I J (↑r) (⇑f) univ
Tactic:
exact contMDiffOn_univ.mpr f.contMDiff_toFun
Proof state after:
no goals
Theorem: diffeo_differential_bijective
Proof state before:
case refine_4
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✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
r : ℕ
hr : 1 ≤ r
f : M ≃ₘ^↑r⟮I, J⟯ N
x : M
⊢ ContMDiffOn J I (↑r) f.invFun univ
Tactic:
exact contMDiffOn_univ.mpr f.contMDiff_invFun
Proof state after:
no goals
Theorem: extendedChart_smooth
Proof state before:
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✝⁷ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
G : Type u_5
inst✝⁴ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
inst✝¹ : SmoothManifoldWithCorners J N
e : PartialHomeomorph M H
he : e ∈ atlas H M
inst✝ : I.Boundaryless
⊢ ContMDiffOn I 𝓘(ℝ, E) ⊤ (↑(e.extend I)) e.source
Tactic:
let e' : PartialHomeomorph E E := PartialHomeomorph.refl E
Proof state after:
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✝⁷ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
G : Type u_5
inst✝⁴ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
inst✝¹ : SmoothManifoldWithCorners J N
e : PartialHomeomorph M H
he : e ∈ atlas H M
inst✝ : I.Boundaryless
e' : PartialHomeomorph E E := PartialHomeomorph.refl E
⊢ ContMDiffOn I 𝓘(ℝ, E) ⊤ (↑(e.extend I)) e.source
Theorem: extendedChart_smooth
Proof state before:
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✝⁷ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
G : Type u_5
inst✝⁴ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
inst✝¹ : SmoothManifoldWithCorners J N
e : PartialHomeomorph M H
he : e ∈ atlas H M
inst✝ : I.Boundaryless
e' : PartialHomeomorph E E := PartialHomeomorph.refl E
⊢ ContMDiffOn I 𝓘(ℝ, E) ⊤ (↑(e.extend I)) e.source
Tactic:
have h₁ : e ∈ maximalAtlas I M := subset_maximalAtlas _ he
Proof state after:
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✝⁷ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
G : Type u_5
inst✝⁴ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
inst✝¹ : SmoothManifoldWithCorners J N
e : PartialHomeomorph M H
he : e ∈ atlas H M
inst✝ : I.Boundaryless
e' : PartialHomeomorph E E := PartialHomeomorph.refl E
h₁ : e ∈ maximalAtlas I M
⊢ ContMDiffOn I 𝓘(ℝ, E) ⊤ (↑(e.extend I)) e.source
Theorem: extendedChart_smooth
Proof state before:
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✝⁷ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
G : Type u_5
inst✝⁴ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
inst✝¹ : SmoothManifoldWithCorners J N
e : PartialHomeomorph M H
he : e ∈ atlas H M
inst✝ : I.Boundaryless
e' : PartialHomeomorph E E := PartialHomeomorph.refl E
h₁ : e ∈ maximalAtlas I M
⊢ ContMDiffOn I 𝓘(ℝ, E) ⊤ (↑(e.extend I)) e.source
Tactic:
have h₂ : e' ∈ maximalAtlas 𝓘(ℝ, E) E := subset_maximalAtlas _ (by rfl)
Proof state after:
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✝⁷ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
G : Type u_5
inst✝⁴ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
inst✝¹ : SmoothManifoldWithCorners J N
e : PartialHomeomorph M H
he : e ∈ atlas H M
inst✝ : I.Boundaryless
e' : PartialHomeomorph E E := PartialHomeomorph.refl E
h₁ : e ∈ maximalAtlas I M
h₂ : e' ∈ maximalAtlas 𝓘(ℝ, E) E
⊢ ContMDiffOn I 𝓘(ℝ, E) ⊤ (↑(e.extend I)) e.source
Theorem: extendedChart_smooth
Proof state before:
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✝⁷ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
G : Type u_5
inst✝⁴ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
inst✝¹ : SmoothManifoldWithCorners J N
e : PartialHomeomorph M H
he : e ∈ atlas H M
inst✝ : I.Boundaryless
e' : PartialHomeomorph E E := PartialHomeomorph.refl E
h₁ : e ∈ maximalAtlas I M
h₂ : e' ∈ maximalAtlas 𝓘(ℝ, E) E
⊢ ContMDiffOn I 𝓘(ℝ, E) ⊤ (↑(e.extend I)) e.source
Tactic:
set f := e.extend I ∘ (e.extend I).symm
Proof state after:
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✝⁷ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
G : Type u_5
inst✝⁴ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
inst✝¹ : SmoothManifoldWithCorners J N
e : PartialHomeomorph M H
he : e ∈ atlas H M
inst✝ : I.Boundaryless
e' : PartialHomeomorph E E := PartialHomeomorph.refl E
h₁ : e ∈ maximalAtlas I M
h₂ : e' ∈ maximalAtlas 𝓘(ℝ, E) E
f : E → E := ↑(e.extend I) ∘ ↑(e.extend I).symm
⊢ ContMDiffOn I 𝓘(ℝ, E) ⊤ (↑(e.extend I)) e.source
Theorem: extendedChart_smooth
Proof state before:
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✝⁷ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
G : Type u_5
inst✝⁴ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
inst✝¹ : SmoothManifoldWithCorners J N
e : PartialHomeomorph M H
he : e ∈ atlas H M
inst✝ : I.Boundaryless
e' : PartialHomeomorph E E := PartialHomeomorph.refl E
h₁ : e ∈ maximalAtlas I M
h₂ : e' ∈ maximalAtlas 𝓘(ℝ, E) E
f : E → E := ↑(e.extend I) ∘ ↑(e.extend I).symm
⊢ ContMDiffOn I 𝓘(ℝ, E) ⊤ (↑(e.extend I)) e.source
Tactic:
have h : ∀ x ∈ (e.extend I) '' e.source, f x = x := fun _ hx ↦ e.extend_right_inv I hx
Proof state after:
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✝⁷ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
G : Type u_5
inst✝⁴ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
inst✝¹ : SmoothManifoldWithCorners J N
e : PartialHomeomorph M H
he : e ∈ atlas H M
inst✝ : I.Boundaryless
e' : PartialHomeomorph E E := PartialHomeomorph.refl E
h₁ : e ∈ maximalAtlas I M
h₂ : e' ∈ maximalAtlas 𝓘(ℝ, E) E
f : E → E := ↑(e.extend I) ∘ ↑(e.extend I).symm
h : ∀ x ∈ ↑(e.extend I) '' e.source, f x = x
⊢ ContMDiffOn I 𝓘(ℝ, E) ⊤ (↑(e.extend I)) e.source
Theorem: extendedChart_smooth
Proof state before:
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✝⁷ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
G : Type u_5
inst✝⁴ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
inst✝¹ : SmoothManifoldWithCorners J N
e : PartialHomeomorph M H
he : e ∈ atlas H M
inst✝ : I.Boundaryless
e' : PartialHomeomorph E E := PartialHomeomorph.refl E
h₁ : e ∈ maximalAtlas I M
h₂ : e' ∈ maximalAtlas 𝓘(ℝ, E) E
f : E → E := ↑(e.extend I) ∘ ↑(e.extend I).symm
h : ∀ x ∈ ↑(e.extend I) '' e.source, f x = x
⊢ ContMDiffOn I 𝓘(ℝ, E) ⊤ (↑(e.extend I)) e.source
Tactic:
apply (contMDiffOn_iff_of_mem_maximalAtlas' h₁ h₂ (Eq.subset rfl) (mapsTo_univ _ _)).mpr
Proof state after:
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✝⁷ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
G : Type u_5
inst✝⁴ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
inst✝¹ : SmoothManifoldWithCorners J N
e : PartialHomeomorph M H
he : e ∈ atlas H M
inst✝ : I.Boundaryless
e' : PartialHomeomorph E E := PartialHomeomorph.refl E
h₁ : e ∈ maximalAtlas I M
h₂ : e' ∈ maximalAtlas 𝓘(ℝ, E) E
f : E → E := ↑(e.extend I) ∘ ↑(e.extend I).symm
h : ∀ x ∈ ↑(e.extend I) '' e.source, f x = x
⊢ ContDiffOn ℝ ⊤ (↑(e'.extend 𝓘(ℝ, E)) ∘ ↑(e.extend I) ∘ ↑(e.extend I).symm) (↑(e.extend I) '' e.source)
Theorem: extendedChart_smooth
Proof state before:
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✝⁷ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
G : Type u_5
inst✝⁴ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
inst✝¹ : SmoothManifoldWithCorners J N
e : PartialHomeomorph M H
he : e ∈ atlas H M
inst✝ : I.Boundaryless
e' : PartialHomeomorph E E := PartialHomeomorph.refl E
h₁ : e ∈ maximalAtlas I M
h₂ : e' ∈ maximalAtlas 𝓘(ℝ, E) E
f : E → E := ↑(e.extend I) ∘ ↑(e.extend I).symm
h : ∀ x ∈ ↑(e.extend I) '' e.source, f x = x
⊢ ContDiffOn ℝ ⊤ (↑(e'.extend 𝓘(ℝ, E)) ∘ ↑(e.extend I) ∘ ↑(e.extend I).symm) (↑(e.extend I) '' e.source)
Tactic:
exact ContMDiffOn.contDiffOn (fun x hx ↦ ContMDiffWithinAt.congr smoothWithinAt_id h (h x hx))
Proof state after:
no goals
Theorem: extendedChart_smooth
Proof state before:
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✝⁷ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
G : Type u_5
inst✝⁴ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
inst✝¹ : SmoothManifoldWithCorners J N
e : PartialHomeomorph M H
he : e ∈ atlas H M
inst✝ : I.Boundaryless
e' : PartialHomeomorph E E := PartialHomeomorph.refl E
h₁ : e ∈ maximalAtlas I M
⊢ e' ∈ atlas E E
Tactic:
rfl
Proof state after:
no goals
Theorem: ofSet_in_maximal_atlas
Proof state before:
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✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
s : Set E
hs : IsOpen s
⊢ PartialHomeomorph.ofSet s hs ∈ maximalAtlas 𝓘(ℝ, E) E
Tactic:
rw [maximalAtlas, mem_maximalAtlas_iff]
Proof state after:
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✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
s : Set E
hs : IsOpen s
⊢ ∀ e' ∈ atlas E E,
    (PartialHomeomorph.ofSet s hs).symm.trans e' ∈ contDiffGroupoid ⊤ 𝓘(ℝ, E) ∧
      e'.symm.trans (PartialHomeomorph.ofSet s hs) ∈ contDiffGroupoid ⊤ 𝓘(ℝ, E)
Theorem: ofSet_in_maximal_atlas
Proof state before:
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✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
s : Set E
hs : IsOpen s
⊢ ∀ e' ∈ atlas E E,
    (PartialHomeomorph.ofSet s hs).symm.trans e' ∈ contDiffGroupoid ⊤ 𝓘(ℝ, E) ∧
      e'.symm.trans (PartialHomeomorph.ofSet s hs) ∈ contDiffGroupoid ⊤ 𝓘(ℝ, E)
Tactic:
intro e' he'
Proof state after:
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✝⁶ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_5
inst✝³ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝² : TopologicalSpace N
inst✝¹ : ChartedSpace G N
inst✝ : SmoothManifoldWithCorners J N
s : Set E
hs : IsOpen s
e' : PartialHomeomorph E E
he' : e' ∈ atlas E E
⊢ (PartialHomeomorph.ofSet s hs).symm.trans e' ∈ contDiffGroupoid ⊤ 𝓘(ℝ, E) ∧
    e'.symm.trans (PartialHomeomorph.ofSet s hs) ∈ contDiffGroupoid ⊤ 𝓘(ℝ, E)