Theorems · Theorem · combinatorics
Finset.disjoint_right
∀ {α : Type u_2} {s t : Finset α}, Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ t → a ∉ s- Defined in
- Mathlib.Data.Finset.Disjoint
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 59 from the axioms · uses propext, Classical.choice, 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.
- Finsetstatement and proof · cited by 13,712
- Disjointstatement · cited by 2,201
- Finset.disjoint_leftproof · cited by 50
- disjoint_commproof · cited by 49
Cited by9
Results whose statement or proof uses this declaration.
- ProbabilityTheory.Kernel.iIndepFun.indepFun_finsetproof · cited by 8
- Finset.disjoint_of_subset_rightproof · cited by 6
- Disjoint.notMem_of_mem_right_finsetproof · cited by 2
- Finset.IsAntichain.disjoint_slice_shadow_fallingproof · cited by 1
- UV.shadow_compression_subset_compression_shadowproof · cited by 1
- Equiv.Perm.Basis.ofPermHomFun_apply_mem_support_cycle_iffproof · cited by 1
- Finset.UV.isInitSeg_of_compressedproof · cited by 1
- MultilinearMap.map_sum_finset_auxproof · cited by 1
- Finset.erdos_ko_radoproof · cited by 0