α : Type u_1
β : Type ?u.558165
γ : Type ?u.558168
δ : Type ?u.558171
ι : Type u_2
R : Type ?u.558177
R' : Type ?u.558180
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
s : ι → Set α
t : Set ι
ht : Set.Countable t
this : Countable ↑t
⊢ ae (Measure.restrict μ (⋃ (i : ι) (_ : i ∈ t), s i)) = ⨆ (i : ι) (_ : i ∈ t), ae (Measure.restrict μ (s i))
α : Type u_1
β : Type ?u.558165
γ : Type ?u.558168
δ : Type ?u.558171
ι : Type u_2
R : Type ?u.558177
R' : Type ?u.558180
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
s : ι → Set α
t : Set ι
ht : Set.Countable t
⊢ ae (Measure.restrict μ (⋃ (i : ι) (_ : i ∈ t), s i)) = ⨆ (i : ι) (_ : i ∈ t), ae (Measure.restrict μ (s i))
haveI := ht.to_subtype
no goals
α : Type u_1
β : Type ?u.558165
γ : Type ?u.558168
δ : Type ?u.558171
ι : Type u_2
R : Type ?u.558177
R' : Type ?u.558180
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
s : ι → Set α
t : Set ι
ht : Set.Countable t
this : Countable ↑t
⊢ ae (Measure.restrict μ (⋃ (i : ι) (_ : i ∈ t), s i)) = ⨆ (i : ι) (_ : i ∈ t), ae (Measure.restrict μ (s i))
rw [biUnion_eq_iUnion, ae_restrict_iUnion_eq, ← iSup_subtype'']