doc-next-gen

Mathlib.Data.Fintype.Defs

Module docstring

{"# 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. ","### Preparatory lemmas "}

Fintype structure
(α : Type*)
Full source 
/-- `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. -/
class Fintype (α : Type*) where
  /-- The `Finset` containing all elements of a `Fintype` -/
  elems : Finset α
  /-- A proof that `elems` contains every element of the type -/
  complete : ∀ x : α, x ∈ elems
Finite Type
Informal description
The structure `Fintype α` represents that the type `α` is finite, meaning there exists a finite set (specifically a `Finset`) containing all elements of type `α`. This is evidenced by a finset `elems` (a list without duplicates up to permutation) along with a proof that every element of type `α` is in this finset.
Finset.nodup_map_iff_injOn theorem
{f : α → β} {s : Finset α} : (Multiset.map f s.val).Nodup ↔ Set.InjOn f s
Full source 
theorem nodup_map_iff_injOn {f : α → β} {s : Finset α} :
    (Multiset.map f s.val).Nodup ↔ Set.InjOn f s := by
  simp [Multiset.nodup_map_iff_inj_on s.nodup, Set.InjOn]
Injectivity on Finite Sets via Multiset Mapping
Informal description
For any function $f : \alpha \to \beta$ and any finite set $s \subseteq \alpha$, the multiset obtained by mapping $f$ over $s$ has no duplicates if and only if $f$ is injective on $s$.
List.instDecidableInjOnToSetOfDecidableEq instance
[DecidableEq β] : Decidable (Set.InjOn f s)
Full source 
instance [DecidableEq β] : Decidable (Set.InjOn f s) :=
  -- Use custom implementation for better performance.
  decidable_of_iff ((Multiset.map f s.val).Nodup) Finset.nodup_map_iff_injOn
Decidability of Injectivity on a Set
Informal description
For any function $f : \alpha \to \beta$ and any set $s \subseteq \alpha$, if equality on $\beta$ is decidable, then the injectivity of $f$ on $s$ is decidable.
List.instDecidableBijOnToSetOfDecidableEq instance
[DecidableEq β] : Decidable (Set.BijOn f s t')
Full source 
instance [DecidableEq β] : Decidable (Set.BijOn f s t') :=
  inferInstanceAs (Decidable (_ ∧ _ ∧ _))
Decidability of Bijectivity on Sets with Decidable Equality
Informal description
For any function $f : \alpha \to \beta$ and sets $s \subseteq \alpha$, $t' \subseteq \beta$, if equality on $\beta$ is decidable, then the property that $f$ is bijective from $s$ to $t'$ is decidable. This means we can algorithmically determine whether $f$ maps $s$ into $t'$, is injective on $s$, and is surjective from $s$ to $t'$.
Finset.univ definition
: Finset α
Full source 
/-- `univ` is the universal finite set of type `Finset α` implied from
  the assumption `Fintype α`. -/
def univ : Finset α :=
  @Fintype.elems α _
Universal finite set of a finite type
Informal description
The universal finite set of type `Finset α`, which contains all elements of the finite type `α`. This is constructed using the `Fintype` instance for `α`, which provides a finite set containing every element of `α`.
Finset.mem_univ theorem
(x : α) : x ∈ (univ : Finset α)
Full source 
@[simp]
theorem mem_univ (x : α) : x ∈ (univ : Finset α) :=
  Fintype.complete x
Universal Membership in Finite Types
Informal description
For any element $x$ of a finite type $\alpha$, $x$ belongs to the universal finite set $\text{univ} : \text{Finset} \alpha$.
Finset.mem_univ_val theorem
: ∀ x, x ∈ (univ : Finset α).1
Full source 
theorem mem_univ_val : ∀ x, x ∈ (univ : Finset α).1 := by simp
Membership in Universal Finset's Underlying List
Informal description
For any element $x$ of a finite type $\alpha$, $x$ is contained in the underlying list of the universal finite set $\text{univ} : \text{Finset} \alpha$.
Finset.coe_univ theorem
: ↑(univ : Finset α) = (Set.univ : Set α)
Full source 
@[simp, norm_cast]
theorem coe_univ : ↑(univ : Finset α) = (Set.univ : Set α) := by ext; simp
Universal Finite Set Coerces to Universal Set
Informal description
The underlying set of the universal finite set `univ` of a finite type `α` is equal to the universal set `Set.univ` of `α`. In other words, the coercion of `Finset.univ` to a set is equal to the universal set containing all elements of `α`.
Finset.coe_eq_univ theorem
: (s : Set α) = Set.univ ↔ s = univ
Full source 
@[simp, norm_cast]
theorem coe_eq_univ : (s : Set α) = Set.univ ↔ s = univ := by rw [← coe_univ, coe_inj]
Equivalence of Universal Set and Universal Finset in Finite Types
Informal description
For any set $s$ of elements of a finite type $\alpha$, the set $s$ is equal to the universal set $\text{Set.univ}$ if and only if the underlying finset of $s$ is equal to the universal finset $\text{Finset.univ}$.
Finset.subset_univ theorem
(s : Finset α) : s ⊆ univ
Full source 
@[simp]
theorem subset_univ (s : Finset α) : s ⊆ univ := fun a _ => mem_univ a
Universal Finite Set Contains All Finite Subsets
Informal description
For any finite subset $s$ of a finite type $\alpha$, $s$ is a subset of the universal finite set $\text{univ} : \text{Finset} \alpha$.
Mathlib.Meta.elabFinsetBuilderSetOf definition
: TermElab
Full source 
/-- 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}`.
-/
@[term_elab setBuilder]
def elabFinsetBuilderSetOf : TermElab
  | `({ $x:ident | $p }), expectedType? => do
    -- If the expected type is not known to be `Finset ?α`, give up.
    unless ← knownToBeFinsetNotSet expectedType? do throwUnsupportedSyntax
    elabTerm (← `(Finset.filter (fun $x:ident ↦ $p) Finset.univ)) expectedType?
  | `({ $x:ident : $t | $p }), expectedType? => do
    -- If the expected type is not known to be `Finset ?α`, give up.
    unless ← knownToBeFinsetNotSet expectedType? do throwUnsupportedSyntax
    elabTerm (← `(Finset.filter (fun $x:ident : $t ↦ $p) Finset.univ)) expectedType?
  | `({ $x:ident ∉ $s:term | $p }), expectedType? => do
    -- If the expected type is known to be `Set ?α`, give up. If it is not known to be `Set ?α` or
    -- `Finset ?α`, check the expected type of `s`.
    unless ← knownToBeFinsetNotSet expectedType? do
      let ty ← try whnfR (← inferType (← elabTerm s none)) catch _ => throwUnsupportedSyntax
      -- If the expected type of `s` is not known to be `Finset ?α`, give up.
      match_expr ty with
      | Finset _ => pure ()
      | _ => throwUnsupportedSyntax
    -- Finally, we can elaborate the syntax as a finset.
    -- TODO: Seems a bit wasteful to have computed the expected type but still use `expectedType?`.
    elabTerm (← `(Finset.filter (fun $x:ident ↦ $p) $sᶜ)) expectedType?
  | `({ $x:ident ≠ $a | $p }), expectedType? => do
    -- If the expected type is not known to be `Finset ?α`, give up.
    unless ← knownToBeFinsetNotSet expectedType? do throwUnsupportedSyntax
    elabTerm (← `(Finset.filter (fun $x:ident ↦ $p) (singleton $a)ᶜ)) expectedType?
  | _, _ => throwUnsupportedSyntax
