α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
t : (a : α) → a ∈ s → Set β
hs : Set.Countable s
this : Countable ↑s
⊢ Set.Countable (⋃ (a : α) (h : a ∈ s), t a h) ↔ ∀ (a : α) (ha : a ∈ s), Set.Countable (t a ha)
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
t : (a : α) → a ∈ s → Set β
hs : Set.Countable s
⊢ Set.Countable (⋃ (a : α) (h : a ∈ s), t a h) ↔ ∀ (a : α) (ha : a ∈ s), Set.Countable (t a ha)
haveI := hs.to_subtype
no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
t : (a : α) → a ∈ s → Set β
hs : Set.Countable s
this : Countable ↑s
⊢ Set.Countable (⋃ (a : α) (h : a ∈ s), t a h) ↔ ∀ (a : α) (ha : a ∈ s), Set.Countable (t a ha)
rw [biUnion_eq_iUnion, countable_iUnion_iff, SetCoe.forall']