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

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).

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.

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

@[simp]

theorem Finset.filter_val {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Finset α) : (filter p s).val = Multiset.filter p s.val

@[simp]

theorem Finset.filter_subset {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Finset α) : filter p s ⊆ s

@[simp]

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

theorem Finset.mem_of_mem_filter {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Finset α} (x : α) (h : x ∈ filter p s) : x ∈ s

theorem Finset.filter_ssubset {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Finset α} : filter p s ⊂ s ↔ ∃ x ∈ s, ¬p x

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

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)

theorem Finset.filter_congr_decidable {α : Type u_1} (s : Finset α) (p : α → Prop) (h : DecidablePred p) [DecidablePred p] : filter p s = filter p s

@[simp]

theorem Finset.filter_True {α : Type u_1} {h : DecidablePred fun (x : α) => True} (s : Finset α) : filter (fun (x : α) => True) s = s

@[simp]

theorem Finset.filter_False {α : Type u_1} {h : DecidablePred fun (x : α) => False} (s : Finset α) : filter (fun (x : α) => False) s = ∅

theorem Finset.filter_eq_self {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Finset α} : filter p s = s ↔ ∀ x ∈ s, p x

theorem Finset.filter_eq_empty_iff {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Finset α} : filter p s = ∅ ↔ ∀ ⦃x : α⦄, x ∈ s → ¬p x

theorem Finset.filter_nonempty_iff {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Finset α} : (filter p s).Nonempty ↔ ∃ a ∈ s, p a

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.

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 ∅.

@[simp]

theorem Finset.filter_const {α : Type u_1} (p : Prop) [Decidable p] (s : Finset α) : filter (fun (_a : α) => p) s = if p then s else ∅

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

@[simp]

theorem Finset.filter_empty {α : Type u_1} (p : α → Prop) [DecidablePred p] : filter p ∅ = ∅

theorem Finset.filter_subset_filter {α : Type u_1} (p : α → Prop) [DecidablePred p] {s t : Finset α} (h : s ⊆ t) : filter p s ⊆ filter p t

theorem Finset.monotone_filter_left {α : Type u_1} (p : α → Prop) [DecidablePred p] : Monotone (filter p)

theorem Finset.monotone_filter_right {α : Type u_1} (s : Finset α) ⦃p q : α → Prop⦄ [DecidablePred p] [DecidablePred q] (h : p ≤ q) : filter p s ⊆ filter q s

@[simp]

theorem Finset.coe_filter {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Finset α) : ↑(filter p s) = {x : α | x ∈ s ∧ p x}

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)

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)

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

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)

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)

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)