Theorems · Theorem · combinatorics
Finset.filter_mem_eq_inter
∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} [inst_1 : (i : α) → Decidable (i ∈ t)], {i ∈ s | i ∈ t} = s ∩ t- Defined in
- Mathlib.Data.Finset.Basic
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableEqDecidable
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.filterstatement · cited by 949
Cited by14
Results whose statement or proof uses this declaration.
- Finset.sum_ite_memproof · cited by 14
- Finset.prod_ite_memproof · cited by 8
- SimpleGraph.antitoneOn_extremalNumber_div_choose_twoproof · cited by 3
- Finset.prod_piecewiseproof · cited by 2
- Fintype.sum_extend_by_zeroproof · cited by 2
- Finset.sum_piecewiseproof · cited by 2
- AffineIndependent.convexHull_interproof · cited by 1
- IsLinearSet.isProperSemilinearSetproof · cited by 1
- SimpleGraph.filter_edgeFinset_toFinset_subsetproof · cited by 1
- Finset.sum_indicator_eq_sum_interproof · cited by 1
- SimpleGraph.IsSRGWith.param_eqproof · cited by 0
- Finset.prod_mulIndicator_eq_prod_interproof · cited by 0