Theorems · Theorem · combinatorics

Finset.mem_filter

∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Finset α} {a : α}, a ∈ Finset.filter p s ↔ a ∈ s ∧ p a

Defined in

Mathlib.Data.Finset.Filter

Cited by

185 results in Mathlib

Foundations

Depth 54 from the axioms, rests on 817 definitions · uses propext, Classical.choice, Quot.sound

Assumes

DecidablePred