internlm/Lean-Github huggingface dataset:
Theorem: sard_local
Proof state before:
case pos
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
s w : Set E
f : E → F
hw : IsOpen w
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
hyp : m < n
hr : 1 ≤ ↑r
hless : ↑μ (f '' s) ≤ 0
⊢ ↑μ (f '' s) = 0
Tactic:
simp only [nonpos_iff_eq_zero, zero_le] at hless ⊢
Proof state after:
case pos
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
s w : Set E
f : E → F
hw : IsOpen w
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
hyp : m < n
hr : 1 ≤ ↑r
hless : ↑μ (f '' s) = 0
⊢ ↑μ (f '' s) = 0
Theorem: sard_local
Proof state before:
case pos
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
s w : Set E
f : E → F
hw : IsOpen w
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
hyp : m < n
hr : 1 ≤ ↑r
hless : ↑μ (f '' s) = 0
⊢ ↑μ (f '' s) = 0
Tactic:
exact hless
Proof state after:
no goals
Theorem: sard_local
Proof state before:
case neg
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
s w : Set E
f : E → F
hw : IsOpen w
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
hyp : ¬m < n
⊢ ↑μ (f '' s) = 0
Tactic:
sorry
Proof state after:
no goals
Theorem: sard_local'
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
s w : Set E
f : E → F
hw : IsOpen w
hs : IsClosed s
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
⊢ IsMeagre (f '' s)
Tactic:
obtain ⟨K''⟩ : Nonempty (PositiveCompacts F) := PositiveCompacts.nonempty'
Proof state after:
case intro
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
s w : Set E
f : E → F
hw : IsOpen w
hs : IsClosed s
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
K'' : PositiveCompacts F
⊢ IsMeagre (f '' s)
Theorem: sard_local'
Proof state before:
case intro
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
s w : Set E
f : E → F
hw : IsOpen w
hs : IsClosed s
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
K'' : PositiveCompacts F
⊢ IsMeagre (f '' s)
Tactic:
let μ : Measure F := addHaarMeasure K''
Proof state after:
case intro
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
s w : Set E
f : E → F
hw : IsOpen w
hs : IsClosed s
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
K'' : PositiveCompacts F
μ : Measure F := addHaarMeasure K''
⊢ IsMeagre (f '' s)
Theorem: sard_local'
Proof state before:
case intro
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
s w : Set E
f : E → F
hw : IsOpen w
hs : IsClosed s
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
K'' : PositiveCompacts F
μ : Measure F := addHaarMeasure K''
⊢ IsMeagre (f '' s)
Tactic:
have ass : μ (f '' s) = 0 := sard_local hr hw hsw hf hf' h'f' μ
Proof state after:
case intro
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
s w : Set E
f : E → F
hw : IsOpen w
hs : IsClosed s
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
K'' : PositiveCompacts F
μ : Measure F := addHaarMeasure K''
ass : ↑μ (f '' s) = 0
⊢ IsMeagre (f '' s)
Theorem: sard_local'
Proof state before:
case intro
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
s w : Set E
f : E → F
hw : IsOpen w
hs : IsClosed s
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
K'' : PositiveCompacts F
μ : Measure F := addHaarMeasure K''
ass : ↑μ (f '' s) = 0
⊢ IsMeagre (f '' s)
Tactic:
have : IsSigmaCompact s := isSigmaCompact_univ.of_isClosed_subset hs (subset_univ s)
Proof state after:
case intro
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
s w : Set E
f : E → F
hw : IsOpen w
hs : IsClosed s
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
K'' : PositiveCompacts F
μ : Measure F := addHaarMeasure K''
ass : ↑μ (f '' s) = 0
this : IsSigmaCompact s
⊢ IsMeagre (f '' s)
Theorem: sard_local'
Proof state before:
case intro
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
s w : Set E
f : E → F
hw : IsOpen w
hs : IsClosed s
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
K'' : PositiveCompacts F
μ : Measure F := addHaarMeasure K''
ass : ↑μ (f '' s) = 0
this : IsSigmaCompact s
⊢ IsMeagre (f '' s)
Tactic:
have : IsSigmaCompact (f '' s) := this.image_of_continuousOn (hf.continuousOn.mono hsw)
Proof state after:
case intro
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
s w : Set E
f : E → F
hw : IsOpen w
hs : IsClosed s
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
K'' : PositiveCompacts F
μ : Measure F := addHaarMeasure K''
ass : ↑μ (f '' s) = 0
this✝ : IsSigmaCompact s
this : IsSigmaCompact (f '' s)
⊢ IsMeagre (f '' s)
Theorem: sard_local'
Proof state before:
case intro
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
s w : Set E
f : E → F
hw : IsOpen w
hs : IsClosed s
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
K'' : PositiveCompacts F
μ : Measure F := addHaarMeasure K''
ass : ↑μ (f '' s) = 0
this✝ : IsSigmaCompact s
this : IsSigmaCompact (f '' s)
⊢ IsMeagre (f '' s)
Tactic:
exact IsMeagre.of_isSigmaCompact_null this ass
Proof state after:
no goals
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)
⊢ MeasureZero J (f '' s)
Tactic:
suffices hyp : ∀ x : M, MeasureZero J (f '' ((chartAt H x).source ∩ s)) from
  measure_zero_image_iff_chart_domains (J := J) hyp
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), MeasureZero J (f '' ((chartAt H x).source ∩ s))
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), MeasureZero J (f '' ((chartAt H x).source ∩ s))
Tactic:
intro 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
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
⊢ MeasureZero J (f '' ((chartAt H x).source ∩ s))
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
⊢ MeasureZero J (f '' ((chartAt H x).source ∩ s))
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✝¹⁵ : 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))