Filtering a finite set #
Main declarations #
Finset.filter
: Given a decidable predicatep : α → Prop
,s.filter p
is the finset consisting of those elements ins
satisfying the predicatep
.
Tags #
finite sets, finset
filter #
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
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
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 theSet
builder notation elaborator that this elaborator partly overrides.Data.Fintype.Basic
for theFinset
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 theFinset
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
If all elements of a Finset
satisfy the predicate p
, s.filter p
is s
.
If all elements of a Finset
fail to satisfy the predicate p
, s.filter p
is ∅
.