theorem Set.pi_nonempty {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t : (i : ι) → Set (α i)} : (s.pi t).Nonempty ↔ (∀ (i : ι), Nonempty (α i)) ∧ ∀ (i : ι), i ∈ s → (t i).Nonempty