Mathlib Map

Theorems · Theorem · order theory

Set.prod_inter_prod

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

Around this declaration

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

MeasureTheory.Measure.prod_restrict · cited by 12Measure.prod_restrictIsPiSystem.prod · cited by 4IsPiSystem.prodUniqueMDiffWithinAt.prod · cited by 2UniqueMDiffWithinAt.prodTopologicalSpace.Compacts.continuous_prod · cited by 2Compacts.continuous_prodUpperSet.prod_sup_prod · cited by 1UpperSet.prod_sup_prodMeasure.ext_of_lintegral_prod_mul_prod_boundedContinuousFunction · cited by 1Measure.ext_of_lintegral_…LowerSet.prod_inf_prod · cited by 1LowerSet.prod_inf_prodNonUnitalSubalgebra.prod_inf_prod · cited by 0NonUnitalSubalgebra.prod_…Subalgebra.prod_inf_prod · cited by 0Subalgebra.prod_inf_prodSubmodule.prod_inf_prod · cited by 0Submodule.prod_inf_prodMeasureTheory.ProbabilityMeasure.continuous_prod · cited by 0ProbabilityMeasure.contin…Set.sym2_inter · cited by 0Set.sym2_interAffineSubspace.prod_inf_prod · cited by 0AffineSubspace.prod_inf_p…NonUnitalStarSubalgebra.prod_inf_prod · cited by 0NonUnitalStarSubalgebra.p…Set · cited by 53352SetSet.ext · cited by 2266Set.extSProd.sprod · cited by 1750SProd.sprodSet.prod_inter_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 and proof · cited by 1,750

Cited by14

Results whose statement or proof uses this declaration.