Theorem: MeasureZero.mono (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
s t : Set M
hst : s ⊆ t
ht : MeasureZero I t
⊢ MeasureZero I s
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
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

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

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

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

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