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✝
μ : 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
cor : ↑(e.extend I).symm ∘ ↑(e.extend I) '' (s ∩ e.source ∩ f ⁻¹' e'.source) = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter : ↑(e.extend I).symm '' s_better = s ∩ e.source ∩ f ⁻¹' e'.source
hsbetter₁ : ↑(e.extend I).symm '' s_better ⊆ s
hsbetter₂ : ↑(e.extend I).symm '' s_better ⊆ e.source
hw : f ∘ ↑(e.extend I).symm '' w ⊆ e'.source
hsbetter₃ : f ∘ ↑(e.extend I).symm '' s_better ⊆ e'.source
this✝¹ : ↑J ∘ ↑e' '' (e'.source ∩ f '' (e.source ∩ s)) = f_local '' s_better
x : E
hx : x ∈ s_better
D : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, F) (f_local x) := mfderiv 𝓘(ℝ, E) 𝓘(ℝ, F) f_local x
A : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace I (↑(e.extend I).symm x) := mfderiv 𝓘(ℝ, E) I (↑(e.extend I).symm) x
B : TangentSpace I (↑(e.extend I).symm x) →L[ℝ] TangentSpace J (f (↑(e.extend I).symm x)) :=
  mfderiv I J f (↑(e.extend I).symm x)
