Theorems · Theorem · combinatorics

Finset.filter.congr_simp

∀ {α : Type u_1} (p p_1 : α → Prop),
  p = p_1 →
    ∀ {inst : DecidablePred p} [inst_1 : DecidablePred p_1] (s s_1 : Finset α),
      s = s_1 → Finset.filter p s = Finset.filter p_1 s_1

Defined in: Mathlib.Data.Finset.Filter
Cited by: 47 results in Mathlib
Foundations: Depth 26 from the axioms · uses propext, Quot.sound
Assumes: DecidablePred

Mathlib docs Source Loogle LeanSearch

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 and proof · cited by 949

Cited by47

Results whose statement or proof uses this declaration.

ProbabilityTheory.iIndepFun.charFunDual_map_finsetSum_eq_prodproof · cited by 4
Finsupp.neLocus_commproof · cited by 3
Nat.sq_mul_squarefree_of_posproof · cited by 3
IsNilpotent.exp_add_of_commuteproof · cited by 3
DFinsupp.neLocus_commproof · cited by 3
Finpartition.equitabilise_auxproof · cited by 3
Chebyshev.psi_eq_sum_theta'proof · cited by 2
Chebyshev.sum_PrimePow_eq_sum_sum'proof · cited by 2
QuadraticMap.map_sumproof · cited by 2
PairReduction.card_pairSetSeq_le_logSizeRadius_mulproof · cited by 1
Finset.addEnergy_commproof · cited by 1
Finset.addEnergy_empty_leftproof · cited by 1