Mathlib Map

Theorems · Theorem · order theory

Set.empty_prod

∀ {α : Type u_1} {β : Type u_2} {t : Set β}, ∅ ×ˢ t = ∅
Defined in
Mathlib.Data.Set.Prod
Cited by
14 results in Mathlib
Foundations
Depth 6 from the axioms · uses propext, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

MeasureTheory.VectorMeasure.prod_apply · cited by 2VectorMeasure.prod_applyProbabilityTheory.Kernel.setIntegral_density · cited by 2Kernel.setIntegral_densityModelWithCorners.boundary_of_boundaryless_left · cited by 1ModelWithCorners.boundary…affineSpan_prod_eq · cited by 1affineSpan_prod_eqProbabilityTheory.setLIntegral_toKernel_prod · cited by 1ProbabilityTheory.setLInt…MeasureTheory.measurableSet_predictable_Ioc_prod · cited by 1MeasureTheory.measurableS…AffineSubspace.prod_bot_left · cited by 1AffineSubspace.prod_bot_l…Set.prod_surjOn_snd_iff · cited by 0Set.prod_surjOn_snd_ifffrontier_univ_prod_eq · cited by 0frontier_univ_prod_eqUpperSet.top_prod · cited by 0UpperSet.top_prodSublattice.bot_prod · cited by 0Sublattice.bot_prodBornology.isBounded_prod · cited by 0Bornology.isBounded_prodLowerSet.bot_prod · cited by 0LowerSet.bot_prodSet.prod_surjOn_fst_iff · cited by 0Set.prod_surjOn_fst_iffSet · cited by 53352SetSet.ext · cited by 2266Set.extSProd.sprod · cited by 1750SProd.sprodSet.empty_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.extproof · cited by 2,266
  • SProd.sprodstatement · cited by 1,750

Cited by14

Results whose statement or proof uses this declaration.