Documentation

Mathlib.Data.Finset.Filter

Filtering a finite set #

Main declarations #

Tags #

finite sets, finset

filter #

def Finset.filter {α : Type u_1} (p : αProp) [DecidablePred p] (s : 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
Instances For

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

    Equations
    Instances For

      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
        @[simp]
        theorem Finset.filter_val {α : Type u_1} (p : αProp) [DecidablePred p] (s : Finset α) :
        (Finset.filter p s).val = Multiset.filter p s.val
        @[simp]
        theorem Finset.filter_subset {α : Type u_1} (p : αProp) [DecidablePred p] (s : Finset α) :
        @[simp]
        theorem Finset.mem_filter {α : Type u_1} {p : αProp} [DecidablePred p] {s : Finset α} {a : α} :
        a Finset.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 Finset.filter p s) :
        x s
        theorem Finset.filter_ssubset {α : Type u_1} {p : αProp} [DecidablePred p] {s : Finset α} :
        Finset.filter p s s xs, ¬p x
        theorem Finset.filter_filter {α : Type u_1} (p q : αProp) [DecidablePred p] [DecidablePred q] (s : Finset α) :
        Finset.filter q (Finset.filter p s) = Finset.filter (fun (a : α) => p a q a) s
        theorem Finset.filter_comm {α : Type u_1} (p q : αProp) [DecidablePred p] [DecidablePred q] (s : Finset α) :
        theorem Finset.filter_congr_decidable {α : Type u_1} (s : Finset α) (p : αProp) (h : DecidablePred p) [DecidablePred p] :
        @[simp]
        theorem Finset.filter_True {α : Type u_1} {h : DecidablePred fun (x : α) => True} (s : Finset α) :
        Finset.filter (fun (x : α) => True) s = s
        @[simp]
        theorem Finset.filter_False {α : Type u_1} {h : DecidablePred fun (x : α) => False} (s : Finset α) :
        Finset.filter (fun (x : α) => False) s =
        theorem Finset.filter_eq_self {α : Type u_1} {p : αProp} [DecidablePred p] {s : Finset α} :
        Finset.filter p s = s xs, p x
        theorem Finset.filter_eq_empty_iff {α : Type u_1} {p : αProp} [DecidablePred p] {s : Finset α} :
        Finset.filter p s = ∀ ⦃x : α⦄, x s¬p x
        theorem Finset.filter_nonempty_iff {α : Type u_1} {p : αProp} [DecidablePred p] {s : Finset α} :
        (Finset.filter p s).Nonempty as, p a
        theorem Finset.filter_true_of_mem {α : Type u_1} {p : αProp} [DecidablePred p] {s : Finset α} (h : xs, p x) :

        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 : xs, ¬p x) :

        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 α) :
        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 : xs, p x q x) :
        @[simp]
        theorem Finset.filter_empty {α : Type u_1} (p : αProp) [DecidablePred p] :
        theorem Finset.filter_subset_filter {α : Type u_1} (p : αProp) [DecidablePred p] {s t : Finset α} (h : s t) :
        theorem Finset.monotone_filter_right {α : Type u_1} (s : Finset α) ⦃p q : αProp [DecidablePred p] [DecidablePred q] (h : p q) :
        @[simp]
        theorem Finset.coe_filter {α : Type u_1} (p : αProp) [DecidablePred p] (s : Finset α) :
        (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₂ : xt, p x) :
        t (Finset.filter p s)
        theorem Finset.disjoint_filter_filter {α : Type u_1} {s t : Finset α} {p q : αProp} [DecidablePred p] [DecidablePred q] :
        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.filter_inj {α : Type u_1} {p : αProp} [DecidablePred p] {s t : Finset α} :
        Finset.filter p s = Finset.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 α} :
        Finset.filter p s = Finset.filter q s ∀ ⦃a : α⦄, a s(p a q a)