Documentation

Mathlib.Data.Fintype.Card

Cardinalities of finite types #

Main declarations #

We also provide the following versions of the pigeonholes principle.

Some more pigeonhole-like statements can be found in Data.Fintype.CardEmbedding.

Types which have an injection from/a surjection to an Infinite type are themselves Infinite. See Infinite.of_injective and Infinite.of_surjective.

Instances #

We provide Infinite instances for

def Fintype.card (α : Type u_4) [Fintype α] :

card α is the number of elements in α, defined when α is a fintype.

Equations
Instances For

    There is (computably) an equivalence between α and Fin (card α).

    Since it is not unique and depends on which permutation of the universe list is used, the equivalence is wrapped in Trunc to preserve computability.

    See Fintype.equivFin for the noncomputable version, and Fintype.truncEquivFinOfCardEq and Fintype.equivFinOfCardEq for an equiv α ≃ Fin n given Fintype.card α = n.

    See Fintype.truncFinBijection for a version without [DecidableEq α].

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

      There is (noncomputably) an equivalence between α and Fin (card α).

      See Fintype.truncEquivFin for the computable version, and Fintype.truncEquivFinOfCardEq and Fintype.equivFinOfCardEq for an equiv α ≃ Fin n given Fintype.card α = n.

      Equations
      Instances For
        def Fintype.truncFinBijection (α : Type u_4) [Fintype α] :
        Trunc { f : Fin (Fintype.card α)α // Function.Bijective f }

        There is (computably) a bijection between Fin (card α) and α.

        Since it is not unique and depends on which permutation of the universe list is used, the bijection is wrapped in Trunc to preserve computability.

        See Fintype.truncEquivFin for a version that gives an equivalence given [DecidableEq α].

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem Fintype.subtype_card {α : Type u_1} {p : αProp} (s : Finset α) (H : ∀ (x : α), x s p x) :
          Fintype.card { x : α // p x } = s.card
          theorem Fintype.card_of_subtype {α : Type u_1} {p : αProp} (s : Finset α) (H : ∀ (x : α), x s p x) [Fintype { x : α // p x }] :
          Fintype.card { x : α // p x } = s.card
          @[simp]
          theorem Fintype.card_ofFinset {α : Type u_1} {p : Set α} (s : Finset α) (H : ∀ (x : α), x s x p) :
          Fintype.card p = s.card
          theorem Fintype.card_of_finset' {α : Type u_1} {p : Set α} (s : Finset α) (H : ∀ (x : α), x s x p) [Fintype p] :
          Fintype.card p = s.card
          theorem Fintype.ofEquiv_card {α : Type u_1} {β : Type u_2} [Fintype α] (f : α β) :
          theorem Fintype.card_congr {α : Type u_4} {β : Type u_5} [Fintype α] [Fintype β] (f : α β) :
          theorem Fintype.card_congr' {α : Type u_4} {β : Type u_4} [Fintype α] [Fintype β] (h : α = β) :
          def Fintype.truncEquivFinOfCardEq {α : Type u_1} [Fintype α] [DecidableEq α] {n : } (h : Fintype.card α = n) :
          Trunc (α Fin n)

          If the cardinality of α is n, there is computably a bijection between α and Fin n.

          See Fintype.equivFinOfCardEq for the noncomputable definition, and Fintype.truncEquivFin and Fintype.equivFin for the bijection α ≃ Fin (card α).

          Equations
          Instances For
            noncomputable def Fintype.equivFinOfCardEq {α : Type u_1} [Fintype α] {n : } (h : Fintype.card α = n) :
            α Fin n

            If the cardinality of α is n, there is noncomputably a bijection between α and Fin n.

            See Fintype.truncEquivFinOfCardEq for the computable definition, and Fintype.truncEquivFin and Fintype.equivFin for the bijection α ≃ Fin (card α).

            Equations
            Instances For
              def Fintype.truncEquivOfCardEq {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (h : Fintype.card α = Fintype.card β) :
              Trunc (α β)

              Two Fintypes with the same cardinality are (computably) in bijection.

              See Fintype.equivOfCardEq for the noncomputable version, and Fintype.truncEquivFinOfCardEq and Fintype.equivFinOfCardEq for the specialization to Fin.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                noncomputable def Fintype.equivOfCardEq {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (h : Fintype.card α = Fintype.card β) :
                α β

                Two Fintypes with the same cardinality are (noncomputably) in bijection.

                See Fintype.truncEquivOfCardEq for the computable version, and Fintype.truncEquivFinOfCardEq and Fintype.equivFinOfCardEq for the specialization to Fin.

                Equations
                Instances For
                  theorem Fintype.card_eq {α : Type u_4} {β : Type u_5} [_F : Fintype α] [_G : Fintype β] :
                  @[simp]
                  theorem Fintype.card_ofSubsingleton {α : Type u_1} (a : α) [Subsingleton α] :

                  Note: this lemma is specifically about Fintype.ofSubsingleton. For a statement about arbitrary Fintype instances, use either Fintype.card_le_one_iff_subsingleton or Fintype.card_unique.

                  @[simp]
                  theorem Fintype.card_unique {α : Type u_1} [Unique α] [h : Fintype α] :
                  @[simp]
                  theorem Fintype.card_ofIsEmpty {α : Type u_1} [IsEmpty α] :

                  Note: this lemma is specifically about Fintype.ofIsEmpty. For a statement about arbitrary Fintype instances, use Fintype.card_eq_zero.

                  @[simp]
                  theorem Set.toFinset_card {α : Type u_4} (s : Set α) [Fintype s] :
                  s.toFinset.card = Fintype.card s
                  @[simp]
                  theorem Finset.card_univ {α : Type u_1} [Fintype α] :
                  Finset.univ.card = Fintype.card α
                  theorem Finset.eq_univ_of_card {α : Type u_1} [Fintype α] (s : Finset α) (hs : s.card = Fintype.card α) :
                  s = Finset.univ
                  theorem Finset.card_eq_iff_eq_univ {α : Type u_1} [Fintype α] (s : Finset α) :
                  s.card = Fintype.card α s = Finset.univ
                  theorem Finset.card_le_univ {α : Type u_1} [Fintype α] (s : Finset α) :
                  s.card Fintype.card α
                  theorem Finset.card_lt_univ_of_not_mem {α : Type u_1} [Fintype α] {s : Finset α} {x : α} (hx : xs) :
                  s.card < Fintype.card α
                  theorem Finset.card_lt_iff_ne_univ {α : Type u_1} [Fintype α] (s : Finset α) :
                  s.card < Fintype.card α s Finset.univ
                  theorem Finset.card_compl_lt_iff_nonempty {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
                  s.card < Fintype.card α s.Nonempty
                  theorem Finset.card_univ_diff {α : Type u_1} [DecidableEq α] [Fintype α] (s : Finset α) :
                  (Finset.univ \ s).card = Fintype.card α - s.card
                  theorem Finset.card_compl {α : Type u_1} [DecidableEq α] [Fintype α] (s : Finset α) :
                  s.card = Fintype.card α - s.card
                  @[simp]
                  theorem Finset.card_add_card_compl {α : Type u_1} [DecidableEq α] [Fintype α] (s : Finset α) :
                  s.card + s.card = Fintype.card α
                  @[simp]
                  theorem Finset.card_compl_add_card {α : Type u_1} [DecidableEq α] [Fintype α] (s : Finset α) :
                  s.card + s.card = Fintype.card α
                  theorem Fintype.card_compl_set {α : Type u_1} [Fintype α] (s : Set α) [Fintype s] [Fintype s] :
                  @[simp]
                  theorem Fintype.card_fin (n : ) :
                  theorem Fintype.card_fin_lt_of_le {m : } {n : } (h : m n) :
                  Fintype.card { i : Fin n // i < m } = m
                  theorem Finset.card_fin (n : ) :
                  Finset.univ.card = n

                  Fin as a map from to Type is injective. Note that since this is a statement about equality of types, using it should be avoided if possible.

                  theorem Fin.val_eq_val_of_heq {k : } {l : } {i : Fin k} {j : Fin l} (h : HEq i j) :
                  i = j
                  theorem Fin.cast_eq_cast' {n : } {m : } (h : Fin n = Fin m) :

                  A reversed version of Fin.cast_eq_cast that is easier to rewrite with.

                  theorem card_finset_fin_le {n : } (s : Finset (Fin n)) :
                  s.card n
                  theorem Fintype.card_subtype_eq {α : Type u_1} (y : α) [Fintype { x : α // x = y }] :
                  Fintype.card { x : α // x = y } = 1
                  theorem Fintype.card_subtype_eq' {α : Type u_1} (y : α) [Fintype { x : α // y = x }] :
                  Fintype.card { x : α // y = x } = 1
                  @[simp]
                  @[simp]
                  theorem Fintype.card_lex (α : Type u_4) [Fintype α] :
                  noncomputable def Fintype.sumLeft {α : Type u_4} {β : Type u_5} [Fintype (α β)] :

                  Given that α ⊕ β is a fintype, α is also a fintype. This is non-computable as it uses that Sum.inl is an injection, but there's no clear inverse if α is empty.

                  Equations
                  Instances For
                    noncomputable def Fintype.sumRight {α : Type u_4} {β : Type u_5} [Fintype (α β)] :

                    Given that α ⊕ β is a fintype, β is also a fintype. This is non-computable as it uses that Sum.inr is an injection, but there's no clear inverse if β is empty.

                    Equations
                    Instances For

                      Relation to Finite #

                      In this section we prove that α : Type* is Finite if and only if Fintype α is nonempty.

                      theorem Fintype.finite {α : Type u_4} (_inst : Fintype α) :
                      @[instance 900]
                      instance Finite.of_fintype (α : Type u_4) [Fintype α] :

                      For efficiency reasons, we want Finite instances to have higher priority than ones coming from Fintype instances.

                      Equations
                      • =
                      theorem nonempty_fintype (α : Type u_4) [Finite α] :

                      See also nonempty_encodable, nonempty_denumerable.

                      noncomputable def Fintype.ofFinite (α : Type u_4) [Finite α] :

                      Noncomputably get a Fintype instance from a Finite instance. This is not an instance because we want Fintype instances to be useful for computations.

                      Equations
                      Instances For
                        theorem Finite.of_injective {α : Sort u_4} {β : Sort u_5} [Finite β] (f : αβ) (H : Function.Injective f) :
                        instance Subtype.finite {α : Sort u_4} [Finite α] {p : αProp} :
                        Finite { x : α // p x }

                        This instance also provides [Finite s] for s : Set α.

                        Equations
                        • =
                        theorem Finite.of_surjective {α : Sort u_4} {β : Sort u_5} [Finite α] (f : αβ) (H : Function.Surjective f) :
                        theorem Finite.exists_univ_list (α : Type u_4) [Finite α] :
                        ∃ (l : List α), l.Nodup ∀ (x : α), x l
                        theorem List.Nodup.length_le_card {α : Type u_4} [Fintype α] {l : List α} (h : l.Nodup) :
                        l.length Fintype.card α
                        theorem Fintype.card_le_of_injective {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : αβ) (hf : Function.Injective f) :
                        theorem Fintype.card_le_of_embedding {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : α β) :
                        theorem Fintype.card_lt_of_injective_of_not_mem {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : αβ) (h : Function.Injective f) {b : β} (w : bSet.range f) :
                        theorem Fintype.card_le_of_surjective {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : αβ) (h : Function.Surjective f) :
                        theorem Fintype.card_range_le {α : Type u_4} {β : Type u_5} (f : αβ) [Fintype α] [Fintype (Set.range f)] :
                        theorem Fintype.card_range {α : Type u_4} {β : Type u_5} {F : Type u_6} [FunLike F α β] [EmbeddingLike F α β] (f : F) [Fintype α] [Fintype (Set.range f)] :
                        theorem Fintype.exists_ne_map_eq_of_card_lt {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : αβ) (h : Fintype.card β < Fintype.card α) :
                        ∃ (x : α) (y : α), x y f x = f y

                        The pigeonhole principle for finitely many pigeons and pigeonholes. This is the Fintype version of Finset.exists_ne_map_eq_of_card_lt_of_maps_to.

                        theorem Fintype.card_eq_one_iff {α : Type u_1} [Fintype α] :
                        Fintype.card α = 1 ∃ (x : α), ∀ (y : α), y = x
                        @[simp]
                        theorem Fintype.card_eq_zero {α : Type u_1} [Fintype α] [IsEmpty α] :

                        A Fintype with cardinality zero is equivalent to Empty.

                        Equations
                        Instances For
                          theorem Fintype.card_pos {α : Type u_1} [Fintype α] [h : Nonempty α] :
                          @[simp]
                          theorem Fintype.card_ne_zero {α : Type u_1} [Fintype α] [Nonempty α] :
                          Equations
                          • =
                          theorem Fintype.card_le_one_iff {α : Type u_1} [Fintype α] :
                          Fintype.card α 1 ∀ (a b : α), a = b
                          theorem Fintype.exists_ne_of_one_lt_card {α : Type u_1} [Fintype α] (h : 1 < Fintype.card α) (a : α) :
                          ∃ (b : α), b a
                          theorem Fintype.exists_pair_of_one_lt_card {α : Type u_1} [Fintype α] (h : 1 < Fintype.card α) :
                          ∃ (a : α) (b : α), a b
                          theorem Fintype.card_eq_one_of_forall_eq {α : Type u_1} [Fintype α] {i : α} (h : ∀ (j : α), j = i) :
                          theorem Fintype.exists_unique_iff_card_one {α : Type u_4} [Fintype α] (p : αProp) [DecidablePred p] :
                          (∃! a : α, p a) (Finset.filter p Finset.univ).card = 1
                          theorem Fintype.one_lt_card {α : Type u_1} [Fintype α] [h : Nontrivial α] :
                          theorem Fintype.one_lt_card_iff {α : Type u_1} [Fintype α] :
                          1 < Fintype.card α ∃ (a : α) (b : α), a b
                          theorem Fintype.two_lt_card_iff {α : Type u_1} [Fintype α] :
                          2 < Fintype.card α ∃ (a : α) (b : α) (c : α), a b a c b c
                          theorem Fintype.card_of_bijective {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {f : αβ} (hf : Function.Bijective f) :
                          theorem Finite.surjective_of_injective {α : Type u_1} [Finite α] {f : αα} (hinj : Function.Injective f) :
                          theorem Finite.injective_iff_surjective_of_equiv {α : Type u_1} {β : Type u_2} [Finite α] {f : αβ} (e : α β) :

                          Alias of the forward direction of Finite.injective_iff_bijective.

                          Alias of the forward direction of Finite.surjective_iff_bijective.

                          theorem Function.Injective.surjective_of_fintype {α : Type u_1} {β : Type u_2} [Finite α] {f : αβ} (e : α β) :

                          Alias of the forward direction of Finite.injective_iff_surjective_of_equiv.

                          theorem Function.Surjective.injective_of_fintype {α : Type u_1} {β : Type u_2} [Finite α] {f : αβ} (e : α β) :

                          Alias of the reverse direction of Finite.injective_iff_surjective_of_equiv.

                          theorem Function.LeftInverse.rightInverse_of_card_le {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {f : αβ} {g : βα} (hfg : Function.LeftInverse f g) (hcard : Fintype.card α Fintype.card β) :
                          theorem Function.RightInverse.leftInverse_of_card_le {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {f : αβ} {g : βα} (hfg : Function.RightInverse f g) (hcard : Fintype.card β Fintype.card α) :
                          @[simp]
                          theorem Equiv.ofLeftInverseOfCardLE_symm_apply {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (hβα : Fintype.card β Fintype.card α) (f : αβ) (g : βα) (h : Function.LeftInverse g f) :
                          ∀ (a : β), (Equiv.ofLeftInverseOfCardLE hβα f g h).symm a = g a
                          @[simp]
                          theorem Equiv.ofLeftInverseOfCardLE_apply {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (hβα : Fintype.card β Fintype.card α) (f : αβ) (g : βα) (h : Function.LeftInverse g f) :
                          ∀ (a : α), (Equiv.ofLeftInverseOfCardLE hβα f g h) a = f a
                          def Equiv.ofLeftInverseOfCardLE {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (hβα : Fintype.card β Fintype.card α) (f : αβ) (g : βα) (h : Function.LeftInverse g f) :
                          α β

                          Construct an equivalence from functions that are inverse to each other.

                          Equations
                          Instances For
                            @[simp]
                            theorem Equiv.ofRightInverseOfCardLE_symm_apply {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (hαβ : Fintype.card α Fintype.card β) (f : αβ) (g : βα) (h : Function.RightInverse g f) :
                            ∀ (a : β), (Equiv.ofRightInverseOfCardLE hαβ f g h).symm a = g a
                            @[simp]
                            theorem Equiv.ofRightInverseOfCardLE_apply {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (hαβ : Fintype.card α Fintype.card β) (f : αβ) (g : βα) (h : Function.RightInverse g f) :
                            ∀ (a : α), (Equiv.ofRightInverseOfCardLE hαβ f g h) a = f a
                            def Equiv.ofRightInverseOfCardLE {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (hαβ : Fintype.card α Fintype.card β) (f : αβ) (g : βα) (h : Function.RightInverse g f) :
                            α β

                            Construct an equivalence from functions that are inverse to each other.

                            Equations
                            Instances For
                              @[simp]
                              theorem Fintype.card_coe {α : Type u_1} (s : Finset α) [Fintype { x : α // x s }] :
                              Fintype.card { x : α // x s } = s.card
                              noncomputable def Finset.equivFin {α : Type u_1} (s : Finset α) :
                              { x : α // x s } Fin s.card

                              Noncomputable equivalence between a finset s coerced to a type and Fin s.card.

                              Equations
                              Instances For
                                noncomputable def Finset.equivFinOfCardEq {α : Type u_1} {s : Finset α} {n : } (h : s.card = n) :
                                { x : α // x s } Fin n

                                Noncomputable equivalence between a finset s as a fintype and Fin n, when there is a proof that s.card = n.

                                Equations
                                Instances For
                                  theorem Finset.card_eq_of_equiv_fin {α : Type u_1} {s : Finset α} {n : } (i : { x : α // x s } Fin n) :
                                  s.card = n
                                  theorem Finset.card_eq_of_equiv_fintype {α : Type u_1} {β : Type u_2} {s : Finset α} [Fintype β] (i : { x : α // x s } β) :
                                  s.card = Fintype.card β
                                  noncomputable def Finset.equivOfCardEq {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (h : s.card = t.card) :
                                  { x : α // x s } { x : β // x t }

                                  Noncomputable equivalence between two finsets s and t as fintypes when there is a proof that s.card = t.card.

                                  Equations
                                  Instances For
                                    theorem Finset.card_eq_of_equiv {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (i : { x : α // x s } { x : β // x t }) :
                                    s.card = t.card
                                    theorem Finset.exists_superset_card_eq {α : Type u_1} [Fintype α] {n : } {s : Finset α} (hsn : s.card n) (hnα : n Fintype.card α) :
                                    ∃ (t : Finset α), s t t.card = n

                                    We can inflate a set s to any bigger size.

                                    theorem set_fintype_card_le_univ {α : Type u_1} [Fintype α] (s : Set α) [Fintype s] :
                                    theorem set_fintype_card_eq_univ_iff {α : Type u_1} [Fintype α] (s : Set α) [Fintype s] :
                                    Fintype.card s = Fintype.card α s = Set.univ
                                    noncomputable def Function.Embedding.equivOfFintypeSelfEmbedding {α : Type u_1} [Finite α] (e : α α) :
                                    α α

                                    An embedding from a Fintype to itself can be promoted to an equivalence.

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem Function.Embedding.equiv_of_fintype_self_embedding_to_embedding {α : Type u_1} [Finite α] (e : α α) :
                                      e.equivOfFintypeSelfEmbedding.toEmbedding = e
                                      @[simp]
                                      theorem Function.Embedding.isEmpty_of_card_lt {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (h : Fintype.card β < Fintype.card α) :
                                      IsEmpty (α β)

                                      If ‖β‖ < ‖α‖ there are no embeddings α ↪ β. This is a formulation of the pigeonhole principle.

                                      Note this cannot be an instance as it needs h.

                                      def Function.Embedding.truncOfCardLE {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (h : Fintype.card α Fintype.card β) :
                                      Trunc (α β)

                                      A constructive embedding of a fintype α in another fintype β when card α ≤ card β.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        theorem Function.Embedding.nonempty_of_card_le {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (h : Fintype.card α Fintype.card β) :
                                        Nonempty (α β)
                                        theorem Function.Embedding.exists_of_card_le_finset {α : Type u_1} {β : Type u_2} [Fintype α] {s : Finset β} (h : Fintype.card α s.card) :
                                        ∃ (f : α β), Set.range f s
                                        @[simp]
                                        theorem Finset.univ_map_embedding {α : Type u_4} [Fintype α] (e : α α) :
                                        Finset.map e Finset.univ = Finset.univ
                                        theorem Fintype.card_subtype_le {α : Type u_1} [Fintype α] (p : αProp) [DecidablePred p] :
                                        Fintype.card { x : α // p x } Fintype.card α
                                        theorem Fintype.card_subtype_lt {α : Type u_1} [Fintype α] {p : αProp} [DecidablePred p] {x : α} (hx : ¬p x) :
                                        Fintype.card { x : α // p x } < Fintype.card α
                                        theorem Fintype.card_subtype {α : Type u_1} [Fintype α] (p : αProp) [DecidablePred p] :
                                        Fintype.card { x : α // p x } = (Finset.filter p Finset.univ).card
                                        @[simp]
                                        theorem Fintype.card_subtype_compl {α : Type u_1} [Fintype α] (p : αProp) [Fintype { x : α // p x }] [Fintype { x : α // ¬p x }] :
                                        Fintype.card { x : α // ¬p x } = Fintype.card α - Fintype.card { x : α // p x }
                                        theorem Fintype.card_subtype_mono {α : Type u_1} (p : αProp) (q : αProp) (h : p q) [Fintype { x : α // p x }] [Fintype { x : α // q x }] :
                                        Fintype.card { x : α // p x } Fintype.card { x : α // q x }
                                        theorem Fintype.card_compl_eq_card_compl {α : Type u_1} [Finite α] (p : αProp) (q : αProp) [Fintype { x : α // p x }] [Fintype { x : α // ¬p x }] [Fintype { x : α // q x }] [Fintype { x : α // ¬q x }] (h : Fintype.card { x : α // p x } = Fintype.card { x : α // q x }) :
                                        Fintype.card { x : α // ¬p x } = Fintype.card { x : α // ¬q x }

                                        If two subtypes of a fintype have equal cardinality, so do their complements.

                                        theorem Fintype.card_quotient_le {α : Type u_1} [Fintype α] (s : Setoid α) [DecidableRel fun (x1 x2 : α) => x1 x2] :
                                        theorem Fintype.card_quotient_lt {α : Type u_1} [Fintype α] {s : Setoid α} [DecidableRel fun (x1 x2 : α) => x1 x2] {x : α} {y : α} (h1 : x y) (h2 : x y) :
                                        theorem univ_eq_singleton_of_card_one {α : Type u_4} [Fintype α] (x : α) (h : Fintype.card α = 1) :
                                        Finset.univ = {x}
                                        theorem Finite.wellFounded_of_trans_of_irrefl {α : Type u_1} [Finite α] (r : ααProp) [IsTrans α r] [IsIrrefl α r] :
                                        @[instance 100]
                                        instance Finite.to_wellFoundedLT {α : Type u_1} [Finite α] [Preorder α] :
                                        Equations
                                        • =
                                        @[instance 100]
                                        instance Finite.to_wellFoundedGT {α : Type u_1} [Finite α] [Preorder α] :
                                        Equations
                                        • =
                                        @[instance 10]
                                        instance Finite.LinearOrder.isWellOrder_lt {α : Type u_1} [Finite α] [LinearOrder α] :
                                        IsWellOrder α fun (x1 x2 : α) => x1 < x2
                                        Equations
                                        • =
                                        @[instance 10]
                                        instance Finite.LinearOrder.isWellOrder_gt {α : Type u_1} [Finite α] [LinearOrder α] :
                                        IsWellOrder α fun (x1 x2 : α) => x1 > x2
                                        Equations
                                        • =
                                        theorem Fintype.false {α : Type u_1} [Infinite α] (_h : Fintype α) :
                                        @[simp]
                                        theorem isEmpty_fintype {α : Type u_4} :
                                        noncomputable def fintypeOfNotInfinite {α : Type u_4} (h : ¬Infinite α) :

                                        A non-infinite type is a fintype.

                                        Equations
                                        Instances For
                                          noncomputable def fintypeOrInfinite (α : Type u_4) :

                                          Any type is (classically) either a Fintype, or Infinite.

                                          One can obtain the relevant typeclasses via cases fintypeOrInfinite α.

                                          Equations
                                          Instances For
                                            theorem Finset.exists_minimal {α : Type u_4} [Preorder α] (s : Finset α) (h : s.Nonempty) :
                                            ms, xs, ¬x < m
                                            theorem Finset.exists_maximal {α : Type u_4} [Preorder α] (s : Finset α) (h : s.Nonempty) :
                                            ms, xs, ¬m < x
                                            theorem Infinite.of_not_fintype {α : Type u_1} (h : Fintype αFalse) :
                                            theorem Infinite.of_injective_to_set {α : Type u_1} {s : Set α} (hs : s Set.univ) {f : αs} (hf : Function.Injective f) :

                                            If s : Set α is a proper subset of α and f : α → s is injective, then α is infinite.

                                            theorem Infinite.of_surjective_from_set {α : Type u_1} {s : Set α} (hs : s Set.univ) {f : sα} (hf : Function.Surjective f) :

                                            If s : Set α is a proper subset of α and f : s → α is surjective, then α is infinite.

                                            theorem Infinite.exists_not_mem_finset {α : Type u_1} [Infinite α] (s : Finset α) :
                                            ∃ (x : α), xs
                                            @[instance 100]
                                            instance Infinite.instNontrivial (α : Type u_4) [H : Infinite α] :
                                            Equations
                                            • =
                                            theorem Infinite.nonempty (α : Type u_4) [Infinite α] :
                                            theorem Infinite.of_injective {α : Sort u_4} {β : Sort u_5} [Infinite β] (f : βα) (hf : Function.Injective f) :
                                            theorem Infinite.of_surjective {α : Sort u_4} {β : Sort u_5} [Infinite β] (f : αβ) (hf : Function.Surjective f) :
                                            instance Infinite.instSigmaOfNonempty {α : Type u_1} {β : αType u_4} [Infinite α] [∀ (a : α), Nonempty (β a)] :
                                            Infinite ((a : α) × β a)
                                            Equations
                                            • =
                                            theorem Infinite.sigma_of_right {α : Type u_1} {β : αType u_4} {a : α} [Infinite (β a)] :
                                            Infinite ((a : α) × β a)
                                            instance Infinite.instSigmaOfNonempty_1 {α : Type u_1} {β : αType u_4} [Nonempty α] [∀ (a : α), Infinite (β a)] :
                                            Infinite ((a : α) × β a)
                                            Equations
                                            • =
                                            Equations
                                            • =
                                            instance instInfiniteListOfNonempty {α : Type u_1} [Nonempty α] :
                                            Equations
                                            • =
                                            instance Infinite.set {α : Type u_1} [Infinite α] :
                                            Equations
                                            • =
                                            instance instInfiniteFinset {α : Type u_1} [Infinite α] :
                                            Equations
                                            • =
                                            instance instInfiniteOption {α : Type u_1} [Infinite α] :
                                            Equations
                                            • =
                                            instance Sum.infinite_of_left {α : Type u_1} {β : Type u_2} [Infinite α] :
                                            Infinite (α β)
                                            Equations
                                            • =
                                            instance Sum.infinite_of_right {α : Type u_1} {β : Type u_2} [Infinite β] :
                                            Infinite (α β)
                                            Equations
                                            • =
                                            instance Prod.infinite_of_right {α : Type u_1} {β : Type u_2} [Nonempty α] [Infinite β] :
                                            Infinite (α × β)
                                            Equations
                                            • =
                                            instance Prod.infinite_of_left {α : Type u_1} {β : Type u_2} [Infinite α] [Nonempty β] :
                                            Infinite (α × β)
                                            Equations
                                            • =
                                            instance instInfiniteProdSubtypeCommute {α : Type u_1} [Mul α] [Infinite α] :
                                            Infinite { p : α × α // Commute p.1 p.2 }
                                            Equations
                                            • =
                                            noncomputable def Infinite.natEmbedding (α : Type u_4) [Infinite α] :
                                            α

                                            Embedding of into an infinite type.

                                            Equations
                                            Instances For
                                              theorem Infinite.exists_subset_card_eq (α : Type u_4) [Infinite α] (n : ) :
                                              ∃ (s : Finset α), s.card = n

                                              See Infinite.exists_superset_card_eq for a version that, for an s : Finset α, provides a superset t : Finset α, s ⊆ t such that t.card is fixed.

                                              theorem Infinite.exists_superset_card_eq {α : Type u_1} [Infinite α] (s : Finset α) (n : ) (hn : s.card n) :
                                              ∃ (t : Finset α), s t t.card = n

                                              See Infinite.exists_subset_card_eq for a version that provides an arbitrary s : Finset α for any cardinality.

                                              noncomputable def fintypeOfFinsetCardLe {ι : Type u_4} (n : ) (w : ∀ (s : Finset ι), s.card n) :

                                              If every finset in a type has bounded cardinality, that type is finite.

                                              Equations
                                              Instances For
                                                theorem not_injective_infinite_finite {α : Sort u_4} {β : Sort u_5} [Infinite α] [Finite β] (f : αβ) :
                                                theorem Finite.exists_ne_map_eq_of_infinite {α : Sort u_4} {β : Sort u_5} [Infinite α] [Finite β] (f : αβ) :
                                                ∃ (x : α) (y : α), x y f x = f y

                                                The pigeonhole principle for infinitely many pigeons in finitely many pigeonholes. If there are infinitely many pigeons in finitely many pigeonholes, then there are at least two pigeons in the same pigeonhole.

                                                See also: Fintype.exists_ne_map_eq_of_card_lt, Finite.exists_infinite_fiber.

                                                instance Function.Embedding.is_empty {α : Sort u_4} {β : Sort u_5} [Infinite α] [Finite β] :
                                                IsEmpty (α β)
                                                Equations
                                                • =
                                                theorem Finite.exists_infinite_fiber {α : Type u_1} {β : Type u_2} [Infinite α] [Finite β] (f : αβ) :
                                                ∃ (y : β), Infinite (f ⁻¹' {y})

                                                The strong pigeonhole principle for infinitely many pigeons in finitely many pigeonholes. If there are infinitely many pigeons in finitely many pigeonholes, then there is a pigeonhole with infinitely many pigeons.

                                                See also: Finite.exists_ne_map_eq_of_infinite

                                                theorem not_surjective_finite_infinite {α : Sort u_4} {β : Sort u_5} [Finite α] [Infinite β] (f : αβ) :
                                                theorem List.exists_pw_disjoint_with_card {α : Type u_4} [Fintype α] {c : List } (hc : c.sum Fintype.card α) :
                                                ∃ (o : List (List α)), List.map List.length o = c (∀ so, s.Nodup) List.Pairwise List.Disjoint o

                                                For any c : List whose sum is at most Fintype.card α, we can find o : List (List α) whose members have no duplicate, whose lengths given by c, and which are pairwise disjoint

                                                def truncOfCardPos {α : Type u_4} [Fintype α] (h : 0 < Fintype.card α) :

                                                A Fintype with positive cardinality constructively contains an element.

                                                Equations
                                                Instances For
                                                  theorem Fintype.induction_subsingleton_or_nontrivial {P : (α : Type u_4) → [inst : Fintype α] → Prop} (α : Type u_4) [Fintype α] (hbase : ∀ (α : Type u_4) [inst : Fintype α] [inst_1 : Subsingleton α], P α) (hstep : ∀ (α : Type u_4) [inst : Fintype α] [inst_1 : Nontrivial α], (∀ (β : Type u_4) [inst_2 : Fintype β], Fintype.card β < Fintype.card αP β)P α) :
                                                  P α

                                                  A custom induction principle for fintypes. The base case is a subsingleton type, and the induction step is for non-trivial types, and one can assume the hypothesis for smaller types (via Fintype.card).

                                                  The major premise is Fintype α, so to use this with the induction tactic you have to give a name to that instance and use that name.