Theorems · Theorem · order theory
Set.insert_sdiff_singleton
∀ {α : Type u_1} {s : Set α} {a : α}, insert a (s \ {a}) = insert a s- Defined in
- Mathlib.Order.BooleanAlgebra.Set
- Cited by
- 28 results in Mathlib
- Foundations
- Depth 58 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- Setstatement and proof · cited by 53,352
- Set.union_sdiff_selfproof · cited by 28
Cited by28
Results whose statement or proof uses this declaration.
- Set.encard_sdiff_singleton_add_oneproof · cited by 6
- Matroid.IsCircuit.sdiff_singleton_isBasisproof · cited by 4
- hasFDerivWithinAt_sdiff_singleton_selfproof · cited by 3
- Set.wellFoundedOn_sdiff_singletonproof · cited by 3
- vectorSpan_image_eq_span_vsub_set_left_neproof · cited by 3
- MulAction.IsMultiplyPretransitive.index_of_fixingSubgroup_mulproof · cited by 2
- contDiffWithinAt_sdiff_singletonproof · cited by 2
- Matroid.IsCircuit.strong_multi_eliminationproof · cited by 2
- hasFDerivWithinAt_sdiff_singletonproof · cited by 2
- exists_sSupIndep_disjoint_sSup_atomsproof · cited by 2
- Set.encard_eq_twoproof · cited by 2
- Set.encard_eq_threeproof · cited by 2