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)

Equations

• List.instDecidableInjOnToSetOfDecidableEq = decidable_of_iff (Multiset.map f s.val).Nodup ⋯

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

Equations

• List.instDecidableBijOnToSetOfDecidableEq = inferInstanceAs (Decidable (Set.MapsTo f ↑s ↑t' ∧ Set.InjOn f ↑s ∧ Set.SurjOn 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 α.

Equations

• Finset.univ = Fintype.elems

@[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}.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Fintype.decidablePiFintype f g = decidable_of_iff (∀ a ∈ Fintype.elems, f a = g a) ⋯

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

Equations

• Fintype.decidableForallFintype = decidable_of_iff (∀ a ∈ Finset.univ, p a) ⋯

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

Equations

• Fintype.decidableExistsFintype = decidable_of_iff (∃ a ∈ Finset.univ, p a) ⋯

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

Equations

• Fintype.decidableMemRangeFintype f x✝ = Fintype.decidableExistsFintype

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

Equations

• Fintype.decidableSubsingleton = decidable_of_iff (∀ a ∈ s, ∀ b ∈ s, a = b) ⋯

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

Equations

• Fintype.decidableEqEquivFintype a b = decidable_of_iff (a.toFun = b.toFun) ⋯

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

Equations

• Fintype.decidableEqEmbeddingFintype a b = decidable_of_iff (⇑a = ⇑b) ⋯

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

Equations

• Fintype.decidableInjectiveFintype f = decidable_of_iff (Multiset.map f Finset.univ.val).Nodup ⋯

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

Equations

• Fintype.decidableSurjectiveFintype x = id inferInstance

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

Equations

• Fintype.decidableBijectiveFintype x = id inferInstance

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

Equations

• Fintype.decidableRightInverseFintype f g = inferInstance

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

Equations

• Fintype.decidableLeftInverseFintype f g = inferInstance

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.

Equations

• Fintype.subtype s H = { elems := { val := Multiset.pmap Subtype.mk s.val ⋯, nodup := ⋯ }, complete := ⋯ }

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.

Equations

• Fintype.ofFinset s H = Fintype.subtype s H

instance Bool.fintype : Fintype Bool

Equations

• Bool.fintype = { elems := { val := {true, false}, nodup := Bool.fintype._proof_1 }, complete := Bool.fintype._proof_2 }

instance Ordering.fintype : Fintype Ordering

Equations

• Ordering.fintype = { elems := { val := {Ordering.lt, Ordering.eq, Ordering.gt}, nodup := Ordering.fintype._proof_1 }, complete := Ordering.fintype._proof_2 }

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

Equations

• OrderDual.fintype α = inst✝

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

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

Equations

• Lex.fintype α = inst✝