α : Type u
β : Type v
γ : Type w
ι : Sort x
t : ι → Set α
inst✝ : Countable ι
ht : ∀ (i : ι), Set.Countable (t i)
this : ∀ (a : ι), Countable ↑(t a)
⊢ Set.Countable (⋃ (i : ι), t i)
α : Type u
β : Type v
γ : Type w
ι : Sort x
t : ι → Set α
inst✝ : Countable ι
ht : ∀ (i : ι), Set.Countable (t i)
⊢ Set.Countable (⋃ (i : ι), t i)
haveI := fun a => (ht a).to_subtype
α : Type u
β : Type v
γ : Type w
ι : Sort x
t : ι → Set α
inst✝ : Countable ι
ht : ∀ (i : ι), Set.Countable (t i)
this : ∀ (a : ι), Countable ↑(t a)
⊢ Set.Countable (range fun a => ↑a.snd)
α : Type u
β : Type v
γ : Type w
ι : Sort x
t : ι → Set α
inst✝ : Countable ι
ht : ∀ (i : ι), Set.Countable (t i)
this : ∀ (a : ι), Countable ↑(t a)
⊢ Set.Countable (⋃ (i : ι), t i)
rw [iUnion_eq_range_psigma]
no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
t : ι → Set α
inst✝ : Countable ι
ht : ∀ (i : ι), Set.Countable (t i)
this : ∀ (a : ι), Countable ↑(t a)
⊢ Set.Countable (range fun a => ↑a.snd)
apply countable_range