α : Type u_1
β : Type ?u.36188
γ : Type ?u.36191
δ : Type ?u.36194
ι : Type ?u.36197
R : Type ?u.36200
R' : Type ?u.36203
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : ↑↑μ s₂ ≤ ↑↑μ s₁
ht : t₁ ⊆ t₂
htμ : ↑↑μ t₂ ≤ ↑↑μ t₁
⊢ ↑↑μ (⋃ (b : Bool), bif b then s₁ else t₁) = ↑↑μ (⋃ (b : Bool), bif b then s₂ else t₂)
α : Type u_1
β : Type ?u.36188
γ : Type ?u.36191
δ : Type ?u.36194
ι : Type ?u.36197
R : Type ?u.36200
R' : Type ?u.36203
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : ↑↑μ s₂ ≤ ↑↑μ s₁
ht : t₁ ⊆ t₂
htμ : ↑↑μ t₂ ≤ ↑↑μ t₁
⊢ ↑↑μ (s₁ ∪ t₁) = ↑↑μ (s₂ ∪ t₂)
rw [union_eq_iUnion, union_eq_iUnion]
no goals
α : Type u_1
β : Type ?u.36188
γ : Type ?u.36191
δ : Type ?u.36194
ι : Type ?u.36197
R : Type ?u.36200
R' : Type ?u.36203
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : ↑↑μ s₂ ≤ ↑↑μ s₁
ht : t₁ ⊆ t₂
htμ : ↑↑μ t₂ ≤ ↑↑μ t₁
⊢ ↑↑μ (⋃ (b : Bool), bif b then s₁ else t₁) = ↑↑μ (⋃ (b : Bool), bif b then s₂ else t₂)
exact measure_iUnion_congr_of_subset (Bool.forall_bool.2 ⟨ht, hs⟩) (Bool.forall_bool.2 ⟨htμ, hsμ⟩)