α : Type u_2
β : Type ?u.304451
γ : Type ?u.304454
δ : Type ?u.304457
ι : Type u_1
R : Type ?u.304463
R' : Type ?u.304466
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
inst✝ : Countable ι
s : ι → Set α
hd : Directed (fun x x_1 => x ⊆ x_1) s
t : Set α
ht : MeasurableSet t
⊢ ↑↑μ (⋃ (i : ι), t ∩ s i) = ⨆ (i : ι), ↑↑μ (t ∩ s i)
α : Type u_2
β : Type ?u.304451
γ : Type ?u.304454
δ : Type ?u.304457
ι : Type u_1
R : Type ?u.304463
R' : Type ?u.304466
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
inst✝ : Countable ι
s : ι → Set α
hd : Directed (fun x x_1 => x ⊆ x_1) s
t : Set α
ht : MeasurableSet t
⊢ ↑↑(restrict μ (⋃ (i : ι), s i)) t = ⨆ (i : ι), ↑↑(restrict μ (s i)) t
simp only [restrict_apply ht, inter_iUnion]
α : Type u_2
β : Type ?u.304451
γ : Type ?u.304454
δ : Type ?u.304457
ι : Type u_1
R : Type ?u.304463
R' : Type ?u.304466
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
inst✝ : Countable ι
s : ι → Set α
hd : Directed (fun x x_1 => x ⊆ x_1) s
t : Set α
ht : MeasurableSet t
⊢ Directed (fun x x_1 => x ⊆ x_1) fun i => t ∩ s i
α : Type u_2
β : Type ?u.304451
γ : Type ?u.304454
δ : Type ?u.304457
ι : Type u_1
R : Type ?u.304463
R' : Type ?u.304466
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
inst✝ : Countable ι
s : ι → Set α
hd : Directed (fun x x_1 => x ⊆ x_1) s
t : Set α
ht : MeasurableSet t
⊢ ↑↑μ (⋃ (i : ι), t ∩ s i) = ⨆ (i : ι), ↑↑μ (t ∩ s i)
rw [measure_iUnion_eq_iSup]
no goals
α : Type u_2
β : Type ?u.304451
γ : Type ?u.304454
δ : Type ?u.304457
ι : Type u_1
R : Type ?u.304463
R' : Type ?u.304466
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
inst✝ : Countable ι
s : ι → Set α
hd : Directed (fun x x_1 => x ⊆ x_1) s
t : Set α
ht : MeasurableSet t
⊢ Directed (fun x x_1 => x ⊆ x_1) fun i => t ∩ s i
exacts [hd.mono_comp _ fun s₁ s₂ => inter_subset_inter_right _]