Documentation

Mathlib.Data.Fintype.Sets

Subsets of finite types #

In a Fintype, all Sets are automatically Finsets, and there are only finitely many of them.

Main results #

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

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

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

      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.

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

      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
          source
          @[simp]
          theorem Set.coe_toFinset {α : Type u_1} (s : Set α) [Fintype ↑s] :
          ↑s.toFinset = s
          source
          @[simp]
          theorem Set.toFinset_nonempty {α : Type u_1} {s : Set α} [Fintype ↑s] :
          s.toFinset.Nonempty ↔ s.Nonempty
          source
          theorem Set.Aesop.toFinset_nonempty_of_nonempty {α : Type u_1} {s : Set α} [Fintype ↑s] :
          s.Nonempty → s.toFinset.Nonempty

          Alias of the reverse direction of Set.toFinset_nonempty.

          source
          @[simp]
          theorem Set.toFinset_inj {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] :
          s.toFinset = t.toFinset ↔ s = t
          source
          theorem Set.toFinset_subset_toFinset {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] :
          s.toFinset ⊆ t.toFinset ↔ s ⊆ t
          source
          @[simp]
          theorem Set.toFinset_ssubset {α : Type u_1} {s : Set α} [Fintype ↑s] {t : Finset α} :
          s.toFinset ⊂ t ↔ s ⊂ ↑t
          source
          @[simp]
          theorem Set.subset_toFinset {α : Type u_1} {t : Set α} {s : Finset α} [Fintype ↑t] :
          s ⊆ t.toFinset ↔ ↑s ⊆ t
          source
          @[simp]
          theorem Set.ssubset_toFinset {α : Type u_1} {t : Set α} {s : Finset α} [Fintype ↑t] :
          s ⊂ t.toFinset ↔ ↑s ⊂ t
          source
          theorem Set.toFinset_ssubset_toFinset {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] :
          s.toFinset ⊂ t.toFinset ↔ s ⊂ t
          source
          @[simp]
          theorem Set.toFinset_subset {α : Type u_1} {s : Set α} [Fintype ↑s] {t : Finset α} :
          s.toFinset ⊆ t ↔ s ⊆ ↑t
          source
          theorem Set.toFinset_mono {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] :
          s ⊆ t → s.toFinset ⊆ t.toFinset

          Alias of the reverse direction of Set.toFinset_subset_toFinset.

          source
          theorem Set.toFinset_strict_mono {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] :
          s ⊂ t → s.toFinset ⊂ t.toFinset

          Alias of the reverse direction of Set.toFinset_ssubset_toFinset.

          source
          @[simp]
          theorem Set.disjoint_toFinset {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] :
          Disjoint s.toFinset t.toFinset ↔ Disjoint s t
          source
          @[simp]
          theorem Set.toFinset_nontrivial {α : Type u_1} {s : Set α} [Fintype ↑s] :
          s.toFinset.Nontrivial ↔ s.Nontrivial
          source
          @[simp]
          theorem Set.toFinset_inter {α : Type u_1} (s t : Set α) [DecidableEq α] [Fintype ↑s] [Fintype ↑t] [Fintype ↑(s ∩ t)] :
          (s ∩ t).toFinset = s.toFinset ∩ t.toFinset
          source
          @[simp]
          theorem Set.toFinset_union {α : Type u_1} (s t : Set α) [DecidableEq α] [Fintype ↑s] [Fintype ↑t] [Fintype ↑(s ∪ t)] :
          (s ∪ t).toFinset = s.toFinset ∪ t.toFinset
          source
          @[simp]
          theorem Set.toFinset_diff {α : Type u_1} (s t : Set α) [DecidableEq α] [Fintype ↑s] [Fintype ↑t] [Fintype ↑(s \ t)] :
          (s \ t).toFinset = s.toFinset \ t.toFinset
          source
          @[simp]
          theorem Set.toFinset_symmDiff {α : Type u_1} (s t : Set α) [DecidableEq α] [Fintype ↑s] [Fintype ↑t] [Fintype ↑(symmDiff s t)] :
          (symmDiff s t).toFinset = symmDiff s.toFinset t.toFinset
          source
          @[simp]
          theorem Set.toFinset_compl {α : Type u_1} (s : Set α) [DecidableEq α] [Fintype ↑s] [Fintype α] [Fintype ↑sᶜ] :
          sᶜ.toFinset = s.toFinsetᶜ
          source
          @[simp]
          theorem Set.toFinset_empty {α : Type u_1} [Fintype ↑∅] :
          ∅.toFinset = ∅
          source
          @[simp]
          theorem Set.toFinset_univ {α : Type u_1} [Fintype α] [Fintype ↑univ] :
          univ.toFinset = Finset.univ
          source
          @[simp]
          theorem Set.toFinset_eq_empty {α : Type u_1} {s : Set α} [Fintype ↑s] :
          s.toFinset = ∅ ↔ s = ∅
          source
          @[simp]
          theorem Set.toFinset_eq_univ {α : Type u_1} {s : Set α} [Fintype α] [Fintype ↑s] :
          s.toFinset = Finset.univ ↔ s = univ
          source
          @[simp]
          theorem Set.toFinset_setOf {α : Type u_1} [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype ↑{x : α | p x}] :
          {x : α | p x}.toFinset = Finset.filter p Finset.univ
          source
          theorem Set.toFinset_ssubset_univ {α : Type u_1} [Fintype α] {s : Set α} [Fintype ↑s] :
          s.toFinset ⊂ Finset.univ ↔ s ⊂ univ
          source
          @[simp]
          theorem Set.toFinset_image {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α → β) (s : Set α) [Fintype ↑s] [Fintype ↑(f '' s)] :
          (f '' s).toFinset = Finset.image f s.toFinset
          source
          @[simp]
          theorem Set.toFinset_range {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype β] (f : β → α) [Fintype ↑(range f)] :
          (range f).toFinset = Finset.image f Finset.univ
          source
          @[simp]
          theorem Set.toFinset_singleton {α : Type u_1} (a : α) [Fintype ↑{a}] :
          {a}.toFinset = {a}
          source
          @[simp]
          theorem Set.toFinset_insert {α : Type u_1} [DecidableEq α] {a : α} {s : Set α} [Fintype ↑(insert a s)] [Fintype ↑s] :
          (insert a s).toFinset = insert a s.toFinset
          source
          theorem Set.filter_mem_univ_eq_toFinset {α : Type u_1} [Fintype α] (s : Set α) [Fintype ↑s] [DecidablePred fun (x : α) => x ∈ s] :
          {x : α | x ∈ s} = s.toFinset
          source
          @[simp]
          theorem Finset.toFinset_coe {α : Type u_1} (s : Finset α) [Fintype ↑↑s] :
          (↑s).toFinset = s

          Fintype (s : Finset α) #

          source
          instance Finset.fintypeCoeSort {α : Type u} (s : Finset α) :
          Fintype { x : α // x ∈ s }
          Equations
            source
            @[simp]
            theorem Finset.univ_eq_attach {α : Type u} (s : Finset α) :
            univ = s.attach
            source
            theorem Fintype.coe_image_univ {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : α → β} :
            ↑(Finset.image f Finset.univ) = Set.range f
            source
            instance List.Subtype.fintype {α : Type u_1} [DecidableEq α] (l : List α) :
            Fintype { x : α // x ∈ l }
            Equations
              source
              instance Multiset.Subtype.fintype {α : Type u_1} [DecidableEq α] (s : Multiset α) :
              Fintype { x : α // x ∈ s }
              Equations
                source
                instance Finset.Subtype.fintype {α : Type u_1} (s : Finset α) :
                Fintype { x : α // x ∈ s }
                Equations
                  source
                  instance FinsetCoe.fintype {α : Type u_1} (s : Finset α) :
                  Fintype ↑↑s
                  Equations
                    source
                    theorem Finset.attach_eq_univ {α : Type u_1} {s : Finset α} :
                    s.attach = univ
                    source
                    instance Prop.fintype :
                    Fintype Prop
                    Equations
                      source
                      @[simp]
                      theorem Fintype.univ_Prop :
                      Finset.univ = {True, False}
                      source
                      instance Subtype.fintype {α : Type u_1} (p : α → Prop) [DecidablePred p] [Fintype α] :
                      Fintype { x : α // p x }
                      Equations
                        source
                        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
                            source
                            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
                              Instances For
                                source
                                @[simp]
                                theorem Fintype.coe_finsetEquivSet {α : Type u_1} [Fintype α] :
                                ⇑finsetEquivSet = Finset.toSet
                                source
                                @[simp]
                                theorem Fintype.finsetEquivSet_apply {α : Type u_1} [Fintype α] (s : Finset α) :
                                finsetEquivSet s = ↑s
                                source
                                @[simp]
                                theorem Fintype.finsetEquivSet_symm_apply {α : Type u_1} [Fintype α] (s : Set α) [Fintype ↑s] :
                                finsetEquivSet.symm s = s.toFinset
                                source
                                noncomputable def Fintype.finsetOrderIsoSet {α : Type u_1} [Fintype α] :
                                Finset α ≃o Set α

                                Given a fintype α, finsetOrderIsoSet is the order isomorphism between Finset α and Set α (all sets on a finite type are finite).

                                Equations
                                  Instances For
                                    source
                                    @[simp]
                                    theorem Fintype.finsetOrderIsoSet_toEquiv {α : Type u_1} [Fintype α] :
                                    finsetOrderIsoSet.toEquiv = finsetEquivSet
                                    source
                                    @[simp]
                                    theorem Fintype.coe_finsetOrderIsoSet {α : Type u_1} [Fintype α] :
                                    ⇑finsetOrderIsoSet = Finset.toSet
                                    source
                                    @[simp]
                                    theorem Fintype.coe_finsetOrderIsoSet_symm {α : Type u_1} [Fintype α] :
                                    ⇑finsetOrderIsoSet.symm = ⇑finsetEquivSet.symm
                                    source
                                    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
                                    source
                                    def finsetStx :
                                    Lean.ParserDescr

                                    finset% t elaborates t as a Finset. If t is a Set, then inserts Set.toFinset. Does not make use of the expected type; useful for big operators over finsets.

                                    #check finset% Finset.range 2 -- Finset Nat
#check finset% (Set.univ : Set Bool) -- Finset Bool
                                    Equations
                                      Instances For
                                        source
                                        def precheckFinsetStx :
                                        Lean.Elab.Term.Quotation.Precheck

                                        quot_precheck for the finset% syntax.

                                        Equations
                                          Instances For