internlm/Lean-Github huggingface dataset:
Theorem: sard_boundaryless
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
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✝⁵ : 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
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x : M
e : PartialHomeomorph M H := chartAt H x
⊢ MeasureZero J (f '' ((chartAt H x).source ∩ s))
Tactic:
intro μ hμ 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
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✝⁵ : 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
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x : M
e : PartialHomeomorph M H := chartAt H x
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
⊢ ↑μ (↑J ∘ ↑(chartAt G y) '' ((chartAt G y).source ∩ f '' ((chartAt H x).source ∩ s))) = 0
Theorem: sard_boundaryless
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
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✝⁵ : 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
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x : M
e : PartialHomeomorph M H := chartAt H x
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
⊢ ↑μ (↑J ∘ ↑(chartAt G y) '' ((chartAt G y).source ∩ f '' ((chartAt H x).source ∩ s))) = 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✝¹⁵ : 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✝⁵ : 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
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x : M
e : PartialHomeomorph M H := chartAt H x
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
⊢ ↑μ (↑J ∘ ↑(chartAt G y) '' ((chartAt G y).source ∩ f '' ((chartAt H x).source ∩ s))) = 0
Theorem: sard_boundaryless
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
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✝⁵ : 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
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x : M
e : PartialHomeomorph M H := chartAt H x
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
⊢ ↑μ (↑J ∘ ↑(chartAt G y) '' ((chartAt G y).source ∩ f '' ((chartAt H x).source ∩ s))) = 0
Tactic:
let w := e.extend I '' (e.source ∩ f ⁻¹' e'.source)
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
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✝⁵ : 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
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x : M
e : PartialHomeomorph M H := chartAt H x
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
⊢ ↑μ (↑J ∘ ↑(chartAt G y) '' ((chartAt G y).source ∩ f '' ((chartAt H x).source ∩ s))) = 0
Theorem: sard_boundaryless
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
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✝⁵ : 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
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x : M
e : PartialHomeomorph M H := chartAt H x
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
⊢ ↑μ (↑J ∘ ↑(chartAt G y) '' ((chartAt G y).source ∩ f '' ((chartAt H x).source ∩ s))) = 0
Tactic:
let s_better := (e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
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
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✝⁵ : 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
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x : M
e : PartialHomeomorph M H := chartAt H x
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
⊢ ↑μ (↑J ∘ ↑(chartAt G y) '' ((chartAt G y).source ∩ f '' ((chartAt H x).source ∩ s))) = 0
Theorem: sard_boundaryless
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
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✝⁵ : 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
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x : M
e : PartialHomeomorph M H := chartAt H x
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
⊢ ↑μ (↑J ∘ ↑(chartAt G y) '' ((chartAt G y).source ∩ f '' ((chartAt H x).source ∩ s))) = 0
Tactic:
let f_local := (J ∘ e') ∘ f ∘ (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
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✝⁵ : 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
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x : M
e : PartialHomeomorph M H := chartAt H x
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
⊢ ↑μ (↑J ∘ ↑(chartAt G y) '' ((chartAt G y).source ∩ f '' ((chartAt H x).source ∩ s))) = 0
Theorem: sard_boundaryless
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
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✝⁵ : 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
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x : M
e : PartialHomeomorph M H := chartAt H x
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
⊢ ↑μ (↑J ∘ ↑(chartAt G y) '' ((chartAt G y).source ∩ f '' ((chartAt H x).source ∩ s))) = 0
Tactic:
have hwopen : IsOpen w := by
  refine e.extend_isOpenMapOn_source I ?_ (inter_subset_left _ _)
  exact e.open_source.inter (e'.open_source.preimage hf.continuous)
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
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✝⁵ : 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
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x : M
e : PartialHomeomorph M H := chartAt H x
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
⊢ ↑μ (↑J ∘ ↑(chartAt G y) '' ((chartAt G y).source ∩ f '' ((chartAt H x).source ∩ s))) = 0
Theorem: sard_boundaryless
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
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✝⁵ : 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
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x : M
e : PartialHomeomorph M H := chartAt H x
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
⊢ ↑μ (↑J ∘ ↑(chartAt G y) '' ((chartAt G y).source ∩ f '' ((chartAt H x).source ∩ s))) = 0
Tactic:
have hsw : s_better ⊆ w := by
  apply image_subset
  rw [inter_assoc]
  apply inter_subset_right s _
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
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✝⁵ : 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
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x : M
e : PartialHomeomorph M H := chartAt H x
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
hsw : s_better ⊆ w
⊢ ↑μ (↑J ∘ ↑(chartAt G y) '' ((chartAt G y).source ∩ f '' ((chartAt H x).source ∩ s))) = 0
Theorem: sard_boundaryless
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
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✝⁵ : 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
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x : M
e : PartialHomeomorph M H := chartAt H x
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
hsw : s_better ⊆ w
⊢ ↑μ (↑J ∘ ↑(chartAt G y) '' ((chartAt G y).source ∩ f '' ((chartAt H x).source ∩ s))) = 0
Tactic:
have hsbetter₀ : s_better ⊆ e.extend I '' e.source := by
  apply image_subset
  rw [inter_comm s, inter_assoc]
  exact inter_subset_left _ _
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
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✝⁵ : 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
inst✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
x : M
e : PartialHomeomorph M H := chartAt H x
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e' : PartialHomeomorph N G := chartAt G y
w : Set E := ↑(e.extend I) '' (e.source ∩ f ⁻¹' e'.source)
s_better : Set E := ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source)
f_local : E → F := (↑J ∘ ↑e') ∘ f ∘ ↑(e.extend I).symm
hwopen : IsOpen w
hsw : s_better ⊆ w
hsbetter₀ : s_better ⊆ ↑(e.extend I) '' e.source
⊢ ↑μ (↑J ∘ ↑(chartAt G y) '' ((chartAt G y).source ∩ f '' ((chartAt H x).source ∩ s))) = 0