α : Type u_1
β : Type ?u.52533
γ : Type ?u.52536
δ : Type ?u.52539
ι : Type u_2
R : Type ?u.52545
R' : Type ?u.52548
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
s : ι → Set α
t : Set ι
ht : Set.Countable t
hd : DirectedOn ((fun x x_1 => x ⊆ x_1) on s) t
this : Encodable ↑t
⊢ ↑↑μ (⋃ (i : ι) (_ : i ∈ t), s i) = ⨆ (i : ι) (_ : i ∈ t), ↑↑μ (s i)
α : Type u_1
β : Type ?u.52533
γ : Type ?u.52536
δ : Type ?u.52539
ι : Type u_2
R : Type ?u.52545
R' : Type ?u.52548
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
s : ι → Set α
t : Set ι
ht : Set.Countable t
hd : DirectedOn ((fun x x_1 => x ⊆ x_1) on s) t
⊢ ↑↑μ (⋃ (i : ι) (_ : i ∈ t), s i) = ⨆ (i : ι) (_ : i ∈ t), ↑↑μ (s i)
haveI := ht.toEncodable
no goals
α : Type u_1
β : Type ?u.52533
γ : Type ?u.52536
δ : Type ?u.52539
ι : Type u_2
R : Type ?u.52545
R' : Type ?u.52548
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
s : ι → Set α
t : Set ι
ht : Set.Countable t
hd : DirectedOn ((fun x x_1 => x ⊆ x_1) on s) t
this : Encodable ↑t
⊢ ↑↑μ (⋃ (i : ι) (_ : i ∈ t), s i) = ⨆ (i : ι) (_ : i ∈ t), ↑↑μ (s i)
rw [biUnion_eq_iUnion, measure_iUnion_eq_iSup hd.directed_val, ← iSup_subtype'']