internlm/Lean-Github huggingface dataset:
Theorem: image_null_of_C1_of_dimension_increase
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✝¹⁵ : I.Boundaryless
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
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✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
hdim : m < n
x : M
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
⊢ ↑μ (↑J ∘ ↑(chartAt G y) '' ((chartAt G y).source ∩ f '' ((chartAt H x).source ∩ univ))) = 0
Tactic:
let e := chartAt H 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✝¹⁵ : I.Boundaryless
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
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✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
hdim : m < n
x : M
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e : PartialHomeomorph M H := chartAt H x
⊢ ↑μ (↑J ∘ ↑(chartAt G y) '' ((chartAt G y).source ∩ f '' ((chartAt H x).source ∩ univ))) = 0
Theorem: image_null_of_C1_of_dimension_increase
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✝¹⁵ : I.Boundaryless
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
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✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
hdim : m < n
x : M
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e : PartialHomeomorph M H := chartAt H x
⊢ ↑μ (↑J ∘ ↑(chartAt G y) '' ((chartAt G y).source ∩ f '' ((chartAt H x).source ∩ univ))) = 0
Tactic:
let e' := chartAt 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✝¹⁵ : I.Boundaryless
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
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✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
hdim : m < n
x : M
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e : PartialHomeomorph M H := chartAt H x
e' : PartialHomeomorph N G := chartAt G y
⊢ ↑μ (↑J ∘ ↑(chartAt G y) '' ((chartAt G y).source ∩ f '' ((chartAt H x).source ∩ univ))) = 0
Theorem: image_null_of_C1_of_dimension_increase
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✝¹⁵ : I.Boundaryless
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
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✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
hdim : m < n
x : M
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e : PartialHomeomorph M H := chartAt H x
e' : PartialHomeomorph N G := chartAt G y
⊢ ↑μ (↑J ∘ ↑(chartAt G y) '' ((chartAt G y).source ∩ f '' ((chartAt H x).source ∩ univ))) = 0
Tactic:
have aux : J ∘ e' '' (e'.source ∩ f '' e.source) = (J ∘ e' ∘ f) '' e.source := by sorry
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✝¹⁵ : I.Boundaryless
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
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✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
hdim : m < n
x : M
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e : PartialHomeomorph M H := chartAt H x
e' : PartialHomeomorph N G := chartAt G y
aux : ↑J ∘ ↑e' '' (e'.source ∩ f '' e.source) = ↑J ∘ ↑e' ∘ f '' e.source
⊢ ↑μ (↑J ∘ ↑(chartAt G y) '' ((chartAt G y).source ∩ f '' ((chartAt H x).source ∩ univ))) = 0
Theorem: image_null_of_C1_of_dimension_increase
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✝¹⁵ : I.Boundaryless
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
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✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
hdim : m < n
x : M
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e : PartialHomeomorph M H := chartAt H x
e' : PartialHomeomorph N G := chartAt G y
aux : ↑J ∘ ↑e' '' (e'.source ∩ f '' e.source) = ↑J ∘ ↑e' ∘ f '' e.source
⊢ ↑μ (↑J ∘ ↑(chartAt G y) '' ((chartAt G y).source ∩ f '' ((chartAt H x).source ∩ univ))) = 0
Tactic:
rw [inter_univ, aux]
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✝¹⁵ : I.Boundaryless
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
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✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
hdim : m < n
x : M
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e : PartialHomeomorph M H := chartAt H x
e' : PartialHomeomorph N G := chartAt G y
aux : ↑J ∘ ↑e' '' (e'.source ∩ f '' e.source) = ↑J ∘ ↑e' ∘ f '' e.source
⊢ ↑μ (↑J ∘ ↑e' ∘ f '' e.source) = 0
Theorem: image_null_of_C1_of_dimension_increase
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✝¹⁵ : I.Boundaryless
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
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✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
hdim : m < n
x : M
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e : PartialHomeomorph M H := chartAt H x
e' : PartialHomeomorph N G := chartAt G y
aux : ↑J ∘ ↑e' '' (e'.source ∩ f '' e.source) = ↑J ∘ ↑e' ∘ f '' e.source
⊢ ↑μ (↑J ∘ ↑e' ∘ f '' e.source) = 0
Tactic:
let g : E → F := J ∘ e' ∘ f ∘ e.invFun ∘ I.invFun
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✝¹⁵ : I.Boundaryless
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
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✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
hdim : m < n
x : M
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e : PartialHomeomorph M H := chartAt H x
e' : PartialHomeomorph N G := chartAt G y
aux : ↑J ∘ ↑e' '' (e'.source ∩ f '' e.source) = ↑J ∘ ↑e' ∘ f '' e.source
g : E → F := ↑J ∘ ↑e' ∘ f ∘ e.invFun ∘ I.invFun
⊢ ↑μ (↑J ∘ ↑e' ∘ f '' e.source) = 0
Theorem: image_null_of_C1_of_dimension_increase
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✝¹⁵ : I.Boundaryless
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
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✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
hdim : m < n
x : M
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e : PartialHomeomorph M H := chartAt H x
e' : PartialHomeomorph N G := chartAt G y
aux : ↑J ∘ ↑e' '' (e'.source ∩ f '' e.source) = ↑J ∘ ↑e' ∘ f '' e.source
g : E → F := ↑J ∘ ↑e' ∘ f ∘ e.invFun ∘ I.invFun
⊢ ↑μ (↑J ∘ ↑e' ∘ f '' e.source) = 0
Tactic:
have : (J ∘ ↑e' ∘ f '' e.source) = g '' (I '' e.target) := by sorry
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✝¹⁵ : I.Boundaryless
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
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✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
hdim : m < n
x : M
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e : PartialHomeomorph M H := chartAt H x
e' : PartialHomeomorph N G := chartAt G y
aux : ↑J ∘ ↑e' '' (e'.source ∩ f '' e.source) = ↑J ∘ ↑e' ∘ f '' e.source
g : E → F := ↑J ∘ ↑e' ∘ f ∘ e.invFun ∘ I.invFun
this : ↑J ∘ ↑e' ∘ f '' e.source = g '' (↑I '' e.target)
⊢ ↑μ (↑J ∘ ↑e' ∘ f '' e.source) = 0
Theorem: image_null_of_C1_of_dimension_increase
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✝¹⁵ : I.Boundaryless
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
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✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
hdim : m < n
x : M
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e : PartialHomeomorph M H := chartAt H x
e' : PartialHomeomorph N G := chartAt G y
aux : ↑J ∘ ↑e' '' (e'.source ∩ f '' e.source) = ↑J ∘ ↑e' ∘ f '' e.source
g : E → F := ↑J ∘ ↑e' ∘ f ∘ e.invFun ∘ I.invFun
this : ↑J ∘ ↑e' ∘ f '' e.source = g '' (↑I '' e.target)
⊢ ↑μ (↑J ∘ ↑e' ∘ f '' e.source) = 0
Tactic:
have hopen : IsOpen (I '' e.target) := by sorry
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✝¹⁵ : I.Boundaryless
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
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✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
hdim : m < n
x : M
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e : PartialHomeomorph M H := chartAt H x
e' : PartialHomeomorph N G := chartAt G y
aux : ↑J ∘ ↑e' '' (e'.source ∩ f '' e.source) = ↑J ∘ ↑e' ∘ f '' e.source
g : E → F := ↑J ∘ ↑e' ∘ f ∘ e.invFun ∘ I.invFun
this : ↑J ∘ ↑e' ∘ f '' e.source = g '' (↑I '' e.target)
hopen : IsOpen (↑I '' e.target)
⊢ ↑μ (↑J ∘ ↑e' ∘ f '' e.source) = 0
Theorem: image_null_of_C1_of_dimension_increase
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✝¹⁵ : I.Boundaryless
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
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✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
hdim : m < n
x : M
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e : PartialHomeomorph M H := chartAt H x
e' : PartialHomeomorph N G := chartAt G y
aux : ↑J ∘ ↑e' '' (e'.source ∩ f '' e.source) = ↑J ∘ ↑e' ∘ f '' e.source
g : E → F := ↑J ∘ ↑e' ∘ f ∘ e.invFun ∘ I.invFun
this : ↑J ∘ ↑e' ∘ f '' e.source = g '' (↑I '' e.target)
hopen : IsOpen (↑I '' e.target)
⊢ ↑μ (↑J ∘ ↑e' ∘ f '' e.source) = 0
Tactic:
have gdiff : ContDiffOn ℝ 1 g (I '' e.target) := by sorry
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✝¹⁵ : I.Boundaryless
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
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✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
hdim : m < n
x : M
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e : PartialHomeomorph M H := chartAt H x
e' : PartialHomeomorph N G := chartAt G y
aux : ↑J ∘ ↑e' '' (e'.source ∩ f '' e.source) = ↑J ∘ ↑e' ∘ f '' e.source
g : E → F := ↑J ∘ ↑e' ∘ f ∘ e.invFun ∘ I.invFun
this : ↑J ∘ ↑e' ∘ f '' e.source = g '' (↑I '' e.target)
hopen : IsOpen (↑I '' e.target)
gdiff : ContDiffOn ℝ 1 g (↑I '' e.target)
⊢ ↑μ (↑J ∘ ↑e' ∘ f '' e.source) = 0
Theorem: image_null_of_C1_of_dimension_increase
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✝¹⁵ : I.Boundaryless
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
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✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
hdim : m < n
x : M
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e : PartialHomeomorph M H := chartAt H x
e' : PartialHomeomorph N G := chartAt G y
aux : ↑J ∘ ↑e' '' (e'.source ∩ f '' e.source) = ↑J ∘ ↑e' ∘ f '' e.source
g : E → F := ↑J ∘ ↑e' ∘ f ∘ e.invFun ∘ I.invFun
this : ↑J ∘ ↑e' ∘ f '' e.source = g '' (↑I '' e.target)
hopen : IsOpen (↑I '' e.target)
gdiff : ContDiffOn ℝ 1 g (↑I '' e.target)
⊢ ↑μ (↑J ∘ ↑e' ∘ f '' e.source) = 0
Tactic:
rw [this]
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✝¹⁵ : I.Boundaryless
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
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✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
hdim : m < n
x : M
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e : PartialHomeomorph M H := chartAt H x
e' : PartialHomeomorph N G := chartAt G y
aux : ↑J ∘ ↑e' '' (e'.source ∩ f '' e.source) = ↑J ∘ ↑e' ∘ f '' e.source
g : E → F := ↑J ∘ ↑e' ∘ f ∘ e.invFun ∘ I.invFun
this : ↑J ∘ ↑e' ∘ f '' e.source = g '' (↑I '' e.target)
hopen : IsOpen (↑I '' e.target)
gdiff : ContDiffOn ℝ 1 g (↑I '' e.target)
⊢ ↑μ (g '' (↑I '' e.target)) = 0
Theorem: image_null_of_C1_of_dimension_increase
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✝¹⁵ : I.Boundaryless
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
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✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
hdim : m < n
x : M
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e : PartialHomeomorph M H := chartAt H x
e' : PartialHomeomorph N G := chartAt G y
aux : ↑J ∘ ↑e' '' (e'.source ∩ f '' e.source) = ↑J ∘ ↑e' ∘ f '' e.source
g : E → F := ↑J ∘ ↑e' ∘ f ∘ e.invFun ∘ I.invFun
this : ↑J ∘ ↑e' ∘ f '' e.source = g '' (↑I '' e.target)
hopen : IsOpen (↑I '' e.target)
gdiff : ContDiffOn ℝ 1 g (↑I '' e.target)
⊢ ↑μ (g '' (↑I '' e.target)) = 0
Tactic:
apply image_measure_zero_of_C1_dimension_increase hopen μ gdiff hdim
Proof state after:
no goals