Theorem: MeasureZero.iUnion (Sard/MeasureZero.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✝⁴ : 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
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

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

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

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

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

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

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 ∘ ↑e '' (e.source ∩ ⋃ n, s n) = ⋃ n, ↑I ∘ ↑e '' (e.source ∩ s n)
Tactic:
rw [inter_iUnion]
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 ∘ ↑e '' ⋃ i, e.source ∩ s i = ⋃ n, ↑I ∘ ↑e '' (e.source ∩ s n)

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 ∘ ↑e '' ⋃ i, e.source ∩ s i = ⋃ n, ↑I ∘ ↑e '' (e.source ∩ s n)
Tactic:
exact image_iUnion
State after:
no goals