Mathlib Map

Theorems · Theorem · logic and foundations

Set.inter_right_comm

∀ {α : Type u} (s₁ s₂ s₃ : Set α), s₁ ∩ s₂ ∩ s₃ = s₁ ∩ s₃ ∩ s₂
Defined in
Mathlib.Data.Set.Basic
Cited by
9 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.

differentiableWithinAt_localInvariantProp · cited by 13differentiableWithinAt_lo…ModelWithCorners.extendCoordChange_source · cited by 9ModelWithCorners.extendCo…Set.inter_sdiff_right_comm · cited by 2Set.inter_sdiff_right_commIsClosed.two_pow_mk_le_two_pow_mk_dense · cited by 2IsClosed.two_pow_mk_le_tw…Matroid.uniqueBaseOn_closure_eq · cited by 1Matroid.uniqueBaseOn_clos…Matroid.IsBase.compl_inter_isBasis_of_inter_isBasis · cited by 1IsBase.compl_inter_isBasi…contDiffWithinAt_localInvariantProp_of_le · cited by 1contDiffWithinAt_localInv…ProbabilityTheory.comap_cond · cited by 0ProbabilityTheory.comap_c…Matroid.uniqueBaseOn_restrict · cited by 0Matroid.uniqueBaseOn_rest…Set · cited by 53352SetSet.ext · cited by 2266Set.extSet.inter_right_commCITED 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
  • Set.extproof · cited by 2,266

Cited by9

Results whose statement or proof uses this declaration.