Documentation

Mathlib.Data.Fintype.Basic

Finite types #

This file defines a typeclass to state that a type is finite.

Main declarations #

See Data.Fintype.Card for the cardinality of a fintype, the equivalence with Fin (Fintype.card α), and pigeonhole principles.

Instances #

Instances for Fintype for

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.

class Fintype (α : Type u_4) :
Type u_4
  • elems : Finset α

    The Finset containing all elements of a Fintype

  • complete : ∀ (x : α), x Fintype.elems

    A proof that elems contains every element of the type

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
    def Finset.univ {α : Type u_1} [Fintype α] :

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

    Equations
    • Finset.univ = Fintype.elems
    Instances For
      @[simp]
      theorem Finset.mem_univ {α : Type u_1} [Fintype α] (x : α) :
      x Finset.univ
      theorem Finset.mem_univ_val {α : Type u_1} [Fintype α] (x : α) :
      x Finset.univ.val
      theorem Finset.eq_univ_iff_forall {α : Type u_1} [Fintype α] {s : Finset α} :
      s = Finset.univ ∀ (x : α), x s
      theorem Finset.eq_univ_of_forall {α : Type u_1} [Fintype α] {s : Finset α} :
      (∀ (x : α), x s) → s = Finset.univ
      @[simp]
      theorem Finset.coe_univ {α : Type u_1} [Fintype α] :
      Finset.univ = Set.univ
      @[simp]
      theorem Finset.coe_eq_univ {α : Type u_1} [Fintype α] {s : Finset α} :
      s = Set.univ s = Finset.univ
      theorem Finset.Nonempty.eq_univ {α : Type u_1} [Fintype α] {s : Finset α} [Subsingleton α] :
      Finset.Nonempty ss = Finset.univ
      theorem Finset.univ_nonempty_iff {α : Type u_1} [Fintype α] :
      theorem Finset.univ_nonempty {α : Type u_1} [Fintype α] [Nonempty α] :
      Finset.Nonempty Finset.univ
      theorem Finset.univ_eq_empty_iff {α : Type u_1} [Fintype α] :
      Finset.univ = IsEmpty α
      @[simp]
      theorem Finset.univ_eq_empty {α : Type u_1} [Fintype α] [IsEmpty α] :
      Finset.univ =
      @[simp]
      theorem Finset.univ_unique {α : Type u_1} [Fintype α] [Unique α] :
      Finset.univ = {default}
      @[simp]
      theorem Finset.subset_univ {α : Type u_1} [Fintype α] (s : Finset α) :
      s Finset.univ
      instance Finset.boundedOrder {α : Type u_1} [Fintype α] :
      Equations
      @[simp]
      theorem Finset.top_eq_univ {α : Type u_1} [Fintype α] :
      = Finset.univ
      theorem Finset.ssubset_univ_iff {α : Type u_1} [Fintype α] {s : Finset α} :
      s Finset.univ s Finset.univ
      theorem Finset.codisjoint_left {α : Type u_1} [Fintype α] {s : Finset α} {t : Finset α} :
      Codisjoint s t ∀ ⦃a : α⦄, ¬a sa t
      theorem Finset.codisjoint_right {α : Type u_1} [Fintype α] {s : Finset α} {t : Finset α} :
      Codisjoint s t ∀ ⦃a : α⦄, ¬a ta s
      Equations
      • Finset.booleanAlgebra = GeneralizedBooleanAlgebra.toBooleanAlgebra
      theorem Finset.sdiff_eq_inter_compl {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) (t : Finset α) :
      s \ t = s t
      theorem Finset.compl_eq_univ_sdiff {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
      s = Finset.univ \ s
      @[simp]
      theorem Finset.mem_compl {α : Type u_1} [Fintype α] {s : Finset α} [DecidableEq α] {a : α} :
      a s ¬a s
      theorem Finset.not_mem_compl {α : Type u_1} [Fintype α] {s : Finset α} [DecidableEq α] {a : α} :
      ¬a s a s
      @[simp]
      theorem Finset.coe_compl {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
      s = (s)
      @[simp]
      theorem Finset.compl_subset_compl {α : Type u_1} [Fintype α] {s : Finset α} {t : Finset α} [DecidableEq α] :
      s t t s
      @[simp]
      theorem Finset.compl_ssubset_compl {α : Type u_1} [Fintype α] {s : Finset α} {t : Finset α} [DecidableEq α] :
      s t t s
      @[simp]
      theorem Finset.compl_empty {α : Type u_1} [Fintype α] [DecidableEq α] :
      = Finset.univ
      @[simp]
      theorem Finset.compl_univ {α : Type u_1} [Fintype α] [DecidableEq α] :
      Finset.univ =
      @[simp]
      theorem Finset.compl_eq_empty_iff {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
      s = s = Finset.univ
      @[simp]
      theorem Finset.compl_eq_univ_iff {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
      s = Finset.univ s =
      @[simp]
      theorem Finset.union_compl {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
      s s = Finset.univ
      @[simp]
      theorem Finset.inter_compl {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
      @[simp]
      theorem Finset.compl_union {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) (t : Finset α) :
      (s t) = s t
      @[simp]
      theorem Finset.compl_inter {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) (t : Finset α) :
      (s t) = s t
      @[simp]
      theorem Finset.compl_erase {α : Type u_1} [Fintype α] {s : Finset α} [DecidableEq α] {a : α} :
      @[simp]
      theorem Finset.compl_insert {α : Type u_1} [Fintype α] {s : Finset α} [DecidableEq α] {a : α} :
      theorem Finset.insert_compl_insert {α : Type u_1} [Fintype α] {s : Finset α} [DecidableEq α] {a : α} (ha : ¬a s) :
      @[simp]
      theorem Finset.insert_compl_self {α : Type u_1} [Fintype α] [DecidableEq α] (x : α) :
      insert x {x} = Finset.univ
      @[simp]
      theorem Finset.compl_filter {α : Type u_1} [Fintype α] [DecidableEq α] (p : αProp) [DecidablePred p] [(x : α) → Decidable ¬p x] :
      (Finset.filter p Finset.univ) = Finset.filter (fun x => ¬p x) Finset.univ
      theorem Finset.compl_ne_univ_iff_nonempty {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
      s Finset.univ Finset.Nonempty s
      theorem Finset.compl_singleton {α : Type u_1} [Fintype α] [DecidableEq α] (a : α) :
      {a} = Finset.erase Finset.univ a
      theorem Finset.insert_inj_on' {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
      Set.InjOn (fun a => insert a s) s
      theorem Finset.image_univ_of_surjective {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] {f : βα} (hf : Function.Surjective f) :
      Finset.image f Finset.univ = Finset.univ
      @[simp]
      theorem Finset.image_univ_equiv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] (f : β α) :
      Finset.image (f) Finset.univ = Finset.univ
      @[simp]
      theorem Finset.univ_inter {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
      Finset.univ s = s
      @[simp]
      theorem Finset.inter_univ {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
      s Finset.univ = s
      @[simp]
      theorem Finset.inter_eq_univ {α : Type u_1} [Fintype α] {s : Finset α} {t : Finset α} [DecidableEq α] :
      s t = Finset.univ s = Finset.univ t = Finset.univ
      theorem Finset.map_univ_of_surjective {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {f : β α} (hf : Function.Surjective f) :
      Finset.map f Finset.univ = Finset.univ
      @[simp]
      theorem Finset.map_univ_equiv {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : β α) :
      Finset.map (Equiv.toEmbedding f) Finset.univ = Finset.univ
      @[simp]
      theorem Finset.piecewise_univ {α : Type u_1} [Fintype α] [(i : α) → Decidable (i Finset.univ)] {δ : αSort u_4} (f : (i : α) → δ i) (g : (i : α) → δ i) :
      Finset.piecewise Finset.univ f g = f
      theorem Finset.piecewise_compl {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) [(i : α) → Decidable (i s)] [(i : α) → Decidable (i s)] {δ : αSort u_4} (f : (i : α) → δ i) (g : (i : α) → δ i) :
      @[simp]
      theorem Finset.piecewise_erase_univ {α : Type u_1} [Fintype α] {δ : αSort u_4} [DecidableEq α] (a : α) (f : (a : α) → δ a) (g : (a : α) → δ a) :
      Finset.piecewise (Finset.erase Finset.univ a) f g = Function.update f a (g a)
      theorem Finset.univ_map_equiv_to_embedding {α : Type u_4} {β : Type u_5} [Fintype α] [Fintype β] (e : α β) :
      Finset.map (Equiv.toEmbedding e) Finset.univ = Finset.univ
      @[simp]
      theorem Finset.univ_filter_exists {α : Type u_1} {β : Type u_2} [Fintype α] (f : αβ) [Fintype β] [DecidablePred fun y => x, f x = y] [DecidableEq β] :
      Finset.filter (fun y => x, f x = y) Finset.univ = Finset.image f Finset.univ
      theorem Finset.univ_filter_mem_range {α : Type u_1} {β : Type u_2} [Fintype α] (f : αβ) [Fintype β] [DecidablePred fun y => y Set.range f] [DecidableEq β] :
      Finset.filter (fun y => y Set.range f) Finset.univ = Finset.image f Finset.univ

      Note this is a special case of (Finset.image_preimage f univ _).symm.

      theorem Finset.coe_filter_univ {α : Type u_1} [Fintype α] (p : αProp) [DecidablePred p] :
      ↑(Finset.filter p Finset.univ) = {x | p x}
      @[simp]
      theorem Finset.subtype_eq_univ {α : Type u_1} {s : Finset α} {p : αProp} [DecidablePred p] [Fintype { a // p a }] :
      Finset.subtype p s = Finset.univ ∀ ⦃a : α⦄, p aa s
      @[simp]
      theorem Finset.subtype_univ {α : Type u_1} [Fintype α] (p : αProp) [DecidablePred p] [Fintype { a // p a }] :
      Finset.subtype p Finset.univ = Finset.univ
      instance Fintype.decidablePiFintype {α : Type u_5} {β : αType u_4} [(a : α) → DecidableEq (β a)] [Fintype α] :
      DecidableEq ((a : α) → β a)
      Equations
      instance Fintype.decidableForallFintype {α : Type u_1} {p : αProp} [DecidablePred p] [Fintype α] :
      Decidable ((a : α) → p a)
      Equations
      • Fintype.decidableForallFintype = decidable_of_iff ((a : α) → a Finset.univp a) (_ : ((a : α) → a Finset.univp a) (a : α) → p a)
      instance Fintype.decidableExistsFintype {α : Type u_1} {p : αProp} [DecidablePred p] [Fintype α] :
      Decidable (a, p a)
      Equations
      instance Fintype.decidableMemRangeFintype {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (f : αβ) :
      Equations
      instance Fintype.decidableEqEquivFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] :
      Equations
      instance Fintype.decidableEqEmbeddingFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] :
      Equations
      theorem Fintype.decidableEqZeroHomFintype.proof_1 {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] (a : ZeroHom α β) (b : ZeroHom α β) :
      a = b a = b
      instance Fintype.decidableEqZeroHomFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] [Zero α] [Zero β] :
      Equations
      instance Fintype.decidableEqOneHomFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] [One α] [One β] :
      Equations
      theorem Fintype.decidableEqAddHomFintype.proof_1 {α : Type u_1} {β : Type u_2} [Add α] [Add β] (a : AddHom α β) (b : AddHom α β) :
      a = b a = b
      instance Fintype.decidableEqAddHomFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] [Add α] [Add β] :
      Equations
      instance Fintype.decidableEqMulHomFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] [Mul α] [Mul β] :
      Equations
      Equations
      theorem Fintype.decidableEqAddMonoidHomFintype.proof_1 {α : Type u_1} {β : Type u_2} [AddZeroClass α] [AddZeroClass β] (a : α →+ β) (b : α →+ β) :
      a = b a = b
      instance Fintype.decidableEqMonoidHomFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] [MulOneClass α] [MulOneClass β] :
      Equations
      instance Fintype.decidableEqRingHomFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] [Semiring α] [Semiring β] :
      Equations
      instance Fintype.decidableInjectiveFintype {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] [Fintype α] :
      DecidablePred Function.Injective
      Equations
      instance Fintype.decidableSurjectiveFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] [Fintype β] :
      DecidablePred Function.Surjective
      Equations
      instance Fintype.decidableBijectiveFintype {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] [Fintype α] [Fintype β] :
      DecidablePred Function.Bijective
      Equations
      instance Fintype.decidableRightInverseFintype {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] (f : αβ) (g : βα) :
      Equations
      instance Fintype.decidableLeftInverseFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype β] (f : αβ) (g : βα) :
      Equations
      def Fintype.ofMultiset {α : Type u_1} [DecidableEq α] (s : Multiset α) (H : ∀ (x : α), x s) :

      Construct a proof of Fintype α from a universal multiset

      Equations
      Instances For
        def Fintype.ofList {α : Type u_1} [DecidableEq α] (l : List α) (H : ∀ (x : α), x l) :

        Construct a proof of Fintype α from a universal list

        Equations
        Instances For
          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
          • One or more equations did not get rendered due to their size.
          Instances For
            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
            Instances For
              def Fintype.ofBijective {α : Type u_1} {β : Type u_2} [Fintype α] (f : αβ) (H : Function.Bijective f) :

              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.
              Instances For
                def Fintype.ofSurjective {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] (f : αβ) (H : Function.Surjective f) :

                If f : α → β is a surjection and α is a fintype, then β is also a fintype.

                Equations
                Instances For
                  instance Finset.decidableCodisjoint {α : Type u_1} [Fintype α] [DecidableEq α] {s : Finset α} {t : Finset α} :
                  Equations
                  instance Finset.decidableIsCompl {α : Type u_1} [Fintype α] [DecidableEq α] {s : Finset α} {t : Finset α} :
                  Equations
                  def Function.Injective.invOfMemRange {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : αβ} (hf : Function.Injective f) :
                  ↑(Set.range f)α

                  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
                  Instances For
                    theorem Function.Injective.left_inv_of_invOfMemRange {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : αβ} (hf : Function.Injective f) (b : ↑(Set.range f)) :
                    @[simp]
                    theorem Function.Injective.right_inv_of_invOfMemRange {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : αβ} (hf : Function.Injective f) (a : α) :
                    Function.Injective.invOfMemRange hf { val := f a, property := (_ : f a Set.range f) } = a
                    def Function.Embedding.invOfMemRange {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (f : α β) (b : ↑(Set.range f)) :
                    α

                    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
                    Instances For
                      @[simp]
                      theorem Function.Embedding.left_inv_of_invOfMemRange {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (f : α β) (b : ↑(Set.range f)) :
                      @[simp]
                      theorem Function.Embedding.right_inv_of_invOfMemRange {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (f : α β) (a : α) :
                      Function.Embedding.invOfMemRange f { val := f a, property := (_ : f a Set.range f) } = a
                      noncomputable def Fintype.ofInjective {α : Type u_1} {β : Type u_2} [Fintype β] (f : αβ) (H : Function.Injective f) :

                      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
                      Instances For
                        def Fintype.ofEquiv {β : Type u_2} (α : Type u_4) [Fintype α] (f : α β) :

                        If f : α ≃ β and α is a fintype, then β is also a fintype.

                        Equations
                        Instances For
                          def Fintype.ofSubsingleton {α : Type u_1} (a : α) [Subsingleton α] :

                          Any subsingleton type with a witness is a fintype (with one term).

                          Equations
                          Instances For
                            @[simp]
                            theorem Fintype.univ_ofSubsingleton {α : Type u_1} (a : α) [Subsingleton α] :
                            Finset.univ = {a}
                            instance Fintype.ofIsEmpty {α : Type u_1} [IsEmpty α] :
                            Equations
                            • Fintype.ofIsEmpty = { elems := , complete := (_ : ∀ (a : α), a ) }
                            @[simp]
                            theorem Fintype.univ_of_isEmpty {α : Type u_1} [IsEmpty α] :
                            Finset.univ =

                            Note: this lemma is specifically about Fintype.of_isEmpty. For a statement about arbitrary Fintype instances, use Finset.univ_eq_empty.

                            def Set.toFinset {α : Type u_1} (s : Set α) [Fintype s] :

                            Construct a finset enumerating a set s, given a Fintype instance.

                            Equations
                            Instances For
                              theorem Set.toFinset_congr {α : Type u_1} {s : Set α} {t : Set α} [Fintype s] [Fintype t] (h : s = t) :
                              @[simp]
                              theorem Set.mem_toFinset {α : Type u_1} {s : Set α} [Fintype s] {a : α} :
                              theorem Set.toFinset_ofFinset {α : Type u_1} {p : Set α} (s : Finset α) (H : ∀ (x : α), x s x p) :

                              Many Fintype instances for sets are defined using an extensionally equal Finset. Rewriting s.toFinset with Set.toFinset_ofFinset replaces the term with such a Finset.

                              def Set.decidableMemOfFintype {α : Type u_1} [DecidableEq α] (s : Set α) [Fintype s] (a : α) :

                              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
                              Instances For
                                @[simp]
                                theorem Set.coe_toFinset {α : Type u_1} (s : Set α) [Fintype s] :
                                ↑(Set.toFinset s) = s
                                @[simp]
                                @[simp]
                                theorem Set.toFinset_inj {α : Type u_1} {s : Set α} {t : Set α} [Fintype s] [Fintype t] :
                                theorem Set.toFinset_subset_toFinset {α : Type u_1} {s : Set α} {t : Set α} [Fintype s] [Fintype t] :
                                @[simp]
                                theorem Set.toFinset_ssubset {α : Type u_1} {s : Set α} [Fintype s] {t : Finset α} :
                                Set.toFinset s t s t
                                @[simp]
                                theorem Set.subset_toFinset {α : Type u_1} {t : Set α} {s : Finset α} [Fintype t] :
                                s Set.toFinset t s t
                                @[simp]
                                theorem Set.ssubset_toFinset {α : Type u_1} {t : Set α} {s : Finset α} [Fintype t] :
                                s Set.toFinset t s t
                                theorem Set.toFinset_ssubset_toFinset {α : Type u_1} {s : Set α} {t : Set α} [Fintype s] [Fintype t] :
                                @[simp]
                                theorem Set.toFinset_subset {α : Type u_1} {s : Set α} [Fintype s] {t : Finset α} :
                                Set.toFinset s t s t
                                theorem Set.toFinset_mono {α : Type u_1} {s : Set α} {t : Set α} [Fintype s] [Fintype t] :

                                Alias of the reverse direction of Set.toFinset_subset_toFinset.

                                theorem Set.toFinset_strict_mono {α : Type u_1} {s : Set α} {t : Set α} [Fintype s] [Fintype t] :

                                Alias of the reverse direction of Set.toFinset_ssubset_toFinset.

                                @[simp]
                                theorem Set.disjoint_toFinset {α : Type u_1} {s : Set α} {t : Set α} [Fintype s] [Fintype t] :
                                @[simp]
                                theorem Set.toFinset_inter {α : Type u_1} (s : Set α) (t : Set α) [DecidableEq α] [Fintype s] [Fintype t] [Fintype ↑(s t)] :
                                @[simp]
                                theorem Set.toFinset_union {α : Type u_1} (s : Set α) (t : Set α) [DecidableEq α] [Fintype s] [Fintype t] [Fintype ↑(s t)] :
                                @[simp]
                                theorem Set.toFinset_diff {α : Type u_1} (s : Set α) (t : Set α) [DecidableEq α] [Fintype s] [Fintype t] [Fintype ↑(s \ t)] :
                                @[simp]
                                theorem Set.toFinset_symmDiff {α : Type u_1} (s : Set α) (t : Set α) [DecidableEq α] [Fintype s] [Fintype t] [Fintype ↑(s t)] :
                                @[simp]
                                theorem Set.toFinset_compl {α : Type u_1} (s : Set α) [DecidableEq α] [Fintype s] [Fintype α] [Fintype s] :
                                @[simp]
                                @[simp]
                                theorem Set.toFinset_univ {α : Type u_1} [Fintype α] [Fintype Set.univ] :
                                Set.toFinset Set.univ = Finset.univ
                                @[simp]
                                theorem Set.toFinset_eq_empty {α : Type u_1} {s : Set α} [Fintype s] :
                                @[simp]
                                theorem Set.toFinset_eq_univ {α : Type u_1} {s : Set α} [Fintype α] [Fintype s] :
                                Set.toFinset s = Finset.univ s = Set.univ
                                @[simp]
                                theorem Set.toFinset_setOf {α : Type u_1} [Fintype α] (p : αProp) [DecidablePred p] [Fintype {x | p x}] :
                                Set.toFinset {x | p x} = Finset.filter p Finset.univ
                                theorem Set.toFinset_ssubset_univ {α : Type u_1} [Fintype α] {s : Set α} [Fintype s] :
                                Set.toFinset s Finset.univ s Set.univ
                                @[simp]
                                theorem Set.toFinset_image {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : αβ) (s : Set α) [Fintype s] [Fintype ↑(f '' s)] :
                                @[simp]
                                theorem Set.toFinset_range {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype β] (f : βα) [Fintype ↑(Set.range f)] :
                                @[simp]
                                theorem Set.toFinset_singleton {α : Type u_1} (a : α) [Fintype {a}] :
                                Set.toFinset {a} = {a}
                                @[simp]
                                theorem Set.toFinset_insert {α : Type u_1} [DecidableEq α] {a : α} {s : Set α} [Fintype ↑(insert a s)] [Fintype s] :
                                theorem Set.filter_mem_univ_eq_toFinset {α : Type u_1} [Fintype α] (s : Set α) [Fintype s] [DecidablePred fun x => x s] :
                                Finset.filter (fun x => x s) Finset.univ = Set.toFinset s
                                @[simp]
                                theorem Finset.toFinset_coe {α : Type u_1} (s : Finset α) [Fintype s] :
                                instance Fin.fintype (n : ) :
                                Equations
                                theorem Fin.univ_def (n : ) :
                                Finset.univ = { val := ↑(List.finRange n), nodup := (_ : List.Nodup (List.finRange n)) }
                                @[simp]
                                theorem List.toFinset_finRange (n : ) :
                                List.toFinset (List.finRange n) = Finset.univ
                                @[simp]
                                theorem Fin.image_succAbove_univ {n : } (i : Fin (n + 1)) :
                                Finset.image (Fin.succAbove i) Finset.univ = {i}
                                @[simp]
                                theorem Fin.image_succ_univ (n : ) :
                                Finset.image Fin.succ Finset.univ = {0}
                                @[simp]
                                theorem Fin.image_castSucc (n : ) :
                                Finset.image Fin.castSucc Finset.univ = {Fin.last n}
                                theorem Fin.univ_succ (n : ) :
                                Finset.univ = Finset.cons 0 (Finset.map { toFun := Fin.succ, inj' := (_ : Function.Injective Fin.succ) } Finset.univ) (_ : ¬0 Finset.map { toFun := Fin.succ, inj' := (_ : Function.Injective Fin.succ) } Finset.univ)

                                Embed Fin n into Fin (n + 1) by prepending zero to the univ

                                theorem Fin.univ_castSuccEmb (n : ) :
                                Finset.univ = Finset.cons (Fin.last n) (Finset.map Fin.castSuccEmb.toEmbedding Finset.univ) (_ : ¬Fin.last n Finset.map { toFun := Fin.castSucc, inj' := (_ : ∀ (x x_1 : Fin n), Fin.castSucc x = Fin.castSucc x_1x = x_1) } Finset.univ)

                                Embed Fin n into Fin (n + 1) by appending a new Fin.last n to the univ

                                theorem Fin.univ_succAbove (n : ) (p : Fin (n + 1)) :
                                Finset.univ = Finset.cons p (Finset.map (Fin.succAboveEmb p).toEmbedding Finset.univ) (_ : ¬p Finset.map { toFun := Fin.succAbove p, inj' := (_ : ∀ (x x_1 : Fin n), Fin.succAbove p x = Fin.succAbove p x_1x = x_1) } Finset.univ)

                                Embed Fin n into Fin (n + 1) by inserting around a specified pivot p : Fin (n + 1) into the univ

                                instance Unique.fintype {α : Type u_4} [Unique α] :
                                Equations
                                instance Fintype.subtypeEq {α : Type u_1} (y : α) :
                                Fintype { x // x = y }

                                Short-circuit instance to decrease search for Unique.fintype, since that relies on a subsingleton elimination for Unique.

                                Equations
                                instance Fintype.subtypeEq' {α : Type u_1} (y : α) :
                                Fintype { x // y = x }

                                Short-circuit instance to decrease search for Unique.fintype, since that relies on a subsingleton elimination for Unique.

                                Equations
                                theorem Fintype.univ_empty :
                                Finset.univ =
                                theorem Fintype.univ_pempty :
                                Finset.univ =
                                theorem Fintype.univ_unit :
                                Finset.univ = {()}
                                theorem Fintype.univ_punit :
                                Finset.univ = {PUnit.unit}
                                Equations
                                @[simp]
                                theorem Fintype.univ_bool :
                                Finset.univ = {true, false}
                                instance Additive.fintype {α : Type u_1} [Fintype α] :
                                Equations
                                Equations
                                def Fintype.prodLeft {α : Type u_4} {β : Type u_5} [DecidableEq α] [Fintype (α × β)] [Nonempty β] :

                                Given that α × β is a fintype, α is also a fintype.

                                Equations
                                Instances For
                                  def Fintype.prodRight {α : Type u_4} {β : Type u_5} [DecidableEq β] [Fintype (α × β)] [Nonempty α] :

                                  Given that α × β is a fintype, β is also a fintype.

                                  Equations
                                  Instances For
                                    instance ULift.fintype (α : Type u_4) [Fintype α] :
                                    Equations
                                    instance PLift.fintype (α : Type u_4) [Fintype α] :
                                    Equations
                                    instance OrderDual.fintype (α : Type u_4) [Fintype α] :
                                    Equations
                                    instance OrderDual.finite (α : Type u_4) [Finite α] :
                                    Equations
                                    instance Lex.fintype (α : Type u_4) [Fintype α] :
                                    Equations

                                    Fintype (s : Finset α) #

                                    instance Finset.fintypeCoeSort {α : Type u} (s : Finset α) :
                                    Fintype { x // x s }
                                    Equations
                                    @[simp]
                                    theorem Finset.univ_eq_attach {α : Type u} (s : Finset α) :
                                    Finset.univ = Finset.attach s
                                    theorem Fintype.coe_image_univ {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : αβ} :
                                    ↑(Finset.image f Finset.univ) = Set.range f
                                    instance List.Subtype.fintype {α : Type u_1} [DecidableEq α] (l : List α) :
                                    Fintype { x // x l }
                                    Equations
                                    instance Multiset.Subtype.fintype {α : Type u_1} [DecidableEq α] (s : Multiset α) :
                                    Fintype { x // x s }
                                    Equations
                                    instance Finset.Subtype.fintype {α : Type u_1} (s : Finset α) :
                                    Fintype { x // x s }
                                    Equations
                                    instance FinsetCoe.fintype {α : Type u_1} (s : Finset α) :
                                    Fintype s
                                    Equations
                                    theorem Finset.attach_eq_univ {α : Type u_1} {s : Finset α} :
                                    Finset.attach s = Finset.univ
                                    instance PLift.fintypeProp (p : Prop) [Decidable p] :
                                    Equations
                                    Equations
                                    @[simp]
                                    theorem Fintype.univ_Prop :
                                    Finset.univ = {True, False}
                                    instance Subtype.fintype {α : Type u_1} (p : αProp) [DecidablePred p] [Fintype α] :
                                    Fintype { x // p x }
                                    Equations
                                    def setFintype {α : Type u_1} [Fintype α] (s : Set α) [DecidablePred fun x => x s] :
                                    Fintype s

                                    A set on a fintype, when coerced to a type, is a fintype.

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem val_inv_unitsEquivProdSubtype_symm_apply (α : Type u_1) [Monoid α] (p : { p // p.fst * p.snd = 1 p.snd * p.fst = 1 }) :
                                      ((unitsEquivProdSubtype α).symm p)⁻¹ = (p).snd
                                      @[simp]
                                      theorem val_unitsEquivProdSubtype_symm_apply (α : Type u_1) [Monoid α] (p : { p // p.fst * p.snd = 1 p.snd * p.fst = 1 }) :
                                      ↑((unitsEquivProdSubtype α).symm p) = (p).fst
                                      @[simp]
                                      theorem unitsEquivProdSubtype_apply_coe (α : Type u_1) [Monoid α] (u : αˣ) :
                                      ↑(↑(unitsEquivProdSubtype α) u) = (u, u⁻¹)
                                      def unitsEquivProdSubtype (α : Type u_1) [Monoid α] :
                                      αˣ { p // p.fst * p.snd = 1 p.snd * p.fst = 1 }

                                      The αˣ type is equivalent to a subtype of α × α.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        @[simp]
                                        theorem unitsEquivNeZero_apply_coe (α : Type u_1) [GroupWithZero α] (a : αˣ) :
                                        ↑(↑(unitsEquivNeZero α) a) = a
                                        @[simp]
                                        theorem unitsEquivNeZero_symm_apply (α : Type u_1) [GroupWithZero α] (a : { a // a 0 }) :
                                        (unitsEquivNeZero α).symm a = Units.mk0 a (_ : a 0)
                                        def unitsEquivNeZero (α : Type u_1) [GroupWithZero α] :
                                        αˣ { a // a 0 }

                                        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.
                                        Instances For
                                          noncomputable def Fintype.finsetEquivSet {α : Type u_1} [Fintype α] :
                                          Finset α Set α

                                          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.
                                          Instances For
                                            @[simp]
                                            theorem Fintype.coe_finsetEquivSet {α : Type u_1} [Fintype α] :
                                            Fintype.finsetEquivSet = Finset.toSet
                                            @[simp]
                                            theorem Fintype.finsetEquivSet_apply {α : Type u_1} [Fintype α] (s : Finset α) :
                                            Fintype.finsetEquivSet s = s
                                            @[simp]
                                            theorem Fintype.finsetEquivSet_symm_apply {α : Type u_1} [Fintype α] (s : Set α) [Fintype s] :
                                            Fintype.finsetEquivSet.symm s = Set.toFinset s
                                            @[simp]
                                            theorem Fintype.finsetOrderIsoSet_toEquiv {α : Type u_1} [Fintype α] :
                                            Fintype.finsetOrderIsoSet.toEquiv = Fintype.finsetEquivSet
                                            noncomputable def Fintype.finsetOrderIsoSet {α : Type u_1} [Fintype α] :

                                            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' := (_ : ∀ {a b : Finset α}, a b a b) }
                                            Instances For
                                              @[simp]
                                              theorem Fintype.coe_finsetOrderIsoSet {α : Type u_1} [Fintype α] :
                                              Fintype.finsetOrderIsoSet = Finset.toSet
                                              @[simp]
                                              theorem Fintype.coe_finsetOrderIsoSet_symm {α : Type u_1} [Fintype α] :
                                              ↑(OrderIso.symm Fintype.finsetOrderIsoSet) = Fintype.finsetEquivSet.symm
                                              instance Quotient.fintype {α : Type u_1} [Fintype α] (s : Setoid α) [DecidableRel fun x x_1 => x x_1] :
                                              Equations
                                              instance PSigma.fintypePropLeft {α : Prop} {β : αType u_4} [Decidable α] [(a : α) → Fintype (β a)] :
                                              Fintype ((a : α) ×' β a)
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              instance PSigma.fintypePropRight {α : Type u_4} {β : αProp} [(a : α) → Decidable (β a)] [Fintype α] :
                                              Fintype ((a : α) ×' β a)
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              instance PSigma.fintypePropProp {α : Prop} {β : αProp} [Decidable α] [(a : α) → Decidable (β a)] :
                                              Fintype ((a : α) ×' β a)
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              instance pfunFintype (p : Prop) [Decidable p] (α : pType u_4) [(hp : p) → Fintype (α hp)] :
                                              Fintype ((hp : p) → α hp)
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              theorem mem_image_univ_iff_mem_range {α : Type u_4} {β : Type u_5} [Fintype α] [DecidableEq β] {f : αβ} {b : β} :
                                              b Finset.image f Finset.univ b Set.range f
                                              def Fintype.chooseX {α : Type u_1} [Fintype α] (p : αProp) [DecidablePred p] (hp : ∃! a, p a) :
                                              { a // p a }

                                              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
                                              Instances For
                                                def Fintype.choose {α : Type u_1} [Fintype α] (p : αProp) [DecidablePred p] (hp : ∃! a, p a) :
                                                α

                                                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
                                                Instances For
                                                  theorem Fintype.choose_spec {α : Type u_1} [Fintype α] (p : αProp) [DecidablePred p] (hp : ∃! a, p a) :
                                                  theorem Fintype.choose_subtype_eq {α : Type u_4} (p : αProp) [Fintype { a // p a }] [DecidableEq α] (x : { a // p a }) (h : optParam (∃! a, a = x) (_ : x, (fun a => a = x) x ∀ (y : { a // p a }), (fun a => a = x) yy = x)) :
                                                  Fintype.choose (fun y => y = x) h = x
                                                  def Fintype.bijInv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : αβ} (f_bij : Function.Bijective f) (b : β) :
                                                  α

                                                  bijInv f is the unique inverse to a bijection f. This acts as a computable alternative to Function.invFun.

                                                  Equations
                                                  Instances For
                                                    theorem Fintype.leftInverse_bijInv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : αβ} (f_bij : Function.Bijective f) :
                                                    theorem Fintype.rightInverse_bijInv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : αβ} (f_bij : Function.Bijective f) :
                                                    theorem Fintype.bijective_bijInv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : αβ} (f_bij : Function.Bijective f) :
                                                    def truncOfMultisetExistsMem {α : Type u_4} (s : Multiset α) :
                                                    (x, x s) → Trunc α

                                                    For s : Multiset α, we can lift the existential statement that ∃ x, x ∈ s to a Trunc α.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      def truncOfNonemptyFintype (α : Type u_4) [Nonempty α] [Fintype α] :

                                                      A Nonempty Fintype constructively contains an element.

                                                      Equations
                                                      Instances For
                                                        def truncSigmaOfExists {α : Type u_4} [Fintype α] {P : αProp} [DecidablePred P] (h : a, P a) :
                                                        Trunc ((a : α) ×' P a)

                                                        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
                                                        Instances For
                                                          @[simp]
                                                          theorem Multiset.count_univ {α : Type u_1} [Fintype α] [DecidableEq α] (a : α) :
                                                          Multiset.count a Finset.univ.val = 1
                                                          @[simp]
                                                          theorem Multiset.map_univ_val_equiv {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (e : α β) :
                                                          Multiset.map (e) Finset.univ.val = Finset.univ.val
                                                          noncomputable def seqOfForallFinsetExistsAux {α : Type u_4} [DecidableEq α] (P : αProp) (r : ααProp) (h : ∀ (s : Finset α), y, ((x : α) → x sP x) → P y ((x : α) → x sr x y)) :
                                                          α

                                                          Auxiliary definition to show exists_seq_of_forall_finset_exists.

                                                          Equations
                                                          Instances For
                                                            theorem exists_seq_of_forall_finset_exists {α : Type u_4} (P : αProp) (r : ααProp) (h : ∀ (s : Finset α), ((x : α) → x sP x) → y, P y ((x : α) → x sr x y)) :
                                                            f, ((n : ) → P (f n)) ((m n : ) → m < nr (f m) (f n))

                                                            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.

                                                            theorem exists_seq_of_forall_finset_exists' {α : Type u_4} (P : αProp) (r : ααProp) [IsSymm α r] (h : ∀ (s : Finset α), ((x : α) → x sP x) → y, P y ((x : α) → x sr x y)) :
                                                            f, ((n : ) → P (f n)) ((m n : ) → m nr (f m) (f n))

                                                            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.