α : Type u_1
β : Type u_2
R : Type ?u.7093
R' : Type ?u.7096
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : Set β
hs : Set.Countable s
t : β → Set α
this : Encodable ↑s
⊢ ↑m (⋃ (i : β) (_ : i ∈ s), t i) = 0 ↔ ∀ (i : β), i ∈ s → ↑m (t i) = 0
α : Type u_1
β : Type u_2
R : Type ?u.7093
R' : Type ?u.7096
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : Set β
hs : Set.Countable s
t : β → Set α
⊢ ↑m (⋃ (i : β) (_ : i ∈ s), t i) = 0 ↔ ∀ (i : β), i ∈ s → ↑m (t i) = 0
haveI := hs.toEncodable
no goals
α : Type u_1
β : Type u_2
R : Type ?u.7093
R' : Type ?u.7096
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : Set β
hs : Set.Countable s
t : β → Set α
this : Encodable ↑s
⊢ ↑m (⋃ (i : β) (_ : i ∈ s), t i) = 0 ↔ ∀ (i : β), i ∈ s → ↑m (t i) = 0
rw [biUnion_eq_iUnion, iUnion_null_iff, SetCoe.forall']