α : Type u_1
β : Type u_2
γ : Type ?u.4604
δ : Type ?u.4607
δ' : Type ?u.4610
ι : Sort ?u.4613
s✝ t u : Set α
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : Set.Countable s
h : ∀ (b : β), b ∈ s → MeasurableSet (f b)
⊢ MeasurableSet (⋃ (x : ↑s), f ↑x)
α : Type u_1
β : Type u_2
γ : Type ?u.4604
δ : Type ?u.4607
δ' : Type ?u.4610
ι : Sort ?u.4613
s✝ t u : Set α
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : Set.Countable s
h : ∀ (b : β), b ∈ s → MeasurableSet (f b)
⊢ MeasurableSet (⋃ (b : β) (_ : b ∈ s), f b)
rw [biUnion_eq_iUnion]
α : Type u_1
β : Type u_2
γ : Type ?u.4604
δ : Type ?u.4607
δ' : Type ?u.4610
ι : Sort ?u.4613
s✝ t u : Set α
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : Set.Countable s
h : ∀ (b : β), b ∈ s → MeasurableSet (f b)
this : Countable ↑s
⊢ MeasurableSet (⋃ (x : ↑s), f ↑x)
α : Type u_1
β : Type u_2
γ : Type ?u.4604
δ : Type ?u.4607
δ' : Type ?u.4610
ι : Sort ?u.4613
s✝ t u : Set α
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : Set.Countable s
h : ∀ (b : β), b ∈ s → MeasurableSet (f b)
⊢ MeasurableSet (⋃ (x : ↑s), f ↑x)
have := hs.to_subtype
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.4604
δ : Type ?u.4607
δ' : Type ?u.4610
ι : Sort ?u.4613
s✝ t u : Set α
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : Set.Countable s
h : ∀ (b : β), b ∈ s → MeasurableSet (f b)
this : Countable ↑s
⊢ MeasurableSet (⋃ (x : ↑s), f ↑x)
exact MeasurableSet.iUnion (by simpa using h)
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.4604
δ : Type ?u.4607
δ' : Type ?u.4610
ι : Sort ?u.4613
s✝ t u : Set α
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : Set.Countable s
h : ∀ (b : β), b ∈ s → MeasurableSet (f b)
this : Countable ↑s
⊢ ∀ (b : ↑s), MeasurableSet (f ↑b)
simpa using h