Theorems · Definition · combinatorics
Finset.bipartiteBelow
{α : Type u_2} → {β : Type u_3} → (r : α → β → Prop) → Finset α → (b : β) → [(a : α) → Decidable (r a b)] → Finset αElements of s which are "below" b according to relation r.
- Cited by
- 24 results in Mathlib
- Foundations
- Depth 26 from the axioms · uses propext, Quot.sound
- Assumes
- Decidable
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
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
- Finset.filterproof · cited by 949
Cited by24
Results whose statement or proof uses this declaration.
- Finset.card_mul_le_card_mulstatement and proof · cited by 6
- Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelowstatement and proof · cited by 5
- Finset.ruzsa_triangle_inequality_div_div_divproof · cited by 3
- Finset.ruzsa_triangle_inequality_sub_sub_subproof · cited by 3
- Finset.bipartiteBelow.congr_simpstatement and proof · cited by 2
- Finset.card_mul_le_card_mul'statement and proof · cited by 2
- Finset.card_nsmul_le_card_nsmulstatement and proof · cited by 2
- Finset.card_nsmul_le_card_nsmul'statement and proof · cited by 2
- Finset.mem_bipartiteBelowstatement · cited by 2
- Finset.local_lubell_yamamoto_meshalkin_inequality_mulproof · cited by 2
- Finset.sum_sum_bipartiteAbove_eq_sum_sum_bipartiteBelowstatement · cited by 1
- Finset.card_mul_eq_card_mulstatement and proof · cited by 1