α : Type u_1
β : Type ?u.578132
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : restrict v i ≤ restrict w i
hj₁ : MeasurableSet j
hj₂ : restrict v j ≤ restrict w j
⊢ restrict v (⋃ (b : Bool), bif b then i else j) ≤ restrict w (⋃ (b : Bool), bif b then i else j)
α : Type u_1
β : Type ?u.578132
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : restrict v i ≤ restrict w i
hj₁ : MeasurableSet j
hj₂ : restrict v j ≤ restrict w j
⊢ restrict v (i ∪ j) ≤ restrict w (i ∪ j)
rw [Set.union_eq_iUnion]
case refine'_1
α : Type u_1
β : Type ?u.578132
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : restrict v i ≤ restrict w i
hj₁ : MeasurableSet j
hj₂ : restrict v j ≤ restrict w j
⊢ ∀ (b : Bool), MeasurableSet (bif b then i else j)

case refine'_2
α : Type u_1
β : Type ?u.578132
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : restrict v i ≤ restrict w i
hj₁ : MeasurableSet j
hj₂ : restrict v j ≤ restrict w j
⊢ ∀ (b : Bool), restrict v (bif b then i else j) ≤ restrict w (bif b then i else j)
α : Type u_1
β : Type ?u.578132
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : restrict v i ≤ restrict w i
hj₁ : MeasurableSet j
hj₂ : restrict v j ≤ restrict w j
⊢ restrict v (⋃ (b : Bool), bif b then i else j) ≤ restrict w (⋃ (b : Bool), bif b then i else j)
refine' restrict_le_restrict_countable_iUnion v w _ _
no goals
case refine'_1
α : Type u_1
β : Type ?u.578132
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : restrict v i ≤ restrict w i
hj₁ : MeasurableSet j
hj₂ : restrict v j ≤ restrict w j
⊢ ∀ (b : Bool), MeasurableSet (bif b then i else j)
measurability
no goals
case refine'_2
α : Type u_1
β : Type ?u.578132
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : restrict v i ≤ restrict w i
hj₁ : MeasurableSet j
hj₂ : restrict v j ≤ restrict w j
⊢ ∀ (b : Bool), restrict v (bif b then i else j) ≤ restrict w (bif b then i else j)
rintro (_ | _) <;> simpa