theorem
Set.Nonempty.sigma
{ι : Type u_1}
{α : ι → Type u_2}
{s : Set ι}
{t : (i : ι) → Set (α i)}
:
Set.Nonempty s → (∀ (i : ι), Set.Nonempty (t i)) → Set.Nonempty (Set.Sigma s t)
theorem
Set.Nonempty.sigma_fst
{ι : Type u_1}
{α : ι → Type u_2}
{s : Set ι}
{t : (i : ι) → Set (α i)}
:
Set.Nonempty (Set.Sigma s t) → Set.Nonempty s
theorem
Set.Nonempty.sigma_snd
{ι : Type u_1}
{α : ι → Type u_2}
{s : Set ι}
{t : (i : ι) → Set (α i)}
:
Set.Nonempty (Set.Sigma s t) → ∃ i, i ∈ s ∧ Set.Nonempty (t i)
theorem
Set.sigma_nonempty_iff
{ι : Type u_1}
{α : ι → Type u_2}
{s : Set ι}
{t : (i : ι) → Set (α i)}
:
Set.Nonempty (Set.Sigma s t) ↔ ∃ i, i ∈ s ∧ Set.Nonempty (t i)