Theorems · Theorem · order theory
Set.prod_nonempty_iff
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, (s ×ˢ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty- Defined in
- Mathlib.Data.Set.Prod
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Set.Nonemptystatement and proof · cited by 2,627
- SProd.sprodstatement and proof · cited by 1,750
- Set.Nonempty.prodproof · cited by 8
- Set.Nonempty.fstproof · cited by 4
- Set.Nonempty.sndproof · cited by 4
Cited by6
Results whose statement or proof uses this declaration.
- Set.prod_subset_prod_iffproof · cited by 15
- IsPiSystem.prodproof · cited by 4
- Set.prod_eq_prod_iff_of_nonemptyproof · cited by 2
- measurableSet_prodproof · cited by 0
- isOpen_prod_iff'proof · cited by 0
- countableInfClosure_prodproof · cited by 0