Documentation

Mathlib.Data.Finset.Powerset

The powerset of a finset #

powerset #

def Finset.powerset {α : Type u_1} (s : Finset α) :

When s is a finset, s.powerset is the finset of all subsets of s (seen as finsets).

Equations
    Instances For
      @[simp]
      theorem Finset.mem_powerset {α : Type u_1} {s t : Finset α} :
      @[simp]
      theorem Finset.coe_powerset {α : Type u_1} (s : Finset α) :
      theorem Finset.mem_powerset_self {α : Type u_1} (s : Finset α) :
      @[simp]
      theorem Finset.powerset_mono {α : Type u_1} {s t : Finset α} :
      @[simp]
      theorem Finset.powerset_inj {α : Type u_1} {s t : Finset α} :
      @[simp]
      @[simp]
      @[simp]
      theorem Finset.card_powerset {α : Type u_1} (s : Finset α) :

      Number of Subsets of a Set

      theorem Finset.notMem_of_mem_powerset_of_notMem {α : Type u_1} {s t : Finset α} {a : α} (ht : t s.powerset) (h : as) :
      at
      @[deprecated Finset.notMem_of_mem_powerset_of_notMem (since := "2025-05-23")]
      theorem Finset.not_mem_of_mem_powerset_of_not_mem {α : Type u_1} {s t : Finset α} {a : α} (ht : t s.powerset) (h : as) :
      at

      Alias of Finset.notMem_of_mem_powerset_of_notMem.

      theorem Finset.powerset_insert {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) :
      theorem Finset.pairwiseDisjoint_pair_insert {α : Type u_1} {s : Finset α} [DecidableEq α] {a : α} (ha : as) :
      (↑s.powerset).PairwiseDisjoint fun (t : Finset α) => {t, insert a t}
      instance Finset.decidableExistsOfDecidableSubsets {α : Type u_1} {s : Finset α} {p : (t : Finset α) → t sProp} [(t : Finset α) → (h : t s) → Decidable (p t h)] :
      Decidable (∃ (t : Finset α) (h : t s), p t h)

      For predicate p decidable on subsets, it is decidable whether p holds for any subset.

      Equations
        instance Finset.decidableForallOfDecidableSubsets {α : Type u_1} {s : Finset α} {p : (t : Finset α) → t sProp} [(t : Finset α) → (h : t s) → Decidable (p t h)] :
        Decidable (∀ (t : Finset α) (h : t s), p t h)

        For predicate p decidable on subsets, it is decidable whether p holds for every subset.

        Equations
          instance Finset.decidableExistsOfDecidableSubsets' {α : Type u_1} {s : Finset α} {p : Finset αProp} [(t : Finset α) → Decidable (p t)] :
          Decidable (∃ ts, p t)

          For predicate p decidable on subsets, it is decidable whether p holds for any subset.

          Equations
            instance Finset.decidableForallOfDecidableSubsets' {α : Type u_1} {s : Finset α} {p : Finset αProp} [(t : Finset α) → Decidable (p t)] :
            Decidable (∀ ts, p t)

            For predicate p decidable on subsets, it is decidable whether p holds for every subset.

            Equations
              def Finset.ssubsets {α : Type u_1} [DecidableEq α] (s : Finset α) :

              For s a finset, s.ssubsets is the finset comprising strict subsets of s.

              Equations
                Instances For
                  @[simp]
                  theorem Finset.mem_ssubsets {α : Type u_1} [DecidableEq α] {s t : Finset α} :
                  theorem Finset.empty_mem_ssubsets {α : Type u_1} [DecidableEq α] {s : Finset α} (h : s.Nonempty) :
                  def Finset.decidableExistsOfDecidableSSubsets {α : Type u_1} [DecidableEq α] {s : Finset α} {p : (t : Finset α) → t sProp} [(t : Finset α) → (h : t s) → Decidable (p t h)] :
                  Decidable (∃ (t : Finset α) (h : t s), p t h)

                  For predicate p decidable on ssubsets, it is decidable whether p holds for any ssubset.

                  Equations
                    Instances For
                      def Finset.decidableForallOfDecidableSSubsets {α : Type u_1} [DecidableEq α] {s : Finset α} {p : (t : Finset α) → t sProp} [(t : Finset α) → (h : t s) → Decidable (p t h)] :
                      Decidable (∀ (t : Finset α) (h : t s), p t h)

                      For predicate p decidable on ssubsets, it is decidable whether p holds for every ssubset.

                      Equations
                        Instances For
                          def Finset.decidableExistsOfDecidableSSubsets' {α : Type u_1} [DecidableEq α] {s : Finset α} {p : Finset αProp} (hu : (t : Finset α) → t sDecidable (p t)) :
                          Decidable (∃ (t : Finset α) (_ : t s), p t)

                          A version of Finset.decidableExistsOfDecidableSSubsets with a non-dependent p. Typeclass inference cannot find hu here, so this is not an instance.

                          Equations
                            Instances For
                              def Finset.decidableForallOfDecidableSSubsets' {α : Type u_1} [DecidableEq α] {s : Finset α} {p : Finset αProp} (hu : (t : Finset α) → t sDecidable (p t)) :
                              Decidable (∀ ts, p t)

                              A version of Finset.decidableForallOfDecidableSSubsets with a non-dependent p. Typeclass inference cannot find hu here, so this is not an instance.

                              Equations
                                Instances For
                                  def Finset.powersetCard {α : Type u_1} (n : ) (s : Finset α) :

                                  Given an integer n and a finset s, then powersetCard n s is the finset of subsets of s of cardinality n.

                                  Equations
                                    Instances For
                                      @[simp]
                                      theorem Finset.mem_powersetCard {α : Type u_1} {n : } {s t : Finset α} :
                                      s powersetCard n t s t s.card = n
                                      @[simp]
                                      theorem Finset.powersetCard_mono {α : Type u_1} {n : } {s t : Finset α} (h : s t) :
                                      @[simp]
                                      theorem Finset.card_powersetCard {α : Type u_1} (n : ) (s : Finset α) :

                                      Formula for the Number of Combinations

                                      @[simp]
                                      theorem Finset.powersetCard_zero {α : Type u_1} (s : Finset α) :
                                      theorem Finset.powersetCard_one {α : Type u_1} (s : Finset α) :
                                      powersetCard 1 s = map { toFun := singleton, inj' := } s
                                      @[simp]
                                      theorem Finset.powersetCard_eq_empty {α : Type u_1} {n : } {s : Finset α} :
                                      @[simp]
                                      theorem Finset.powersetCard_card_add {α : Type u_1} {n : } (s : Finset α) (hn : 0 < n) :
                                      theorem Finset.powersetCard_eq_filter {α : Type u_1} {n : } {s : Finset α} :
                                      powersetCard n s = filter (fun (x : Finset α) => x.card = n) s.powerset
                                      theorem Finset.powersetCard_succ_insert {α : Type u_1} [DecidableEq α] {x : α} {s : Finset α} (h : xs) (n : ) :
                                      @[simp]
                                      theorem Finset.powersetCard_nonempty {α : Type u_1} {n : } {s : Finset α} :
                                      theorem Finset.powersetCard_nonempty_of_le {α : Type u_1} {n : } {s : Finset α} :

                                      Alias of the reverse direction of Finset.powersetCard_nonempty.

                                      @[simp]
                                      theorem Finset.powersetCard_self {α : Type u_1} (s : Finset α) :
                                      theorem Finset.powerset_card_disjiUnion {α : Type u_1} (s : Finset α) :
                                      s.powerset = (range (s.card + 1)).disjiUnion (fun (i : ) => powersetCard i s)
                                      theorem Finset.powerset_card_biUnion {α : Type u_1} [DecidableEq (Finset α)] (s : Finset α) :
                                      s.powerset = (range (s.card + 1)).biUnion fun (i : ) => powersetCard i s
                                      theorem Finset.powersetCard_sup {α : Type u_1} [DecidableEq α] (u : Finset α) (n : ) (hn : n < u.card) :
                                      theorem Finset.powersetCard_map {α : Type u_1} {β : Type u_2} (f : α β) (n : ) (s : Finset α) :