Theorems · Theorem · order theory
Set.disjoint_right
∀ {α : Type u} {s t : Set α}, Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ t → a ∉ s- Defined in
- Mathlib.Data.Set.Disjoint
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 22 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- Disjointstatement · cited by 2,201
- Set.disjoint_leftproof · cited by 121
- disjoint_commproof · cited by 49
Cited by17
Results whose statement or proof uses this declaration.
- ProbabilityTheory.Kernel.indepSets_piiUnionInter_of_disjointproof · cited by 4
- Disjoint.notMem_of_mem_rightproof · cited by 4
- Fin.Embedding.exists_embedding_disjoint_range_of_add_le_ENat_cardproof · cited by 2
- SimpleGraph.IsBipartiteWith.mem_of_mem_adj'proof · cited by 2
- Composition.mem_range_embedding_iff'proof · cited by 2
- BumpCovering.exists_isSubordinate_of_locallyFinite_of_propproof · cited by 2
- exists_contMDiffMap_zero_one_of_isClosedproof · cited by 2
- Set.indicator_add_eq_rightproof · cited by 2
- PrimeSpectrum.isLocalization_away_iff_atPrime_of_basicOpen_eq_singletonproof · cited by 1
- DenseRange.zsmul_of_ergodic_add_leftproof · cited by 1
- BumpCovering.exists_isSubordinate_of_locallyFinite_of_prop_t2spaceproof · cited by 1
- Submodule.mem_of_isLocalized_spanproof · cited by 1