Mathlib Map

Theorems · Theorem · order theory

Set.univ_prod_univ

∀ {α : Type u_1} {β : Type u_2}, Set.univ ×ˢ Set.univ = Set.univ
Defined in
Mathlib.Data.Set.Prod
Cited by
32 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.

HasFPowerSeriesAt.hasStrictFDerivAt · cited by 7HasFPowerSeriesAt.hasStri…tangentBundle_model_space_chartAt · cited by 4tangentBundle_model_space…uniformContinuousOn_univ · cited by 4uniformContinuousOn_univNumberField.mixedEmbedding.polarCoordReal_symm_target_ae_eq_univ · cited by 2mixedEmbedding.polarCoord…uniformEquicontinuousOn_univ · cited by 2uniformEquicontinuousOn_u…ContDiffAt.prodMap · cited by 2ContDiffAt.prodMapSet.image2_range · cited by 2Set.image2_rangeMeasureTheory.FiniteMeasure.mass_prod · cited by 2FiniteMeasure.mass_prodProbabilityTheory.Kernel.tendsto_integral_density_of_monotone · cited by 2Kernel.tendsto_integral_d…range_toPullbackDiag · cited by 2range_toPullbackDiagContMDiffAt.mfderiv · cited by 2ContMDiffAt.mfderivPartialEquiv.refl_prod_refl · cited by 2PartialEquiv.refl_prod_re…MeasureTheory.Measure.ext_prod · cited by 1Measure.ext_prodTendstoUniformly.prodMap · cited by 1TendstoUniformly.prodMapMDifferentiableAt.prodMap · cited by 1MDifferentiableAt.prodMapSet · cited by 53352SetSet.univ · cited by 3945Set.univSet.ext · cited by 2266Set.extSProd.sprod · cited by 1750SProd.sprodSet.univ_prod_univCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by32

Results whose statement or proof uses this declaration.