Lattice operations on finsets #
sup #
Supremum of a finite set: sup {a, b, c} f = f a ⊔ f b ⊔ f c⊔ f b ⊔ f c⊔ f c
Equations
- Finset.sup s f = Finset.fold (fun x x_1 => x ⊔ x_1) ⊥ f s
Alias of the reverse direction of Finset.sup_le_iff
.
See also Finset.product_bunionᵢ
.
Computing sup
in a subtype (closed under sup
) is the same as computing it in α
.
inf #
Infimum of a finite set: inf {a, b, c} f = f a ⊓ f b ⊓ f c⊓ f b ⊓ f c⊓ f c
Equations
- Finset.inf s f = Finset.fold (fun x x_1 => x ⊓ x_1) ⊤ f s
Alias of the reverse direction of Finset.le_inf_iff
.
Computing inf
in a subtype (closed under inf
) is the same as computing it in α
.
Given nonempty finset s
then s.sup' H f
is the supremum of its image under f
in (possibly
unbounded) join-semilattice α
, where H
is a proof of nonemptiness. If α
has a bottom element
you may instead use Finset.sup
which does not require s
nonempty.
Equations
- Finset.sup' s H f = WithBot.unbot (Finset.sup s (WithBot.some ∘ f)) (_ : Finset.sup s (WithBot.some ∘ f) ≠ ⊥)
Given nonempty finset s
then s.inf' H f
is the infimum of its image under f
in (possibly
unbounded) meet-semilattice α
, where H
is a proof of nonemptiness. If α
has a top element you
may instead use Finset.inf
which does not require s
nonempty.
Equations
- Finset.inf' s H f = WithTop.untop (Finset.inf s (WithTop.some ∘ f)) (_ : Finset.inf s (WithTop.some ∘ f) ≠ ⊤)
max and min of finite sets #
Let s
be a finset in a linear order. Then s.max
is the maximum of s
if s
is not empty,
and ⊥⊥
otherwise. It belongs to WithBot α
. If you want to get an element of α
, see
s.max'
.
Equations
- Finset.max s = Finset.sup s WithBot.some
Let s
be a finset in a linear order. Then s.min
is the minimum of s
if s
is not empty,
and ⊤⊤
otherwise. It belongs to WithTop α
. If you want to get an element of α
, see
s.min'
.
Equations
- Finset.min s = Finset.inf s WithTop.some
Given a nonempty finset s
in a linear order α
, then s.min' h
is its minimum, as an
element of α
, where h
is a proof of nonemptiness. Without this assumption, use instead s.min
,
taking values in WithTop α
.
Equations
- Finset.min' s H = Finset.inf' s H id
Given a nonempty finset s
in a linear order α
, then s.max' h
is its maximum, as an
element of α
, where h
is a proof of nonemptiness. Without this assumption, use instead s.max
,
taking values in WithBot α
.
Equations
- Finset.max' s H = Finset.sup' s H id
{a}.min' _
is a
.
{a}.max' _
is a
.
If there's more than 1 element, the min' is less than the max'. An alternate version of
min'_lt_max'
which is sometimes more convenient.
If finsets s
and t
are interleaved, then Finset.card s ≤ Finset.card t + 1≤ Finset.card t + 1
.
If finsets s
and t
are interleaved, then Finset.card s ≤ Finset.card (t \ s) + 1≤ Finset.card (t \ s) + 1
.
Induction principle for Finset
s in a linearly ordered type: a predicate is true on all
s : Finset α
provided that:
- it is true on the empty
Finset
, - for every
s : Finset α
and an elementa
strictly greater than all elements ofs
,p s
impliesp (insert a s)
.
Induction principle for Finset
s in a linearly ordered type: a predicate is true on all
s : Finset α
provided that:
- it is true on the empty
Finset
, - for every
s : Finset α
and an elementa
strictly less than all elements ofs
,p s
impliesp (insert a s)
.
Induction principle for Finset
s in any type from which a given function f
maps to a linearly
ordered type : a predicate is true on all s : Finset α
provided that:
- it is true on the empty
Finset
, - for every
s : Finset α
and an elementa
such that for elements ofs
denoted byx
we havef x ≤ f a≤ f a
,p s
impliesp (insert a s)
.
Induction principle for Finset
s in any type from which a given function f
maps to a linearly
ordered type : a predicate is true on all s : Finset α
provided that:
- it is true on the empty
Finset
, - for every
s : Finset α
and an elementa
such that for elements ofs
denoted byx
we havef a ≤ f x≤ f x
,p s
impliesp (insert a s)
.
Supremum of s i
, i : ι
, is equal to the supremum over t : Finset ι
of suprema
⨆ i ∈ t, s i⨆ i ∈ t, s i∈ t, s i
. This version assumes ι
is a Type _
. See supᵢ_eq_supᵢ_finset'
for a version
that works for ι : Sort*
.
Supremum of s i
, i : ι
, is equal to the supremum over t : Finset ι
of suprema
⨆ i ∈ t, s i⨆ i ∈ t, s i∈ t, s i
. This version works for ι : Sort*
. See supᵢ_eq_supᵢ_finset
for a version
that assumes ι : Type _
but has no plift
s.
Infimum of s i
, i : ι
, is equal to the infimum over t : Finset ι
of infima
⨅ i ∈ t, s i⨅ i ∈ t, s i∈ t, s i
. This version assumes ι
is a Type _
. See infᵢ_eq_infᵢ_finset'
for a version
that works for ι : Sort*
.
Infimum of s i
, i : ι
, is equal to the infimum over t : Finset ι
of infima
⨅ i ∈ t, s i⨅ i ∈ t, s i∈ t, s i
. This version works for ι : Sort*
. See infᵢ_eq_infᵢ_finset
for a version
that assumes ι : Type _
but has no plift
s.
Union of an indexed family of sets s : ι → Set α→ Set α
is equal to the union of the unions
of finite subfamilies. This version assumes ι : Type _
. See also unionᵢ_eq_unionᵢ_finset'
for
a version that works for ι : Sort*
.
Union of an indexed family of sets s : ι → Set α→ Set α
is equal to the union of the unions
of finite subfamilies. This version works for ι : Sort*
. See also unionᵢ_eq_unionᵢ_finset
for
a version that assumes ι : Type _
but avoids plift
s in the right hand side.
Intersection of an indexed family of sets s : ι → Set α→ Set α
is equal to the intersection of the
intersections of finite subfamilies. This version assumes ι : Type _
. See also
interᵢ_eq_interᵢ_finset'
for a version that works for ι : Sort*
.
Intersection of an indexed family of sets s : ι → Set α→ Set α
is equal to the intersection of the
intersections of finite subfamilies. This version works for ι : Sort*
. See also
interᵢ_eq_interᵢ_finset
for a version that assumes ι : Type _
but avoids plift
s in the right
hand side.