Finset set builder notation elaborator
Informal description
The elaborator for set builder notation in `Finset` translates expressions of the form: - `{x | p x}` to `Finset.filter (fun x ↦ p x) Finset.univ` - `{x : α | p x}` to `Finset.filter (fun x : α ↦ p x) Finset.univ` - `{x ∉ s | p x}` to `Finset.filter (fun x ↦ p x) sᶜ` (where `s` is a `Finset`) - `{x ≠ a | p x}` to `Finset.filter (fun x ↦ p x) {a}ᶜ` This elaborator handles cases where the expected type is known to be a `Finset` and not a `Set`.
Mathlib.Meta.delabFinsetFilter definition
: Delab
Full source 
/-- Delaborator for `Finset.filter`. The `pp.funBinderTypes` option controls whether
to show the domain type when the filter is over `Finset.univ`. -/
@[app_delab Finset.filter] def delabFinsetFilter : Delab :=
  whenPPOption getPPNotation do
  let #[_, p, _, t] := (← getExpr).getAppArgs | failure
  guardguard p.isLambda
  let i ← withNaryArg 1 <| withBindingBodyUnusedName (pure ⟨·⟩)
  let p ← withNaryArg 1 <| withBindingBody i.getId delab
  if t.isAppOfArity ``Finset.univ 2 then
    if ← getPPOption getPPFunBinderTypes then
      let ty ← withNaryArg 0 delab
      `({$i:ident : $ty | $p})
    else
      `({$i:ident | $p})
  -- check if `t` is of the form `s₀ᶜ`, in which case we display `x ∉ s₀` instead
  else if t.isAppOfArity ``HasCompl.compl 3 then
    let #[_, _, s₀] := t.getAppArgs | failure
    -- if `s₀` is a singleton, we can even use the notation `x ≠ a`
    if s₀.isAppOfArity ``Singleton.singleton 4 then
      let t ← withNaryArg 3 <| withNaryArg 2 <| withNaryArg 3 delab
      `({$i:ident ≠ $t | $p})
    else
      let t ← withNaryArg 3 <| withNaryArg 2 delab
      `({$i:ident ∉ $t | $p})
  else
    let t ← withNaryArg 3 delab
    `({$i:ident ∈ $t | $p})
Pretty-printer for Finset filter expressions
Informal description
The delaborator for `Finset.filter` expressions, which controls how filter operations on finite sets are pretty-printed. When the filter is applied to `Finset.univ`, it can display either as `{x | p x}` or `{x : α | p x}` depending on pretty-printing settings. For complement operations, it displays as `x ∉ s₀` or `x ≠ a` when appropriate.
Fintype.decidablePiFintype instance
{α} {β : α → Type*} [∀ a, DecidableEq (β a)] [Fintype α] : DecidableEq (∀ a, β a)
Full source 
instance decidablePiFintype {α} {β : α → Type*} [∀ a, DecidableEq (β a)] [Fintype α] :
    DecidableEq (∀ a, β a) := fun f g =>
  decidable_of_iff (∀ a ∈ @Fintype.elems α _, f a = g a)
    (by simp [funext_iff, Fintype.complete])
Decidable Equality for Functions on Finite Types
Informal description
For any finite type $\alpha$ and a family of types $\beta : \alpha \to \text{Type*}$ where each $\beta a$ has decidable equality, the function type $\forall a, \beta a$ also has decidable equality.
Fintype.decidableForallFintype instance
{p : α → Prop} [DecidablePred p] [Fintype α] : Decidable (∀ a, p a)
Full source 
instance decidableForallFintype {p : α → Prop} [DecidablePred p] [Fintype α] :
    Decidable (∀ a, p a) :=
  decidable_of_iff (∀ a ∈ @univ α _, p a) (by simp)
Decidability of Universal Quantifiers over Finite Types
Informal description
For any finite type $\alpha$ and predicate $p : \alpha \to \text{Prop}$ with decidable values, the universal statement $\forall a, p(a)$ is decidable.
Fintype.decidableExistsFintype instance
{p : α → Prop} [DecidablePred p] [Fintype α] : Decidable (∃ a, p a)
Full source 
instance decidableExistsFintype {p : α → Prop} [DecidablePred p] [Fintype α] :
    Decidable (∃ a, p a) :=
  decidable_of_iff (∃ a ∈ @univ α _, p a) (by simp)
Decidability of Existential Quantifiers over Finite Types
Informal description
For any finite type $\alpha$ and decidable predicate $p : \alpha \to \text{Prop}$, the existential statement $\exists a, p(a)$ is decidable.
Fintype.decidableMemRangeFintype instance
[Fintype α] [DecidableEq β] (f : α → β) : DecidablePred (· ∈ Set.range f)
Full source 
instance decidableMemRangeFintype [Fintype α] [DecidableEq β] (f : α → β) :
    DecidablePred (· ∈ Set.range f) := fun _ => Fintype.decidableExistsFintype
Decidability of Range Membership for Finite Types
Informal description
For any finite type $\alpha$, type $\beta$ with decidable equality, and function $f : \alpha \to \beta$, the predicate $\lambda x, x \in \text{range}(f)$ is decidable. That is, for any $y \in \beta$, we can algorithmically determine whether $y$ is in the range of $f$.
Fintype.decidableSubsingleton instance
[Fintype α] [DecidableEq α] {s : Set α} [DecidablePred (· ∈ s)] : Decidable s.Subsingleton
Full source 
instance decidableSubsingleton [Fintype α] [DecidableEq α] {s : Set α} [DecidablePred (· ∈ s)] :
    Decidable s.Subsingleton := decidable_of_iff (∀ a ∈ s, ∀ b ∈ s, a = b) Iff.rfl
Decidability of Subsingleton Property for Finite Sets
Informal description
For any finite type $\alpha$ with decidable equality and any subset $s$ of $\alpha$ with decidable membership, the property of $s$ being a subsingleton (i.e., containing at most one element) is decidable.
Fintype.decidableEqEquivFintype instance
[DecidableEq β] [Fintype α] : DecidableEq (α ≃ β)
Full source 
instance decidableEqEquivFintype [DecidableEq β] [Fintype α] : DecidableEq (α ≃ β) := fun a b =>
  decidable_of_iff (a.1 = b.1) Equiv.coe_fn_injective.eq_iff
Decidable Equality for Equivalences of Finite Types
Informal description
For any finite type $\alpha$ and any type $\beta$ with decidable equality, the type $\alpha \simeq \beta$ of equivalences (bijections with inverse) between $\alpha$ and $\beta$ has decidable equality.
Fintype.decidableEqEmbeddingFintype instance
[DecidableEq β] [Fintype α] : DecidableEq (α ↪ β)
Full source 
instance decidableEqEmbeddingFintype [DecidableEq β] [Fintype α] : DecidableEq (α ↪ β) := fun a b =>
  decidable_of_iff ((a : α → β) = b) Function.Embedding.coe_injective.eq_iff
Decidable Equality for Injective Embeddings of Finite Types
Informal description
For any finite type $\alpha$ and any type $\beta$ with decidable equality, the type $\alpha \hookrightarrow \beta$ of injective function embeddings from $\alpha$ to $\beta$ has decidable equality.
Fintype.nodup_map_univ_iff_injective theorem
[Fintype α] {f : α → β} : (Multiset.map f univ.val).Nodup ↔ Function.Injective f
Full source 
theorem nodup_map_univ_iff_injective [Fintype α] {f : α → β} :
    (Multiset.map f univ.val).Nodup ↔ Function.Injective f := by
  rw [nodup_map_iff_injOn, coe_univ, Set.injective_iff_injOn_univ]
Injectivity Characterization via Multiset Mapping on Finite Types
Informal description
For a finite type $\alpha$ and a function $f : \alpha \to \beta$, the multiset obtained by applying $f$ to all elements of $\alpha$ has no duplicates if and only if $f$ is injective.
Fintype.decidableInjectiveFintype instance
[DecidableEq β] [Fintype α] : DecidablePred (Injective : (α → β) → Prop)
Full source 
instance decidableInjectiveFintype [DecidableEq β] [Fintype α] :
    DecidablePred (Injective : (α → β) → Prop) :=
  -- Use custom implementation for better performance.
  fun f => decidable_of_iff ((Multiset.map f univ.val).Nodup) nodup_map_univ_iff_injective
Decidability of Injectivity for Functions from Finite Types
Informal description
For any finite type $\alpha$ and any type $\beta$ with decidable equality, the injectivity of a function $f : \alpha \to \beta$ is decidable.
Fintype.decidableSurjectiveFintype instance
[DecidableEq β] [Fintype α] [Fintype β] : DecidablePred (Surjective : (α → β) → Prop)
Full source 
instance decidableSurjectiveFintype [DecidableEq β] [Fintype α] [Fintype β] :
    DecidablePred (Surjective : (α → β) → Prop) := fun x => by unfold Surjective; infer_instance
Decidability of Surjectivity for Finite Types
Informal description
For any finite types $\alpha$ and $\beta$ with decidable equality on $\beta$, the surjectivity of a function $f : \alpha \to \beta$ is decidable.
Fintype.decidableBijectiveFintype instance
[DecidableEq β] [Fintype α] [Fintype β] : DecidablePred (Bijective : (α → β) → Prop)
Full source 
instance decidableBijectiveFintype [DecidableEq β] [Fintype α] [Fintype β] :
    DecidablePred (Bijective : (α → β) → Prop) := fun x => by unfold Bijective; infer_instance
Decidability of Bijectivity for Finite Types
Informal description
For any finite types $\alpha$ and $\beta$ with decidable equality on $\beta$, the bijectivity of a function $f : \alpha \to \beta$ is decidable.
Fintype.decidableRightInverseFintype instance
[DecidableEq α] [Fintype α] (f : α → β) (g : β → α) : Decidable (Function.RightInverse f g)
Full source 
instance decidableRightInverseFintype [DecidableEq α] [Fintype α] (f : α → β) (g : β → α) :
    Decidable (Function.RightInverse f g) :=
  show Decidable (∀ x, g (f x) = x) by infer_instance
Decidability of Right Inverses for Finite Types
Informal description
For any finite type $\alpha$ with decidable equality, and any function $f : \alpha \to \beta$ and $g : \beta \to \alpha$, it is decidable whether $g$ is a right inverse of $f$, i.e., whether $f \circ g = \text{id}_\beta$.
Fintype.decidableLeftInverseFintype instance
[DecidableEq β] [Fintype β] (f : α → β) (g : β → α) : Decidable (Function.LeftInverse f g)
Full source 
instance decidableLeftInverseFintype [DecidableEq β] [Fintype β] (f : α → β) (g : β → α) :
    Decidable (Function.LeftInverse f g) :=
  show Decidable (∀ x, f (g x) = x) by infer_instance
Decidability of Left Inverses for Finite Types
Informal description
For any finite type $\beta$ with decidable equality, and any functions $f : \alpha \to \beta$ and $g : \beta \to \alpha$, it is decidable whether $g$ is a left inverse of $f$, i.e., whether $g \circ f = \text{id}_\alpha$.
Fintype.instFastSubsingleton instance
(α : Type*) : Lean.Meta.FastSubsingleton (Fintype α)
Full source 
instance (α : Type*) : Lean.Meta.FastSubsingleton (Fintype α) := {}
Fast Uniqueness of Finite Type Structures
Informal description
For any type $\alpha$, the type of finite type structures on $\alpha$ is a fast subsingleton, meaning any two instances are equal and this can be determined quickly.
Fintype.subtype definition
{p : α → Prop} (s : Finset α) (H : ∀ x : α, x ∈ s ↔ p x) : Fintype { x // p x }
Full source 
/-- Given a predicate that can be represented by a finset, the subtype
associated to the predicate is a fintype. -/
protected def subtype {p : α → Prop} (s : Finset α) (H : ∀ x : α, x ∈ sx ∈ s ↔ p x) :
    Fintype { x // p x } :=
  ⟨⟨s.1.pmap Subtype.mk fun x => (H x).1, s.nodup.pmap fun _ _ _ _ => congr_arg Subtype.val⟩,
    fun ⟨x, px⟩ => Multiset.mem_pmap.2 ⟨x, (H x).2 px, rfl⟩⟩
Finite subtype defined by a predicate and a finset
Informal description
Given a predicate $p : \alpha \to \mathrm{Prop}$ and a finite set $s$ of elements of type $\alpha$ such that an element $x \in \alpha$ is in $s$ if and only if $p(x)$ holds, the subtype $\{x \mid p(x)\}$ is a finite type. The finite type structure is constructed by filtering the elements of $s$ that satisfy $p$ and proving that all elements of the subtype are contained in this filtered set.
Fintype.ofFinset definition
{p : Set α} (s : Finset α) (H : ∀ x, x ∈ s ↔ x ∈ p) : Fintype p
Full source 
/-- Construct a fintype from a finset with the same elements. -/
def ofFinset {p : Set α} (s : Finset α) (H : ∀ x, x ∈ sx ∈ s ↔ x ∈ p) : Fintype p :=
  Fintype.subtype s H
Finite type structure from a finset matching a set
Informal description
Given a set $p$ over a type $\alpha$ and a finite set $s$ of elements of $\alpha$ such that an element $x \in \alpha$ belongs to $s$ if and only if it belongs to $p$, the set $p$ can be endowed with a finite type structure. This is constructed by showing that $s$ contains all elements of $p$ and using the `Fintype.subtype` construction.
OrderDual.fintype instance
(α : Type*) [Fintype α] : Fintype αᵒᵈ
Full source 
instance OrderDual.fintype (α : Type*) [Fintype α] : Fintype αᵒᵈ :=
  ‹Fintype α›
Finite Order Dual
Informal description
For any finite type $\alpha$, the order dual $\alpha^{\mathrm{op}}$ is also finite.
OrderDual.finite instance
(α : Type*) [Finite α] : Finite αᵒᵈ
Full source 
instance OrderDual.finite (α : Type*) [Finite α] : Finite αᵒᵈ :=
  ‹Finite α›
Finite Types are Closed under Order Duality
Informal description
For any finite type $\alpha$, the order dual $\alpha^{\mathrm{op}}$ is also finite.
Lex.fintype instance
(α : Type*) [Fintype α] : Fintype (Lex α)
Full source 
instance Lex.fintype (α : Type*) [Fintype α] : Fintype (Lex α) :=
  ‹Fintype α›
Finite Type under Lexicographic Order
Informal description
For any finite type $\alpha$, the lexicographic order on $\alpha$ is also a finite type.