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
.
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.
- elems : Finset α
- complete : ∀ (x : α), x ∈ Fintype.elems
A proof that
elems
contains every element of the type
Instances
Equations
- Finset.boundedOrder = BoundedOrder.mk
Equations
- Finset.booleanAlgebra = GeneralizedBooleanAlgebra.toBooleanAlgebra
Elaborate set builder notation for Finset
.
{x | p x}
is elaborated asFinset.filter (fun x ↦ p x) Finset.univ
if the expected type isFinset ?α
.{x : α | p x}
is elaborated asFinset.filter (fun x : α ↦ p x) Finset.univ
if the expected type isFinset ?α
.{x ∉ s | p x}
is elaborated asFinset.filter (fun x ↦ p x) sᶜ
if either the expected type isFinset ?α
or the expected type is notSet ?α
ands
has expected typeFinset ?α
.{x ≠ a | p x}
is elaborated asFinset.filter (fun x ↦ p x) {a}ᶜ
if the expected type isFinset ?α
.
See also
Data.Set.Defs
for theSet
builder notation elaborator that this elaborator partly overrides.Data.Finset.Basic
for theFinset
builder notation elaborator partly overriding this one for syntax of the form{x ∈ s | p x}
.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
Note this is a special case of (Finset.image_preimage f univ _).symm
.
Equations
- Fintype.decidablePiFintype f g = decidable_of_iff (∀ a ∈ Fintype.elems, f a = g a) ⋯
Equations
- Fintype.decidableForallFintype = decidable_of_iff (∀ a ∈ Finset.univ, p a) ⋯
Equations
- Fintype.decidableExistsFintype = decidable_of_iff (∃ a ∈ Finset.univ, p a) ⋯
Equations
- Fintype.decidableMemRangeFintype f x = Fintype.decidableExistsFintype
Equations
- Fintype.decidableSubsingleton = decidable_of_iff (∀ a ∈ s, ∀ b ∈ s, a = b) ⋯
Equations
- Fintype.decidableEqEquivFintype a b = decidable_of_iff (a.toFun = b.toFun) ⋯
Equations
- Fintype.decidableEqEmbeddingFintype a b = decidable_of_iff (⇑a = ⇑b) ⋯
Equations
- Fintype.decidableEqMulEquivFintype a b = decidable_of_iff (⇑a = ⇑b) ⋯
Equations
- Fintype.decidableEqAddEquivFintype a b = decidable_of_iff (⇑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 = inferInstance
Equations
- Fintype.decidableLeftInverseFintype f g = inferInstance
Construct a proof of Fintype α
from a universal multiset
Equations
- Fintype.ofMultiset s H = { elems := s.toFinset, complete := ⋯ }
Instances For
Construct a proof of Fintype α
from a universal list
Equations
- Fintype.ofList l H = { elems := l.toFinset, complete := ⋯ }
Instances For
Given a predicate that can be represented by a finset, the subtype associated to the predicate is a fintype.
Equations
- Fintype.subtype s H = { elems := { val := Multiset.pmap Subtype.mk s.val ⋯, nodup := ⋯ }, complete := ⋯ }
Instances For
Construct a fintype from a finset with the same elements.
Equations
- Fintype.ofFinset s H = Fintype.subtype s H
Instances For
If f : α → β
is a bijection and α
is a fintype, then β
is also a fintype.
Equations
- Fintype.ofBijective f H = { elems := Finset.map { toFun := f, inj' := ⋯ } Finset.univ, complete := ⋯ }
Instances For
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 := ⋯ }
Instances For
Equations
- Finset.decidableCodisjoint = decidable_of_iff (∀ ⦃a : α⦄, a ∉ s → a ∈ t) ⋯
Equations
- Finset.decidableIsCompl = decidable_of_iff' (Disjoint s t ∧ Codisjoint s t) ⋯
The inverse of an hf : injective
function f : α → β
, of the type ↥(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
- hf.invOfMemRange b = Finset.choose (fun (a : α) => f a = ↑b) Finset.univ ⋯
Instances For
The inverse of an embedding f : α ↪ β
, of the type ↥(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
- f.invOfMemRange b = ⋯.invOfMemRange b
Instances For
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) ⋯ else { elems := ∅, complete := ⋯ }
Instances For
If f : α ≃ β
and α
is a fintype, then β
is also a fintype.
Equations
- Fintype.ofEquiv α f = Fintype.ofBijective ⇑f ⋯
Instances For
Any subsingleton type with a witness is a fintype (with one term).
Equations
- Fintype.ofSubsingleton a = { elems := {a}, complete := ⋯ }
Instances For
An empty type is a fintype. Not registered as an instance, to make sure that there aren't two
conflicting Fintype ι
instances around when casing over whether a fintype ι
is empty or not.
Instances For
Note: this lemma is specifically about Fintype.ofIsEmpty
. For a statement about
arbitrary Fintype
instances, use Finset.univ_eq_empty
.
Equations
- Fintype.instPEmpty = Fintype.ofIsEmpty
Construct a finset enumerating a set s
, given a Fintype
instance.
Equations
- s.toFinset = Finset.map (Function.Embedding.subtype fun (x : α) => x ∈ s) Finset.univ
Instances For
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
- s.decidableMemOfFintype a = decidable_of_iff (a ∈ s.toFinset) ⋯
Instances For
Alias of the reverse direction of Set.toFinset_nonempty
.
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 := ⋯ }, complete := ⋯ }
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} ⋯
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} ⋯
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 := ⋯ }
Instances For
Given that α × β
is a fintype, β
is also a fintype.
Equations
- Fintype.prodRight = { elems := Finset.image Prod.snd Finset.univ, complete := ⋯ }
Instances For
Equations
- ULift.fintype α = Fintype.ofEquiv α Equiv.ulift.symm
Equations
- PLift.fintype α = Fintype.ofEquiv α Equiv.plift.symm
Equations
- OrderDual.fintype α = inst
Equations
- List.Subtype.fintype l = Fintype.ofList l.attach ⋯
Equations
- Multiset.Subtype.fintype s = Fintype.ofMultiset s.attach ⋯
Equations
- Finset.Subtype.fintype s = { elems := s.attach, complete := ⋯ }
Equations
Equations
- PLift.fintypeProp p = { elems := if h : p then {{ down := h }} else ∅, complete := ⋯ }
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 set on a fintype, when coerced to a type, is a fintype.
Equations
- setFintype s = Subtype.fintype fun (x : α) => x ∈ s
Instances For
Given Fintype α
, finsetEquivSet
is the equiv between Finset α
and Set α
. (All
sets on a finite type are finite.)
Equations
Instances For
Given a fintype α
, finsetOrderIsoSet
is the order isomorphism between Finset α
and Set α
(all sets on a finite type are finite).
Equations
- Fintype.finsetOrderIsoSet = { toEquiv := Fintype.finsetEquivSet, map_rel_iff' := ⋯ }
Instances For
Equations
- Quotient.fintype s = Fintype.ofSurjective Quotient.mk'' ⋯
Equations
- PSigma.fintypePropLeft = if h : α then Fintype.ofEquiv (β h) { toFun := fun (x : β h) => ⟨h, x⟩, invFun := PSigma.snd, left_inv := ⋯, right_inv := ⋯ } else { elems := ∅, complete := ⋯ }
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 = ⟨Finset.choose p Finset.univ ⋯, ⋯⟩
Instances For
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)
Instances For
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) ⋯
Instances For
A Nonempty
Fintype
constructively contains an element.
Equations
- truncOfNonemptyFintype α = truncOfMultisetExistsMem Finset.univ.val ⋯
Instances For
By iterating over the elements of a fintype, we can lift an existential statement ∃ a, P a
to Trunc (Σ' a, P a)
, containing data.
Equations
- truncSigmaOfExists h = truncOfNonemptyFintype ((a : α) ×' P a)
Instances For
For functions on finite sets, they are bijections iff they map universes into universes.
Auxiliary definition to show exists_seq_of_forall_finset_exists
.
Equations
- seqOfForallFinsetExistsAux P r h x = Classical.choose ⋯
Instances For
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
.
We also ensure that all constructed points satisfy a given predicate P
.
finset% t
elaborates t
as a Finset
.
If t
is a Set
, then inserts Set.toFinset
.
Does not make use of the expected type; useful for big operators over finsets.
#check finset% Finset.range 2 -- Finset Nat
#check finset% (Set.univ : Set Bool) -- Finset Bool
Equations
- finsetStx = Lean.ParserDescr.node `finsetStx 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "finset% ") (Lean.ParserDescr.cat `term 0))
Instances For
quot_precheck
for the finset%
syntax.
Equations
- One or more equations did not get rendered due to their size.