Basic lemmas on finite sets #
This file contains lemmas on the interaction of various definitions on the Finset
type.
For an explanation of Finset
design decisions, please see Mathlib/Data/Finset/Defs.lean
.
Main declarations #
Main definitions #
Finset.choose
: Given a proofh
of existence and uniqueness of a certain element satisfying a predicate,choose s h
returns the element ofs
satisfying that predicate.
Equivalences between finsets #
- The
Mathlib/Logic/Equiv/Defs.lean
file describes a general type of equivalence, so look in there for any lemmas. There is some API for rewriting sums and products froms
tot
given thats ≃ t
. TODO: examples
Tags #
finite sets, finset
Lattice structure #
union #
inter #
Alias of the reverse direction of Finset.not_disjoint_iff_nonempty_inter
.
erase #
sdiff #
attach #
Alias of the reverse direction of Finset.attach_nonempty_iff
.
filter #
Alias of Finset.disjoint_filter_filter_neg
.
After filtering out everything that does not equal a given value, at most that value remains.
This is equivalent to filter_eq'
with the equality the other way.
After filtering out everything that does not equal a given value, at most that value remains.
This is equivalent to filter_eq
with the equality the other way.
range #
dedup on list and multiset #
Alias of the reverse direction of Multiset.toFinset_nonempty
.
Alias of the reverse direction of List.toFinset_nonempty_iff
.
choose #
Given a finset l
and a predicate p
, associate to a proof that there is a unique element of
l
satisfying p
this unique element, as an element of the corresponding subtype.
Equations
- Finset.chooseX p l hp = Multiset.chooseX p l.val hp
Instances For
Given a finset l
and a predicate p
, associate to a proof that there is a unique element of
l
satisfying p
this unique element, as an element of the ambient type.
Equations
- Finset.choose p l hp = ↑(Finset.chooseX p l hp)
Instances For
The disjoint union of finsets is a sum
Equations
- Equiv.Finset.union s t h = ((Equiv.Set.ofEq ⋯).trans (Equiv.Set.union ⋯)).symm
Instances For
The type of dependent functions on the disjoint union of finsets s ∪ t
is equivalent to the
type of pairs of functions on s
and on t
. This is similar to Equiv.sumPiEquivProdPi
.
Equations
- One or more equations did not get rendered due to their size.