Mathlib Map

Theorems · Theorem · order theory

Set.Nonempty.prod

∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, s.Nonempty → t.Nonempty → (s ×ˢ t).Nonempty
Defined in
Mathlib.Data.Set.Prod
Cited by
8 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Set.prod_nonempty_iff · cited by 6Set.prod_nonempty_iffIsConnected.prod · cited by 5IsConnected.prodGromovHausdorff.hausdorffDist_optimal · cited by 1GromovHausdorff.hausdorff…Complex.norm_circleTransformBoundingFunction_le · cited by 1Complex.norm_circleTransf…UniformOnFun.isBasis_gen · cited by 0UniformOnFun.isBasis_genIsPathConnected.prod · cited by 0IsPathConnected.prodBornology.isBounded_prod_self · cited by 0Bornology.isBounded_prod_…Bornology.isBounded_prod · cited by 0Bornology.isBounded_prodSet · cited by 53352SetSet.Nonempty · cited by 2627Set.NonemptySProd.sprod · cited by 1750SProd.sprodNonempty.prodCITED BYCITES

Cites3

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

Cited by8

Results whose statement or proof uses this declaration.