C : TangentSpace J ((f ∘ ↑(e.extend I).symm) x) →L[ℝ]
  TangentSpace 𝓘(ℝ, F) (↑(e'.extend J) ((f ∘ ↑(e.extend I).symm) x)) :=
  mfderiv J 𝓘(ℝ, F) (↑(e'.extend J)) ((f ∘ ↑(e.extend I).symm) x)
hnA : ↑(e.extend I) '' e.source ∈ 𝓝 x
hr : 1 ≤ ↑r
he : e ∈ maximalAtlas I M
this✝ : ↑I '' e.target ∈ 𝓝 x
hA : MDifferentiableAt 𝓘(ℝ, E) I (e.invFun ∘ I.invFun) x
hB : MDifferentiableAt I J f ((e.invFun ∘ I.invFun) x)
hBA : MDifferentiableAt 𝓘(ℝ, E) J (f ∘ e.invFun ∘ I.invFun) x
hnC : f ∘ e.invFun ∘ I.invFun '' w ∈ 𝓝 ((f ∘ e.invFun ∘ I.invFun) x)
this : ContMDiffOn J 𝓘(ℝ, F) ⊤ (↑J ∘ ↑e') e'.source
⊢ MDifferentiableAt J 𝓘(ℝ, F) (↑J ∘ ↑e') ((f ∘ e.invFun ∘ I.invFun) x)
Tactic:
exact SmoothAt.mdifferentiableAt ((this.mono hw).contMDiffAt hnC)
Proof state after:
no goals
Theorem: sard
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
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:
sorry
Proof state after:
no goals
Theorem: sard'
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✝¹ : T2Space N
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hs : IsClosed s
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
⊢ IsMeagre (f '' s)
Tactic:
have : LocallyCompactSpace M := Manifold.locallyCompact_of_finiteDimensional I
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✝¹ : T2Space N
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hs : IsClosed s
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
this : LocallyCompactSpace M
⊢ IsMeagre (f '' s)
Theorem: sard'
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✝¹ : T2Space N
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hs : IsClosed s
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
this : LocallyCompactSpace M
⊢ IsMeagre (f '' s)
Tactic:
have : IsSigmaCompact s := isSigmaCompact_univ.of_isClosed_subset hs (subset_univ 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✝¹ : T2Space N
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hs : IsClosed s
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
this✝ : LocallyCompactSpace M
this : IsSigmaCompact s
⊢ IsMeagre (f '' s)
Theorem: sard'
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✝¹ : T2Space N
inst✝ : J.Boundaryless
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hs : IsClosed s
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
this✝ : LocallyCompactSpace M
this : IsSigmaCompact s
⊢ IsMeagre (f '' s)
Tactic:
exact MeasureZero.isMeagre_of_isSigmaCompact J (sard I hf hf' h'f') (this.image (hf.continuous))
Proof state after:
no goals
Theorem: MeasureZero.mono
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s t : Set M
hst : s ⊆ t
ht : MeasureZero I t
⊢ MeasureZero I s
Tactic:
intro μ 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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s t : Set M
hst : s ⊆ t
ht : MeasureZero I t
μ : Measure E
hμ : μ.IsAddHaarMeasure
x : M
⊢ ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ s)) = 0
Theorem: MeasureZero.mono
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s t : Set M
hst : s ⊆ t
ht : MeasureZero I t
μ : Measure E
hμ : μ.IsAddHaarMeasure
x : M
⊢ ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ s)) = 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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s t : Set M
hst : s ⊆ t
ht : MeasureZero I t
μ : Measure E
hμ : μ.IsAddHaarMeasure
x : M
e : PartialHomeomorph M H := chartAt H x
⊢ ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ s)) = 0
Theorem: MeasureZero.mono
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s t : Set M
hst : s ⊆ t
ht : MeasureZero I t
μ : Measure E
hμ : μ.IsAddHaarMeasure
x : M
e : PartialHomeomorph M H := chartAt H x
⊢ ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ s)) = 0
Tactic:
have : I ∘ e '' (e.source ∩ s) ⊆  I ∘ e '' (e.source ∩ t) := by
  apply image_subset
  exact inter_subset_inter_right e.source hst
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s t : Set M
hst : s ⊆ t
ht : MeasureZero I t
μ : Measure E
hμ : μ.IsAddHaarMeasure
x : M
e : PartialHomeomorph M H := chartAt H x
this : ↑I ∘ ↑e '' (e.source ∩ s) ⊆ ↑I ∘ ↑e '' (e.source ∩ t)
⊢ ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ s)) = 0
Theorem: MeasureZero.mono
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s t : Set M
hst : s ⊆ t
ht : MeasureZero I t
μ : Measure E
hμ : μ.IsAddHaarMeasure
x : M
e : PartialHomeomorph M H := chartAt H x
this : ↑I ∘ ↑e '' (e.source ∩ s) ⊆ ↑I ∘ ↑e '' (e.source ∩ t)
⊢ ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ s)) = 0
Tactic:
exact measure_mono_null this (ht μ x)
Proof state after:
no goals
Theorem: MeasureZero.mono
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s t : Set M
hst : s ⊆ t
ht : MeasureZero I t
μ : Measure E
hμ : μ.IsAddHaarMeasure
x : M
e : PartialHomeomorph M H := chartAt H x
⊢ ↑I ∘ ↑e '' (e.source ∩ s) ⊆ ↑I ∘ ↑e '' (e.source ∩ t)
Tactic:
apply image_subset
Proof state after:
case h
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s t : Set M
hst : s ⊆ t
ht : MeasureZero I t
μ : Measure E
hμ : μ.IsAddHaarMeasure
x : M
e : PartialHomeomorph M H := chartAt H x
⊢ e.source ∩ s ⊆ e.source ∩ t
Theorem: MeasureZero.mono
Proof state before:
case h
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s t : Set M
hst : s ⊆ t
ht : MeasureZero I t
μ : Measure E
hμ : μ.IsAddHaarMeasure
x : M
e : PartialHomeomorph M H := chartAt H x
⊢ e.source ∩ s ⊆ e.source ∩ t
Tactic:
exact inter_subset_inter_right e.source hst
Proof state after:
no goals
Theorem: MeasureZero.empty
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
⊢ MeasureZero I ∅
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✝⁴ : I.Boundaryless
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : M
⊢ ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ ∅)) = 0
Theorem: MeasureZero.empty
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✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : M
⊢ ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ ∅)) = 0
Tactic:
simp only [comp_apply, inter_empty, image_empty, OuterMeasure.empty']
Proof state after:
no goals
Theorem: MeasureZero.iUnion
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✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
ι : Type u_4
inst✝ : Encodable ι
s : ι → Set M
hs : ∀ (n : ι), MeasureZero I (s n)
⊢ MeasureZero I (⋃ n, s n)
Tactic:
intro μ 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✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
ι : Type u_4
inst✝ : Encodable ι
s : ι → Set M
hs : ∀ (n : ι), MeasureZero I (s n)
μ : Measure E
hμ : μ.IsAddHaarMeasure
x : M
⊢ ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ ⋃ n, s n)) = 0
Theorem: MeasureZero.iUnion
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✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
ι : Type u_4
inst✝ : Encodable ι
s : ι → Set M
hs : ∀ (n : ι), MeasureZero I (s n)
μ : Measure E
hμ : μ.IsAddHaarMeasure
x : M
⊢ ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ ⋃ n, s n)) = 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✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
ι : Type u_4
inst✝ : Encodable ι
s : ι → Set M
hs : ∀ (n : ι), MeasureZero I (s n)
μ : Measure E
hμ : μ.IsAddHaarMeasure
x : M
e : PartialHomeomorph M H := chartAt H x
⊢ ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ ⋃ n, s n)) = 0
Theorem: MeasureZero.iUnion
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✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
ι : Type u_4
inst✝ : Encodable ι
s : ι → Set M
hs : ∀ (n : ι), MeasureZero I (s n)
μ : Measure E
hμ : μ.IsAddHaarMeasure
x : M
e : PartialHomeomorph M H := chartAt H x
⊢ ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ ⋃ n, s n)) = 0
Tactic:
have : I ∘ e '' (e.source ∩ (⋃ (n : ι),  s n)) = ⋃ (n : ι), I ∘ e '' (e.source ∩ s n) := by
  rw [inter_iUnion]
  exact image_iUnion
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✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
ι : Type u_4
inst✝ : Encodable ι
s : ι → Set M
hs : ∀ (n : ι), MeasureZero I (s n)
μ : Measure E
hμ : μ.IsAddHaarMeasure
x : M
e : PartialHomeomorph M H := chartAt H x
this : ↑I ∘ ↑e '' (e.source ∩ ⋃ n, s n) = ⋃ n, ↑I ∘ ↑e '' (e.source ∩ s n)
⊢ ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ ⋃ n, s n)) = 0
Theorem: MeasureZero.iUnion
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✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
ι : Type u_4
inst✝ : Encodable ι
s : ι → Set M
hs : ∀ (n : ι), MeasureZero I (s n)
μ : Measure E
hμ : μ.IsAddHaarMeasure
x : M
e : PartialHomeomorph M H := chartAt H x
this : ↑I ∘ ↑e '' (e.source ∩ ⋃ n, s n) = ⋃ n, ↑I ∘ ↑e '' (e.source ∩ s n)
⊢ ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ ⋃ n, s n)) = 0
Tactic:
simp_all only [comp_apply, OuterMeasure.iUnion_null_iff]
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✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
ι : Type u_4
inst✝ : Encodable ι
s : ι → Set M
hs : ∀ (n : ι), MeasureZero I (s n)
μ : Measure E
hμ : μ.IsAddHaarMeasure
x : M
e : PartialHomeomorph M H := chartAt H x
this : (fun a => ↑I (↑e a)) '' (e.source ∩ ⋃ n, s n) = ⋃ n, (fun a => ↑I (↑e a)) '' (e.source ∩ s n)
⊢ ∀ (i : ι), ↑μ ((fun a => ↑I (↑e a)) '' (e.source ∩ s i)) = 0
Theorem: MeasureZero.iUnion
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✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
ι : Type u_4
inst✝ : Encodable ι
s : ι → Set M
hs : ∀ (n : ι), MeasureZero I (s n)
μ : Measure E
hμ : μ.IsAddHaarMeasure
x : M
e : PartialHomeomorph M H := chartAt H x
this : (fun a => ↑I (↑e a)) '' (e.source ∩ ⋃ n, s n) = ⋃ n, (fun a => ↑I (↑e a)) '' (e.source ∩ s n)
⊢ ∀ (i : ι), ↑μ ((fun a => ↑I (↑e a)) '' (e.source ∩ s i)) = 0
Tactic:
intro i
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✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
ι : Type u_4
inst✝ : Encodable ι
s : ι → Set M
hs : ∀ (n : ι), MeasureZero I (s n)
μ : Measure E
hμ : μ.IsAddHaarMeasure
x : M
e : PartialHomeomorph M H := chartAt H x
this : (fun a => ↑I (↑e a)) '' (e.source ∩ ⋃ n, s n) = ⋃ n, (fun a => ↑I (↑e a)) '' (e.source ∩ s n)
i : ι
⊢ ↑μ ((fun a => ↑I (↑e a)) '' (e.source ∩ s i)) = 0
Theorem: MeasureZero.iUnion
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✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
ι : Type u_4
inst✝ : Encodable ι
s : ι → Set M
hs : ∀ (n : ι), MeasureZero I (s n)
μ : Measure E
hμ : μ.IsAddHaarMeasure
x : M
e : PartialHomeomorph M H := chartAt H x
this : (fun a => ↑I (↑e a)) '' (e.source ∩ ⋃ n, s n) = ⋃ n, (fun a => ↑I (↑e a)) '' (e.source ∩ s n)
i : ι
⊢ ↑μ ((fun a => ↑I (↑e a)) '' (e.source ∩ s i)) = 0
Tactic:
apply hs
Proof state after:
no goals