# Filtering a finite set #

## Main declarations #

- `Finset.filter`: Given a decidable predicate `p : α → Prop`, `s.filter p` is the finset consisting of those elements in `s` satisfying the predicate `p`.

## Tags #

finite sets, finset

### filter #

source
def Finset.filter {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Finset α) :
Finset α

`Finset.filter p s` is the set of elements of `s` that satisfy `p`.

For example, one can use `s.filter (· ∈ t)` to get the intersection of `s` with `t : Set α` as a `Finset α` (when a `DecidablePred (· ∈ t)` instance is available).

Equations

- Finset.filter p s = { val := Multiset.filter p s.val, nodup := ⋯ }

Instances For

source
def Mathlib.Meta.knownToBeFinsetNotSet (expectedType? : Option Lean.Expr) :
Lean.Elab.TermElabM Bool

Return `true` if `expectedType?` is `some (Finset ?α)`, throws `throwUnsupportedSyntax` if it is `some (Set ?α)`, and returns `false` otherwise.

Equations

- One or more equations did not get rendered due to their size.
- Mathlib.Meta.knownToBeFinsetNotSet none = pure false

Instances For

source
def Mathlib.Meta.elabFinsetBuilderSep :
Lean.Elab.Term.TermElab

Elaborate set builder notation for `Finset`.

`{x ∈ s | p x}` is elaborated as `Finset.filter (fun x ↦ p x) s` if either the expected type is `Finset ?α` or the expected type is not `Set ?α` and `s` has expected type `Finset ?α`.

See also

- `Data.Set.Defs` for the `Set` builder notation elaborator that this elaborator partly overrides.
- `Data.Fintype.Basic` for the `Finset` builder notation elaborator handling syntax of the form `{x | p x}`, `{x : α | p x}`, `{x ∉ s | p x}`, `{x ≠ a | p x}`.
- `Order.LocallyFinite.Basic` for the `Finset` builder notation elaborator handling syntax of the form `{x ≤ a | p x}`, `{x ≥ a | p x}`, `{x < a | p x}`, `{x > a | p x}`.

TODO: Write a delaborator

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Finset.filter_val {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Finset α) :
(filter p s).val = Multiset.filter p s.val
source
@[simp]
theorem Finset.filter_subset {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Finset α) :
filter p s ⊆ s
source
@[simp]
theorem Finset.mem_filter {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Finset α} {a : α} :
a ∈ filter p s ↔ a ∈ s ∧ p a
source
theorem Finset.mem_of_mem_filter {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Finset α} (x : α) (h : x ∈ filter p s) :
x ∈ s
source
theorem Finset.filter_ssubset {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Finset α} :
filter p s ⊂ s ↔ ∃ x ∈ s, ¬p x
source
theorem Finset.filter_filter {α : Type u_1} (p q : α → Prop) [DecidablePred p] [DecidablePred q] (s : Finset α) :
filter q (filter p s) = filter (fun (a : α) => p a ∧ q a) s
source
theorem Finset.filter_comm {α : Type u_1} (p q : α → Prop) [DecidablePred p] [DecidablePred q] (s : Finset α) :
filter q (filter p s) = filter p (filter q s)
source
theorem Finset.filter_congr_decidable {α : Type u_1} (s : Finset α) (p : α → Prop) (h : DecidablePred p) [DecidablePred p] :
filter p s = filter p s
source
@[simp]
theorem Finset.filter_true {α : Type u_1} {h : DecidablePred fun (x : α) => True} (s : Finset α) :
filter (fun (x : α) => True) s = s
source
@[deprecated Finset.filter_true (since := "2025-08-24")]
theorem Finset.filter_True {α : Type u_1} {h : DecidablePred fun (x : α) => True} (s : Finset α) :
filter (fun (x : α) => True) s = s

Alias of `Finset.filter_true`.

source
@[simp]
theorem Finset.filter_false {α : Type u_1} {h : DecidablePred fun (x : α) => False} (s : Finset α) :
filter (fun (x : α) => False) s = ∅
source
@[deprecated Finset.filter_false (since := "2025-08-24")]
theorem Finset.filter_False {α : Type u_1} {h : DecidablePred fun (x : α) => False} (s : Finset α) :
filter (fun (x : α) => False) s = ∅

