α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → Finset β
h : Set.Finite (range f)
⊢ Set.Finite (⋃ (x : Finset β) (_ : x ∈ range fun a => f a), ↑x)
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → Finset β
h : Set.Finite (range f)
⊢ Set.Finite (⋃ (a : α), ↑(f a))
rw [← biUnion_range]
no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → Finset β
h : Set.Finite (range f)
⊢ Set.Finite (⋃ (x : Finset β) (_ : x ∈ range fun a => f a), ↑x)
exact h.biUnion fun y _ => y.finite_toSet