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 a Finset and a proof that all terms of type α are in it.
• Finset.univ: The finset of all elements of a fintype.

See Data.Fintype.Basic for elementary results, 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 as Fintype.subtype
• Option α are in Data.Fintype.Option
• α × β are in Data.Fintype.Prod
• α ⊕ β are in Data.Fintype.Sum
• Σ (a : α), β a are in Data.Fintype.Sigma

These files also contain appropriate Infinite instances for these types.

Infinite instances for ℕ, ℤ, Multiset α, and List α are in Data.Fintype.Lattice.

class Fintype (α : Type u_4) : Type u_4

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 α

  The Finset containing all elements of a Fintype

• complete (x : α) : x ∈ elems

  A proof that elems contains every element of the type

Preparatory lemmas

theorem Finset.nodup_map_iff_injOn {α : Type u_1} {β : Type u_2} {f : α → β} {s : Finset α} : (Multiset.map f s.val).Nodup ↔ Set.InjOn f ↑s

instance List.instDecidableInjOnToSetOfDecidableEq {α : Type u_1} {β : Type u_2} {f : α → β} {s : Finset α} [DecidableEq β] : Decidable (Set.InjOn f ↑s)

instance List.instDecidableBijOnToSetOfDecidableEq {α : Type u_1} {β : Type u_2} {f : α → β} {s : Finset α} {t' : Finset β} [DecidableEq β] : Decidable (Set.BijOn f ↑s ↑t')

def Finset.univ {α : Type u_1} [Fintype α] : Finset α

univ is the universal finite set of type Finset α implied from the assumption Fintype α.

@[simp]

theorem Finset.mem_univ {α : Type u_1} [Fintype α] (x : α) : x ∈ univ

theorem Finset.mem_univ_val {α : Type u_1} [Fintype α] (x : α) : x ∈ univ.val

theorem Finset.eq_univ_iff_forall {α : Type u_1} [Fintype α] {s : Finset α} : s = univ ↔ ∀ (x : α), x ∈ s

theorem Finset.eq_univ_of_forall {α : Type u_1} [Fintype α] {s : Finset α} : (∀ (x : α), x ∈ s) → s = univ

@[simp]

theorem Finset.coe_univ {α : Type u_1} [Fintype α] : ↑univ = Set.univ

@[simp]

theorem Finset.coe_eq_univ {α : Type u_1} [Fintype α] {s : Finset α} : ↑s = Set.univ ↔ s = univ

@[simp]

theorem Finset.subset_univ {α : Type u_1} [Fintype α] (s : Finset α) : s ⊆ univ

def Mathlib.Meta.elabFinsetBuilderSetOf : Lean.Elab.Term.TermElab

Elaborate set builder notation for Finset.

• {x | p x} is elaborated as Finset.filter (fun x ↦ p x) Finset.univ if the expected type is Finset ?α.
• {x : α | p x} is elaborated as Finset.filter (fun x : α ↦ p x) Finset.univ if the expected type is Finset ?α.
• {x ∉ s | p x} is elaborated as Finset.filter (fun x ↦ p x) sᶜ if either the expected type is Finset ?α or the expected type is not Set ?α and s has expected type Finset ?α.
• {x ≠ a | p x} is elaborated as Finset.filter (fun x ↦ p x) {a}ᶜ if the expected type is Finset ?α.

See also

• Data.Set.Defs for the Set builder notation elaborator that this elaborator partly overrides.
• Data.Finset.Basic for the Finset builder notation elaborator partly overriding this one for syntax of the form {x ∈ s | p x}.
• Data.Fintype.Basic for the Finset 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 the Finset builder notation elaborator handling syntax of the form {x ≤ a | p x}, {x ≥ a | p x}, {x < a | p x}, {x > a | p x}.

def Mathlib.Meta.delabFinsetFilter : Lean.PrettyPrinter.Delaborator.Delab

Delaborator for Finset.filter. The pp.funBinderTypes option controls whether to show the domain type when the filter is over Finset.univ.

instance Fintype.decidablePiFintype {α : Type u_5} {β : α → Type u_4} [(a : α) → DecidableEq (β a)] [Fintype α] : DecidableEq ((a : α) → β a)

instance Fintype.decidableForallFintype {α : Type u_1} {p : α → Prop} [DecidablePred p] [Fintype α] : Decidable (∀ (a : α), p a)

instance Fintype.decidableExistsFintype {α : Type u_1} {p : α → Prop} [DecidablePred p] [Fintype α] : Decidable (∃ (a : α), p a)

instance Fintype.decidableMemRangeFintype {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (f : α → β) : DecidablePred fun (x : β) => x ∈ Set.range f

instance Fintype.decidableSubsingleton {α : Type u_1} [Fintype α] [DecidableEq α] {s : Set α} [DecidablePred fun (x : α) => x ∈ s] : Decidable s.Subsingleton

instance Fintype.decidableEqEquivFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] : DecidableEq (α ≃ β)

instance Fintype.decidableEqEmbeddingFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] : DecidableEq (α ↪ β)

theorem Fintype.nodup_map_univ_iff_injective {α : Type u_1} {β : Type u_2} [Fintype α] {f : α → β} : (Multiset.map f Finset.univ.val).Nodup ↔ Function.Injective f

instance Fintype.decidableInjectiveFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] : DecidablePred Function.Injective

instance Fintype.decidableSurjectiveFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] [Fintype β] : DecidablePred Function.Surjective

instance Fintype.decidableBijectiveFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] [Fintype β] : DecidablePred Function.Bijective

instance Fintype.decidableRightInverseFintype {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] (f : α → β) (g : β → α) : Decidable (Function.RightInverse f g)

instance Fintype.decidableLeftInverseFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype β] (f : α → β) (g : β → α) : Decidable (Function.LeftInverse f g)

instance Fintype.subsingleton (α : Type u_4) : Subsingleton (Fintype α)

instance Fintype.instFastSubsingleton (α : Type u_4) : Lean.Meta.FastSubsingleton (Fintype α)

def Fintype.subtype {α : Type u_1} {p : α → Prop} (s : Finset α) (H : ∀ (x : α), x ∈ s ↔ p x) : Fintype { x : α // p x }

Given a predicate that can be represented by a finset, the subtype associated to the predicate is a fintype.

def Fintype.ofFinset {α : Type u_1} {p : Set α} (s : Finset α) (H : ∀ (x : α), x ∈ s ↔ x ∈ p) : Fintype ↑p

Construct a fintype from a finset with the same elements.

instance Bool.fintype : Fintype Bool

instance Ordering.fintype : Fintype Ordering

instance OrderDual.fintype (α : Type u_4) [Fintype α] : Fintype αᵒᵈ

instance OrderDual.finite (α : Type u_4) [Finite α] : Finite αᵒᵈ

instance Lex.fintype (α : Type u_4) [Fintype α] : Fintype (Lex α)