α : Type u_1
β : Type ?u.278939
γ : Type ?u.278942
δ : Type ?u.278945
ι : Type ?u.278948
R : Type ?u.278951
R' : Type ?u.278954
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s'✝ t✝ : Set α
ht : NullMeasurableSet t✝
s' : Set α
hs' : MeasurableSet s'
t : Set α
⊢ ↑↑μ (s ∩ t) = ↑↑μ (s ∩ t ∩ s') + ↑↑μ ((s ∩ t) \ s')
α : Type u_1
β : Type ?u.278939
γ : Type ?u.278942
δ : Type ?u.278945
ι : Type ?u.278948
R : Type ?u.278951
R' : Type ?u.278954
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s'✝ t✝ : Set α
ht : NullMeasurableSet t✝
s' : Set α
hs' : MeasurableSet s'
t : Set α
⊢ ↑(↑(OuterMeasure.restrict s) ↑μ) t =
    ↑(↑(OuterMeasure.restrict s) ↑μ) (t ∩ s') + ↑(↑(OuterMeasure.restrict s) ↑μ) (t \ s')
suffices μ (s ∩ t) = μ (s ∩ t ∩ s') + μ ((s ∩ t) \ s') by
  simpa [← Set.inter_assoc, Set.inter_comm _ s, ← inter_diff_assoc]
no goals
α : Type u_1
β : Type ?u.278939
γ : Type ?u.278942
δ : Type ?u.278945
ι : Type ?u.278948
R : Type ?u.278951
R' : Type ?u.278954
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s'✝ t✝ : Set α
ht : NullMeasurableSet t✝
s' : Set α
hs' : MeasurableSet s'
t : Set α
⊢ ↑↑μ (s ∩ t) = ↑↑μ (s ∩ t ∩ s') + ↑↑μ ((s ∩ t) \ s')
exact le_toOuterMeasure_caratheodory _ _ hs' _
no goals
α : Type u_1
β : Type ?u.278939
γ : Type ?u.278942
δ : Type ?u.278945
ι : Type ?u.278948
R : Type ?u.278951
R' : Type ?u.278954
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s'✝ t✝ : Set α
ht : NullMeasurableSet t✝
s' : Set α
hs' : MeasurableSet s'
t : Set α
this : ↑↑μ (s ∩ t) = ↑↑μ (s ∩ t ∩ s') + ↑↑μ ((s ∩ t) \ s')
⊢ ↑(↑(OuterMeasure.restrict s) ↑μ) t =
    ↑(↑(OuterMeasure.restrict s) ↑μ) (t ∩ s') + ↑(↑(OuterMeasure.restrict s) ↑μ) (t \ s')
simpa [← Set.inter_assoc, Set.inter_comm _ s, ← inter_diff_assoc]
no goals
α : Type u_1
β : Type ?u.278939
γ : Type ?u.278942
δ : Type ?u.278945
ι : Type ?u.278948
R : Type ?u.278951
R' : Type ?u.278954
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
ht : NullMeasurableSet t
⊢ ↑(↑(OuterMeasure.restrict s) ↑μ) t = ↑↑μ (t ∩ s)
simp only [OuterMeasure.restrict_apply]