Theorem: MeasureZero.union (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
hs : MeasureZero I s
ht : MeasureZero I t
⊢ MeasureZero I (s ∪ t)
Tactic:
let u : Bool → Set M := fun b ↦ cond b s t
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
hs : MeasureZero I s
ht : MeasureZero I t
u : Bool → Set M := fun b => bif b then s else t
⊢ MeasureZero I (s ∪ t)

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
hs : MeasureZero I s
ht : MeasureZero I t
u : Bool → Set M := fun b => bif b then s else t
this : ∀ (i : Bool), MeasureZero I (u i)
⊢ MeasureZero I (s ∪ t)
Tactic:
rw [union_eq_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
s t : Set M
hs : MeasureZero I s
ht : MeasureZero I t
u : Bool → Set M := fun b => bif b then s else t
this : ∀ (i : Bool), MeasureZero I (u i)
⊢ MeasureZero I (⋃ b, bif b then s else t)

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
hs : MeasureZero I s
ht : MeasureZero I t
u : Bool → Set M := fun b => bif b then s else t
this : ∀ (i : Bool), MeasureZero I (u i)
⊢ MeasureZero I (⋃ b, bif b then s else t)
Tactic:
exact MeasureZero.iUnion this
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
hs : MeasureZero I s
ht : MeasureZero I t
u : Bool → Set M := fun b => bif b then s else t
⊢ ∀ (i : Bool), MeasureZero I (u i)
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
s t : Set M
hs : MeasureZero I s
ht : MeasureZero I t
u : Bool → Set M := fun b => bif b then s else t
i : Bool
⊢ MeasureZero I (u i)

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
hs : MeasureZero I s
ht : MeasureZero I t
u : Bool → Set M := fun b => bif b then s else t
i : Bool
⊢ MeasureZero I (u i)
Tactic:
cases i
State after:
case false
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
hs : MeasureZero I s
ht : MeasureZero I t
u : Bool → Set M := fun b => bif b then s else t
⊢ MeasureZero I (u false)

case true
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
hs : MeasureZero I s
ht : MeasureZero I t
u : Bool → Set M := fun b => bif b then s else t
⊢ MeasureZero I (u true)

State before:
case false
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
hs : MeasureZero I s
ht : MeasureZero I t
u : Bool → Set M := fun b => bif b then s else t
⊢ MeasureZero I (u false)
Tactic:
exact ht
State after:
no goals

State before:
case true
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
hs : MeasureZero I s
ht : MeasureZero I t
u : Bool → Set M := fun b => bif b then s else t
⊢ MeasureZero I (u true)
Tactic:
exact hs
State after:
no goals