Finite types #
This file defines a typeclass to state that a type is finite.
Main declarations #
Fintype α
: Typeclass saying that a type is finite. It takes as fields aFinset
and a proof that all terms of typeα
are in it.Finset.univ
: The finset of all elements of a fintype.
See Data.Fintype.Card
for the cardinality of a fintype,
the equivalence with Fin (Fintype.card α)
, and pigeonhole principles.
Instances #
Instances for Fintype
for
{x // p x}
are in this file asFintype.subtype
Option α
are inData.Fintype.Option
α × β× β
are inData.Fintype.Prod
α ⊕ β⊕ β
are inData.Fintype.Sum
Σ (a : α), β a
are inData.Fintype.Sigma
These files also contain appropriate Infinite
instances for these types.
Infinite
instances for ℕ
, ℤ
, Multiset α
, and List α
are in Data.Fintype.Lattice
.
Types which have a surjection from/an injection to a Fintype
are themselves fintypes.
See Fintype.ofInjective
and Fintype.ofSurjective
.
- elems : Finset α
A proof that
elems
contains every element of the typecomplete : ∀ (x : α), x ∈ elems
Fintype α
means that α
is finite, i.e. there are only
finitely many distinct elements of type α
. The evidence of this
is a finset elems
(a list up to permutation without duplicates),
together with a proof that everything of type α
is in the list.
Instances
Equations
- Finset.boundedOrder = let src := inferInstanceAs (OrderBot (Finset α)); BoundedOrder.mk
Equations
- Finset.booleanAlgebra = GeneralizedBooleanAlgebra.toBooleanAlgebra
Note this is a special case of (finset.image_preimage f univ _).symm
.
Equations
- Fintype.decidablePiFintype f g = decidable_of_iff (∀ (a : α), a ∈ Fintype.elems → f a = g a) (_ : (∀ (a : α), a ∈ Fintype.elems → f a = g a) ↔ f = g)
Equations
- Fintype.decidableForallFintype = decidable_of_iff ((a : α) → a ∈ Finset.univ → p a) (_ : ((a : α) → a ∈ Finset.univ → p a) ↔ (a : α) → p a)
Equations
- Fintype.decidableMemRangeFintype f x = Fintype.decidableExistsFintype
Equations
- Fintype.decidableEqEquivFintype a b = decidable_of_iff (a.toFun = b.toFun) (_ : ↑a = ↑b ↔ a = b)
Equations
- Fintype.decidableEqEmbeddingFintype a b = decidable_of_iff (↑a = ↑b) (_ : ↑a = ↑b ↔ a = b)
Equations
- Fintype.decidableEqZeroHomFintype a b = decidable_of_iff (↑a = ↑b) (_ : ↑a = ↑b ↔ a = b)
Equations
- Fintype.decidableEqOneHomFintype a b = decidable_of_iff (↑a = ↑b) (_ : ↑a = ↑b ↔ a = b)
Equations
- Fintype.decidableEqAddHomFintype a b = decidable_of_iff (↑a = ↑b) (_ : ↑a = ↑b ↔ a = b)
Equations
- Fintype.decidableEqMulHomFintype a b = decidable_of_iff (↑a = ↑b) (_ : ↑a = ↑b ↔ a = b)
Equations
- Fintype.decidableEqAddMonoidHomFintype a b = decidable_of_iff (↑a = ↑b) (_ : ↑a = ↑b ↔ a = b)
Equations
- Fintype.decidableEqMonoidHomFintype a b = decidable_of_iff (↑a = ↑b) (_ : ↑a = ↑b ↔ a = b)
Equations
- Fintype.decidableEqMonoidWithZeroHomFintype a b = decidable_of_iff (↑a = ↑b) (_ : ↑a = ↑b ↔ a = b)
Equations
- Fintype.decidableEqRingHomFintype a b = decidable_of_iff (↑a = ↑b) (_ : ↑a = ↑b ↔ a = b)
Equations
- Fintype.decidableInjectiveFintype x = id inferInstance
Equations
- Fintype.decidableSurjectiveFintype x = id inferInstance
Equations
- Fintype.decidableBijectiveFintype x = id inferInstance
Equations
- Fintype.decidableRightInverseFintype f g = let_fun this := inferInstance; this
Equations
- Fintype.decidableLeftInverseFintype f g = let_fun this := inferInstance; this
Construct a proof of Fintype α
from a universal multiset
Equations
- Fintype.ofMultiset s H = { elems := Multiset.toFinset s, complete := (_ : ∀ (x : α), x ∈ Multiset.toFinset s) }
Construct a proof of Fintype α
from a universal list
Equations
- Fintype.ofList l H = { elems := List.toFinset l, complete := (_ : ∀ (x : α), x ∈ List.toFinset l) }
Construct a fintype from a finset with the same elements.
Equations
- Fintype.ofFinset s H = Fintype.subtype s H
If f : α → β→ β
is a bijection and α
is a fintype, then β
is also a fintype.
Equations
- One or more equations did not get rendered due to their size.
If f : α → β→ β
is a surjection and α
is a fintype, then β
is also a fintype.
Equations
- Fintype.ofSurjective f H = { elems := Finset.image f Finset.univ, complete := (_ : ∀ (b : β), b ∈ Finset.image f Finset.univ) }
Equations
- Finset.decidableCodisjoint = decidable_of_iff (∀ ⦃a : α⦄, ¬a ∈ s → a ∈ t) (_ : (∀ ⦃a : α⦄, ¬a ∈ s → a ∈ t) ↔ Codisjoint s t)
Equations
- Finset.decidableIsCompl = decidable_of_iff' (Disjoint s t ∧ Codisjoint s t) (_ : IsCompl s t ↔ Disjoint s t ∧ Codisjoint s t)
The inverse of an hf : injective
function f : α → β→ β
, of the type ↥(Set.range f) → α↥(Set.range f) → α→ α
.
This is the computable version of Function.invFun
that requires Fintype α
and DecidableEq β
,
or the function version of applying (Equiv.ofInjective f hf).symm
.
This function should not usually be used for actual computation because for most cases,
an explicit inverse can be stated that has better computational properties.
This function computes by checking all terms a : α
to find the f a = b
, so it is O(N) where
N = Fintype.card α
.
Equations
- Function.Injective.invOfMemRange hf b = Finset.choose (fun a => f a = ↑b) Finset.univ (_ : ∃! a, a ∈ Finset.univ ∧ (fun a => f a = ↑b) a)
The inverse of an embedding f : α ↪ β↪ β
, of the type ↥(Set.range f) → α↥(Set.range f) → α→ α
.
This is the computable version of Function.invFun
that requires Fintype α
and DecidableEq β
,
or the function version of applying (Equiv.ofInjective f f.injective).symm
.
This function should not usually be used for actual computation because for most cases,
an explicit inverse can be stated that has better computational properties.
This function computes by checking all terms a : α
to find the f a = b
, so it is O(N) where
N = Fintype.card α
.
Equations
Given an injective function to a fintype, the domain is also a fintype. This is noncomputable because injectivity alone cannot be used to construct preimages.
Equations
- Fintype.ofInjective f H = if hα : Nonempty α then Fintype.ofSurjective (Function.invFun f) (_ : Function.Surjective (Function.invFun f)) else { elems := ∅, complete := (_ : ∀ (x : α), x ∈ ∅) }
If f : α ≃ β≃ β
and α
is a fintype, then β
is also a fintype.
Equations
- Fintype.ofEquiv α f = Fintype.ofBijective ↑f (_ : Function.Bijective ↑f)
Any subsingleton type with a witness is a fintype (with one term).
Equations
- Fintype.ofSubsingleton a = { elems := {a}, complete := (_ : ∀ (x : α), x ∈ {a}) }
Note: this lemma is specifically about Fintype.of_isEmpty
. For a statement about
arbitrary Fintype
instances, use Finset.univ_eq_empty
.
Construct a finset enumerating a set s
, given a Fintype
instance.
Equations
- Set.toFinset s = Finset.map (Function.Embedding.subtype fun x => x ∈ s) Finset.univ
Membership of a set with a Fintype
instance is decidable.
Using this as an instance leads to potential loops with Subtype.fintype
under certain decidability
assumptions, so it should only be declared a local instance.
Equations
- Set.decidableMemOfFintype s a = decidable_of_iff (a ∈ Set.toFinset s) (_ : a ∈ Set.toFinset s ↔ a ∈ s)
Alias of the reverse direction of Set.toFinset_subset_toFinset
.
Alias of the reverse direction of Set.toFinset_ssubset_toFinset
.
Equations
- Fin.fintype n = { elems := { val := ↑(List.finRange n), nodup := (_ : List.Nodup (List.finRange n)) }, complete := (_ : ∀ (a : Fin n), a ∈ List.finRange n) }
Embed Fin n
into Fin (n + 1)
by prepending zero to the univ
Embed Fin n
into Fin (n + 1)
by appending a new Fin.last n
to the univ
Embed Fin n
into Fin (n + 1)
by inserting
around a specified pivot p : Fin (n + 1)
into the univ
Equations
- Unique.fintype = Fintype.ofSubsingleton default
Short-circuit instance to decrease search for Unique.fintype
,
since that relies on a subsingleton elimination for Unique
.
Equations
- Fintype.subtypeEq y = Fintype.subtype {y} (_ : ∀ (a : α), a ∈ {y} ↔ a = y)
Short-circuit instance to decrease search for Unique.fintype
,
since that relies on a subsingleton elimination for Unique
.
Equations
- Fintype.subtypeEq' y = Fintype.subtype {y} (_ : ∀ (a : α), a ∈ {y} ↔ y = a)
Equations
Equations
- Bool.fintype = { elems := { val := {true, false}, nodup := Bool.fintype.proof_1 }, complete := Bool.fintype.proof_2 }
Equations
- Additive.fintype = Fintype.ofEquiv α Additive.ofMul
Equations
- Multiplicative.fintype = Fintype.ofEquiv α Multiplicative.ofAdd
Given that α × β× β
is a fintype, α
is also a fintype.
Equations
- Fintype.prodLeft = { elems := Finset.image Prod.fst Finset.univ, complete := (_ : ∀ (a : α), a ∈ Finset.image Prod.fst Finset.univ) }
Given that α × β× β
is a fintype, β
is also a fintype.
Equations
- Fintype.prodRight = { elems := Finset.image Prod.snd Finset.univ, complete := (_ : ∀ (b : β), b ∈ Finset.image Prod.snd Finset.univ) }
Equations
- ULift.fintype α = Fintype.ofEquiv α (Equiv.symm Equiv.ulift)
Equations
- PLift.fintype α = Fintype.ofEquiv α (Equiv.symm Equiv.plift)
Equations
- OrderDual.fintype α = inst
Equations
Equations
- Lex.fintype α = inst
Fintype (s : Finset α)
#
Equations
- Finset.fintypeCoeSort s = { elems := Finset.attach s, complete := (_ : ∀ (x : { x // x ∈ s }), x ∈ Finset.attach s) }
Equations
- List.Subtype.fintype l = Fintype.ofList (List.attach l) (_ : ∀ (x : { x // x ∈ l }), x ∈ List.attach l)
Equations
- Multiset.Subtype.fintype s = Fintype.ofMultiset (Multiset.attach s) (_ : ∀ (x : { x // x ∈ s }), x ∈ Multiset.attach s)
Equations
- Finset.Subtype.fintype s = { elems := Finset.attach s, complete := (_ : ∀ (x : { x // x ∈ s }), x ∈ Finset.attach s) }
Equations
Equations
- Prop.fintype = { elems := { val := {True, False}, nodup := Prop.fintype.proof_1 }, complete := Prop.fintype.proof_2 }
Equations
- Subtype.fintype p = Fintype.subtype (Finset.filter p Finset.univ) (_ : ∀ (a : α), a ∈ Finset.filter p Finset.univ ↔ p a)
A set on a fintype, when coerced to a type, is a fintype.
Equations
- setFintype s = Subtype.fintype fun x => x ∈ s
In a GroupWithZero
α
, the unit group αˣ
is equivalent to the subtype of nonzero
elements.
Equations
- One or more equations did not get rendered due to their size.
Given Fintype α
, finsetEquivSet
is the equiv between Finset α
and Set α
. (All
sets on a finite type are finite.)
Equations
- One or more equations did not get rendered due to their size.
Equations
- Quotient.fintype s = Fintype.ofSurjective Quotient.mk'' (_ : ∀ (x : Quotient s), ∃ a, Quotient.mk'' a = x)
Given a fintype α
and a predicate p
, associate to a proof that there is a unique element of
α
satisfying p
this unique element, as an element of the corresponding subtype.
Equations
- Fintype.chooseX p hp = { val := Finset.choose p Finset.univ (_ : ∃! a, a ∈ Finset.univ ∧ p a), property := Fintype.chooseX.proof_2 p hp }
Given a fintype α
and a predicate p
, associate to a proof that there is a unique element of
α
satisfying p
this unique element, as an element of α
.
Equations
- Fintype.choose p hp = ↑(Fintype.chooseX p hp)
bijInv f
is the unique inverse to a bijection f
. This acts
as a computable alternative to Function.invFun
.
Equations
- Fintype.bijInv f_bij b = Fintype.choose (fun a => f a = b) (_ : ∃! a, (fun a => f a = b) a)
A Nonempty
Fintype
constructively contains an element.
Equations
- truncOfNonemptyFintype α = truncOfMultisetExistsMem Finset.univ.val (_ : ∃ x, x ∈ Finset.univ.val)
By iterating over the elements of a fintype, we can lift an existential statement ∃ a, P a∃ a, P a
to Trunc (Σ' a, P a)
, containing data.
Equations
- truncSigmaOfExists h = truncOfNonemptyFintype ((a : α) ×' P a)
Auxiliary definition to show exists_seq_of_forall_finset_exists
.
Equations
- seqOfForallFinsetExistsAux P r h x = Classical.choose (h (Finset.image (fun i => seqOfForallFinsetExistsAux P r h ↑i) Finset.univ))
Induction principle to build a sequence, by adding one point at a time satisfying a given relation with respect to all the previously chosen points.
More precisely, Assume that, for any finite set s
, one can find another point satisfying
some relation r
with respect to all the points in s
. Then one may construct a
function f : ℕ → α→ α
such that r (f m) (f n)
holds whenever m < n
.
We also ensure that all constructed points satisfy a given predicate P
.
Induction principle to build a sequence, by adding one point at a time satisfying a given symmetric relation with respect to all the previously chosen points.
More precisely, Assume that, for any finite set s
, one can find another point satisfying
some relation r
with respect to all the points in s
. Then one may construct a
function f : ℕ → α→ α
such that r (f m) (f n)
holds whenever m ≠ n≠ n
.
We also ensure that all constructed points satisfy a given predicate P
.