internlm/Lean-Github huggingface dataset:
Theorem: bijective_iff_inverses'
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
X : Type u_7
Y : Type u_8
inst✝³ : NormedAddCommGroup X
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f : X →L[ℝ] Y
g : Y →L[ℝ] X
h1 : g.comp f = ContinuousLinearMap.id ℝ X
h2 : f.comp g = ContinuousLinearMap.id ℝ Y
h : f.toFun ∘ g.toFun = id
⊢ Bijective ⇑f
Tactic:
have : g.toFun ∘ f.toFun = id := by calc g.toFun ∘ f.toFun
  _ = (g.comp f).toFun := rfl
  _ = (ContinuousLinearMap.id ℝ X).toFun := by rw [h1]
  _ = id := 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
X : Type u_7
Y : Type u_8
inst✝³ : NormedAddCommGroup X
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f : X →L[ℝ] Y
g : Y →L[ℝ] X
h1 : g.comp f = ContinuousLinearMap.id ℝ X
h2 : f.comp g = ContinuousLinearMap.id ℝ Y
h : f.toFun ∘ g.toFun = id
this : g.toFun ∘ f.toFun = id
⊢ Bijective ⇑f
Theorem: bijective_iff_inverses'
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
X : Type u_7
Y : Type u_8
inst✝³ : NormedAddCommGroup X
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f : X →L[ℝ] Y
g : Y →L[ℝ] X
h1 : g.comp f = ContinuousLinearMap.id ℝ X
h2 : f.comp g = ContinuousLinearMap.id ℝ Y
h : f.toFun ∘ g.toFun = id
this : g.toFun ∘ f.toFun = id
⊢ Bijective ⇑f
Tactic:
exact bijective_iff_inverses this h
Proof state after:
no goals
Theorem: bijective_iff_inverses'
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
X : Type u_7
Y : Type u_8
inst✝³ : NormedAddCommGroup X
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f : X →L[ℝ] Y
g : Y →L[ℝ] X
h1 : g.comp f = ContinuousLinearMap.id ℝ X
h2 : f.comp g = ContinuousLinearMap.id ℝ Y
⊢ (f.comp g).toFun = (ContinuousLinearMap.id ℝ Y).toFun
Tactic:
rw [h2]
Proof state after:
no goals
Theorem: bijective_iff_inverses'
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
X : Type u_7
Y : Type u_8
inst✝³ : NormedAddCommGroup X
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f : X →L[ℝ] Y
g : Y →L[ℝ] X
h1 : g.comp f = ContinuousLinearMap.id ℝ X
h2 : f.comp g = ContinuousLinearMap.id ℝ Y
h : f.toFun ∘ g.toFun = id
⊢ g.toFun ∘ f.toFun = id
Tactic:
calc g.toFun ∘ f.toFun
_ = (g.comp f).toFun := rfl
_ = (ContinuousLinearMap.id ℝ X).toFun := by rw [h1]
_ = id := rfl
Proof state after:
no goals
Theorem: bijective_iff_inverses'
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
X : Type u_7
Y : Type u_8
inst✝³ : NormedAddCommGroup X
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f : X →L[ℝ] Y
g : Y →L[ℝ] X
h1 : g.comp f = ContinuousLinearMap.id ℝ X
h2 : f.comp g = ContinuousLinearMap.id ℝ Y
h : f.toFun ∘ g.toFun = id
⊢ (g.comp f).toFun = (ContinuousLinearMap.id ℝ X).toFun
Tactic:
rw [h1]
Proof state after:
no goals
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
⊢ Bijective ⇑(mfderiv I J f x)
Tactic:
set A := mfderiv I J f x
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
⊢ Bijective ⇑A
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
⊢ Bijective ⇑A
Tactic:
let y := f x
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
⊢ Bijective ⇑A
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
⊢ Bijective ⇑A
Tactic:
have hyx : g y = x := hleft_inv x 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
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
⊢ Bijective ⇑A
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
⊢ Bijective ⇑A
Tactic:
have hysource : y ∈ t := hst 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
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
⊢ Bijective ⇑A
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
⊢ Bijective ⇑A
Tactic:
have : f '' s = t := subset_antisymm (mapsTo'.mp hst) (fun y hy ↦ ⟨g y, hts hy, hright_inv y hy⟩)
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
⊢ Bijective ⇑A
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
⊢ Bijective ⇑A
Tactic:
have : g '' t = s := by
  rw [← this, ← image_comp]
  exact EqOn.image_eq_self hleft_inv
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
⊢ Bijective ⇑A
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
⊢ Bijective ⇑A
Tactic:
have hopen : IsOpen (g '' t) := by rw [this]; exact hs
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)
⊢ Bijective ⇑A
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)
⊢ Bijective ⇑A
Tactic:
have hx2 : x ∈ g '' t := by simp_rw [this]; exact 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
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
⊢ Bijective ⇑A
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
⊢ Bijective ⇑A
Tactic:
let A' := mfderiv J I g y
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
⊢ Bijective ⇑A