α : Type u_1
β : Type ?u.69435
R : Type ?u.69438
R' : Type ?u.69441
ms : Set (OuterMeasure α)
m m₁ m₂ : OuterMeasure α
s : Set α
this : ↑(⨆ (i : Bool), bif i then m₁ else m₂) s = ⨆ (i : Bool), ↑(bif i then m₁ else m₂) s
⊢ ↑(m₁ ⊔ m₂) s = ↑m₁ s ⊔ ↑m₂ s
α : Type u_1
β : Type ?u.69435
R : Type ?u.69438
R' : Type ?u.69441
ms : Set (OuterMeasure α)
m m₁ m₂ : OuterMeasure α
s : Set α
⊢ ↑(m₁ ⊔ m₂) s = ↑m₁ s ⊔ ↑m₂ s
have := iSup_apply (fun b => cond b m₁ m₂) s
no goals
α : Type u_1
β : Type ?u.69435
R : Type ?u.69438
R' : Type ?u.69441
ms : Set (OuterMeasure α)
m m₁ m₂ : OuterMeasure α
s : Set α
this : ↑(⨆ (i : Bool), bif i then m₁ else m₂) s = ⨆ (i : Bool), ↑(bif i then m₁ else m₂) s
⊢ ↑(m₁ ⊔ m₂) s = ↑m₁ s ⊔ ↑m₂ s
rwa [iSup_bool_eq, iSup_bool_eq] at this