Theorem: sard_local' (Sard/MainTheorem.lean)

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'
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)

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''
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)

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' μ
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)

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)
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)

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)
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)

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
State after:
no goals