Image and map operations on finite sets #
This file provides the finite analog of Set.image
, along with some other similar functions.
Note there are two ways to take the image over a finset; via Finset.image
which applies the
function then removes duplicates (requiring DecidableEq
), or via Finset.map
which exploits
injectivity of the function to avoid needing to deduplicate. Choosing between these is similar to
choosing between insert
and Finset.cons
, or between Finset.union
and Finset.disjUnion
.
Main definitions #
Finset.image
: Given a functionf : α → β
,s.image f
is the image finset inβ
.Finset.map
: Given an embeddingf : α ↪ β
,s.map f
is the image finset inβ
.Finset.filterMap
Given a functionf : α → Option β
,s.filterMap f
is the image finset inβ
, filtering outnone
s.Finset.subtype
:s.subtype p
is the finset ofSubtype p
whose elements belong tos
.Finset.fin
:s.fin n
is the finset of all elements ofs
less thann
.
map #
If the only elements outside s
are those left fixed by σ
, then mapping by σ
has no effect.
Alias of the reverse direction of Finset.map_subset_map
.
Alias of the reverse direction of Finset.map_ssubset_map
.
Alias of the reverse direction of Finset.map_nonempty
.
image #
Alias of Finset.forall_mem_image
.
Alias of the forward direction of Finset.image_nonempty
.
filterMap #
filterMap f s
is a combination filter/map operation on s
.
The function f : α → Option β
is applied to each element of s
;
if f a
is some b
then b
is included in the result, otherwise
a
is excluded from the resulting finset.
In notation, filterMap f s
is the finset {b : β | ∃ a ∈ s , f a = some b}
.
Equations
Instances For
Subtype #
Given a finset s
and a predicate p
, s.subtype p
is the finset of Subtype p
whose
elements belong to s
.
Equations
Instances For
s.subtype p
converts back to s.filter p
with
Embedding.subtype
.
If all elements of a Finset
satisfy the predicate p
,
s.subtype p
converts back to s
with Embedding.subtype
.
If a Finset
of a subtype is converted to the main type with
Embedding.subtype
, all elements of the result have the property of
the subtype.
If a Finset
of a subtype is converted to the main type with
Embedding.subtype
, the result does not contain any value that does
not satisfy the property of the subtype.
Alias of Finset.notMem_map_subtype_of_not_property
.
If a Finset
of a subtype is converted to the main type with
Embedding.subtype
, the result does not contain any value that does
not satisfy the property of the subtype.
If a Finset
is a subset of the image of a Set
under f
,
then it is equal to the Finset.image
of a Finset
subset of that Set
.
If a finset t
is a subset of the image of another finset s
under f
, then it is equal to the
image of a subset of s
.
For the version where s
is a set, see subset_set_image_iff
.