case inl
α : Type u_2
β : Type ?u.3894
γ : Type ?u.3897
δ : Type ?u.3900
δ' : Type ?u.3903
ι : Sort u_1
s t u : Set α
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h✝ : IsEmpty ι
⊢ MeasurableSet (⋃ (b : ι), f b)

case inr
α : Type u_2
β : Type ?u.3894
γ : Type ?u.3897
δ : Type ?u.3900
δ' : Type ?u.3903
ι : Sort u_1
s t u : Set α
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h✝ : Nonempty ι
⊢ MeasurableSet (⋃ (b : ι), f b)
α : Type u_2
β : Type ?u.3894
γ : Type ?u.3897
δ : Type ?u.3900
δ' : Type ?u.3903
ι : Sort u_1
s t u : Set α
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
⊢ MeasurableSet (⋃ (b : ι), f b)
cases isEmpty_or_nonempty ι
no goals
case inl
α : Type u_2
β : Type ?u.3894
γ : Type ?u.3897
δ : Type ?u.3900
δ' : Type ?u.3903
ι : Sort u_1
s t u : Set α
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h✝ : IsEmpty ι
⊢ MeasurableSet (⋃ (b : ι), f b)
simp
case inr.intro
α : Type u_2
β : Type ?u.3894
γ : Type ?u.3897
δ : Type ?u.3900
δ' : Type ?u.3903
ι : Sort u_1
s t u : Set α
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h✝ : Nonempty ι
e : ℕ → ι
he : Surjective e
⊢ MeasurableSet (⋃ (b : ι), f b)
case inr
α : Type u_2
β : Type ?u.3894
γ : Type ?u.3897
δ : Type ?u.3900
δ' : Type ?u.3903
ι : Sort u_1
s t u : Set α
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h✝ : Nonempty ι
⊢ MeasurableSet (⋃ (b : ι), f b)
rcases exists_surjective_nat ι with ⟨e, he⟩
case inr.intro
α : Type u_2
β : Type ?u.3894
γ : Type ?u.3897
δ : Type ?u.3900
δ' : Type ?u.3903
ι : Sort u_1
s t u : Set α
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h✝ : Nonempty ι
e : ℕ → ι
he : Surjective e
⊢ MeasurableSet (⋃ (x : ℕ), f (e x))
case inr.intro
α : Type u_2
β : Type ?u.3894
γ : Type ?u.3897
δ : Type ?u.3900
δ' : Type ?u.3903
ι : Sort u_1
s t u : Set α
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h✝ : Nonempty ι
e : ℕ → ι
he : Surjective e
⊢ MeasurableSet (⋃ (b : ι), f b)
rw [← iUnion_congr_of_surjective _ he (fun _ => rfl)]
no goals
case inr.intro
α : Type u_2
β : Type ?u.3894
γ : Type ?u.3897
δ : Type ?u.3900
δ' : Type ?u.3903
ι : Sort u_1
s t u : Set α
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h✝ : Nonempty ι
e : ℕ → ι
he : Surjective e
⊢ MeasurableSet (⋃ (x : ℕ), f (e x))
exact m.measurableSet_iUnion _ fun _ => h _