Theorems · Theorem · group theory
Finset.add_mem_add
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {s t : Finset α} {a b : α}, a ∈ s → b ∈ t → a + b ∈ s + t- Cited by
- 12 results in Mathlib
- Foundations
- Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableEqAdd
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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.addstatement · cited by 133
- Finset.mem_image₂_of_memproof · cited by 20
Cited by12
Results whose statement or proof uses this declaration.
- Finset.addEnergy_eq_sum_sq'proof · cited by 2
- Finset.nsmul_ssubset_nsmul_succ_of_nsmul_ne_closureproof · cited by 1
- Finset.Nontrivial.add_leftproof · cited by 1
- MeasureTheory.Measure.haar.le_addIndex_mulproof · cited by 1
- Finset.card_sq_le_card_mul_addEnergyproof · cited by 1
- Finset.le_card_add_mul_addEnergyproof · cited by 0
- Finset.le_card_quotient_add_sq_inter_addSubgroupproof · cited by 0
- UniqueSums.of_sameproof · cited by 0
- Finset.addEnergy_eq_sum_sqproof · cited by 0
- Finset.card_nsmul_quotient_add_nsmul_inter_addSubgroup_leproof · cited by 0
- cauchy_davenport_add_of_linearOrder_isCancelAddproof · cited by 0
- Finset.Nontrivial.add_rightproof · cited by 0