Finiteness of sigma types

instance Finite.instSigma {α : Type u_1} {β : α → Type u_2} [Finite α] [∀ (a : α), Finite (β a)] : Finite ((a : α) × β a)

instance Finite.instPSigma {ι : Sort u_3} {π : ι → Sort u_4} [Finite ι] [∀ (i : ι), Finite (π i)] : Finite ((i : ι) ×' π i)

instance Finite.Set.finite_sigma {α : Type u_1} {β : α → Type u_2} (s : Set α) (t : (i : α) → Set (β i)) [Finite ↑s] [∀ (i : α), Finite ↑(t i)] : Finite ↑(s.sigma t)

theorem Set.Finite.sigma {α : Type u_1} {β : α → Type u_2} {s : Set α} {t : (i : α) → Set (β i)} (hs : s.Finite) (ht : ∀ i ∈ s, (t i).Finite) : (s.sigma t).Finite

A finite sum of finite sets is finite