Alias of `Finset.filter_false`.

source
@[simp]
theorem Finset.filter_eq_self {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Finset α} :
filter p s = s ↔ ∀ x ∈ s, p x
source
@[simp]
theorem Finset.filter_eq_empty_iff {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Finset α} :
filter p s = ∅ ↔ ∀ ⦃x : α⦄, x ∈ s → ¬p x
source
theorem Finset.filter_nonempty_iff {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Finset α} :
(filter p s).Nonempty ↔ ∃ a ∈ s, p a
source
theorem Finset.filter_true_of_mem {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Finset α} (h : ∀ x ∈ s, p x) :
filter p s = s

If all elements of a `Finset` satisfy the predicate `p`, `s.filter p` is `s`.

source
theorem Finset.filter_false_of_mem {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Finset α} (h : ∀ x ∈ s, ¬p x) :
filter p s = ∅

If all elements of a `Finset` fail to satisfy the predicate `p`, `s.filter p` is `∅`.

source
@[simp]
theorem Finset.filter_const {α : Type u_1} (p : Prop) [Decidable p] (s : Finset α) :
filter (fun (_a : α) => p) s = if p then s else ∅
source
theorem Finset.filter_congr {α : Type u_1} {p q : α → Prop} [DecidablePred p] [DecidablePred q] {s : Finset α} (H : ∀ x ∈ s, p x ↔ q x) :
filter p s = filter q s
source
@[simp]
theorem Finset.filter_empty {α : Type u_1} (p : α → Prop) [DecidablePred p] :
filter p ∅ = ∅
source
theorem Finset.filter_subset_filter {α : Type u_1} (p : α → Prop) [DecidablePred p] {s t : Finset α} (h : s ⊆ t) :
filter p s ⊆ filter p t
source
theorem Finset.monotone_filter_left {α : Type u_1} (p : α → Prop) [DecidablePred p] :
Monotone (filter p)
source
theorem Finset.monotone_filter_right {α : Type u_1} (s : Finset α) ⦃p q : α → Prop⦄ [DecidablePred p] [DecidablePred q] (h : ∀ a ∈ s, p a → q a) :
filter p s ⊆ filter q s
source
@[simp]
theorem Finset.coe_filter {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Finset α) :
↑(filter p s) = {x : α | x ∈ s ∧ p x}
source
theorem Finset.subset_coe_filter_of_subset_forall {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Finset α) {t : Set α} (h₁ : t ⊆ ↑s) (h₂ : ∀ x ∈ t, p x) :
t ⊆ ↑(filter p s)
source
theorem Finset.disjoint_filter_filter {α : Type u_1} {s t : Finset α} {p q : α → Prop} [DecidablePred p] [DecidablePred q] :
Disjoint s t → Disjoint (filter p s) (filter q t)
source
theorem Set.pairwiseDisjoint_filter {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α → β) (s : Set β) (t : Finset α) :
s.PairwiseDisjoint fun (x : β) => Finset.filter (fun (x_1 : α) => f x_1 = x) t
source
theorem Finset.disjoint_filter_and_not_filter {α : Type u_1} (p q : α → Prop) [DecidablePred p] [DecidablePred q] {s : Finset α} :
Disjoint (filter (fun (x : α) => p x ∧ ¬q x) s) (filter (fun (x : α) => q x ∧ ¬p x) s)
source
theorem Finset.filter_inj {α : Type u_1} {p : α → Prop} [DecidablePred p] {s t : Finset α} :
filter p s = filter p t ↔ ∀ ⦃a : α⦄, p a → (a ∈ s ↔ a ∈ t)
source
theorem Finset.filter_inj' {α : Type u_1} {p q : α → Prop} [DecidablePred p] [DecidablePred q] {s : Finset α} :
filter p s = filter q s ↔ ∀ ⦃a : α⦄, a ∈ s → (p a ↔ q a)