Theorems · Theorem · order theory
Finset.insert_eq
∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), insert a s = {a} ∪ s- Defined in
- Mathlib.Data.Finset.Lattice.Lemmas
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 27 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
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
Cited by12
Results whose statement or proof uses this declaration.
- MeasureTheory.lmarginal_insertproof · cited by 4
- MeasureTheory.lmarginal_insert'proof · cited by 2
- Finset.fold_union_empty_singletonproof · cited by 1
- SimpleGraph.IsSRGWith.card_commonNeighbors_eq_of_adj_complproof · cited by 1
- xInTermsOfW_vars_auxproof · cited by 1
- Finsupp.support_single_addproof · cited by 1
- Finset.pluennecke_petridis_inequality_addproof · cited by 1
- Finset.pluennecke_petridis_inequality_mulproof · cited by 1
- AhlswedeZhang.supSum_of_univ_notMemproof · cited by 1
- Finset.covBy_iff_card_sdiff_eq_oneproof · cited by 0
- Finsupp.support_add_singleproof · cited by 0
- Finset.induction_on_unionproof · cited by 0