Theorems · Theorem · order theory
Finset.sdiff_subset
∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s \ t ⊆ s- Defined in
- Mathlib.Data.Finset.SDiff
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 62 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 by21
Results whose statement or proof uses this declaration.
- Finset.sum_eraseproof · cited by 5
- Finpartition.equitabilise_auxproof · cited by 3
- Finset.prod_involutionproof · cited by 2
- SimpleGraph.deleteFar_iffproof · cited by 2
- Finset.prod_eraseproof · cited by 2
- BoxIntegral.integrable_of_bounded_and_ae_continuousWithinAtproof · cited by 2
- Int.erdos_ginzburg_zivproof · cited by 2
- Finset.sum_involutionproof · cited by 2
- Nat.eq_properDivisors_of_subset_of_sum_eq_sumproof · cited by 2
- OrthogonalFamily.norm_sq_sdiff_sumproof · cited by 2
- Finset.mem_upShadow_iterate_iff_exists_sdiffproof · cited by 1
- HallMarriageTheorem.hall_hard_inductive_step_Bproof · cited by 1