Mathlib Map

Theorems · Theorem · order theory

Set.prod_mono

∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β}, s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ ×ˢ t₁ ⊆ s₂ ×ˢ t₂
Defined in
Mathlib.Data.Set.Prod
Cited by
52 results in Mathlib
Foundations
Depth 7 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.prod_subset_prod_iff · cited by 15Set.prod_subset_prod_iffSet.prod_mono_right · cited by 11Set.prod_mono_rightSet.prod_mono_left · cited by 7Set.prod_mono_leftMonotone.set_prod · cited by 4Monotone.set_prodMeasureTheory.Measure.prod_prod_le · cited by 4Measure.prod_prod_leFilter.HasBasis.prod_same_index · cited by 3HasBasis.prod_same_indexSubsemiring.prod_mono · cited by 2Subsemiring.prod_monoSublattice.prod_mono · cited by 2Sublattice.prod_monoAntitone.set_prod · cited by 2Antitone.set_prodProbabilityTheory.Kernel.setIntegral_density · cited by 2Kernel.setIntegral_densitySubmodule.span_prod_le · cited by 2Submodule.span_prod_leSubring.prod_mono · cited by 2Subring.prod_monoManifold.LiftSourceTargetPropertyAt.prodMap · cited by 2LiftSourceTargetPropertyA…AddSubgroup.prod_mono · cited by 2AddSubgroup.prod_mononhdsSet_prod_le · cited by 2nhdsSet_prod_leSet · cited by 53352SetSProd.sprod · cited by 1750SProd.sprodSet.prod_monoCITED BYCITES

Cites2

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
  • SProd.sprodstatement and proof · cited by 1,750

Cited by52

Results whose statement or proof uses this declaration.