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
  • s.powerset = { val := Multiset.pmap Finset.mk s.val.powerset , nodup := }
Instances For
    @[simp]
    theorem Finset.mem_powerset {α : Type u_1} {s : Finset α} {t : Finset α} :
    s t.powerset s t
    @[simp]
    theorem Finset.coe_powerset {α : Type u_1} (s : Finset α) :
    s.powerset = Finset.toSet ⁻¹' 𝒫s
    theorem Finset.empty_mem_powerset {α : Type u_1} (s : Finset α) :
    s.powerset
    theorem Finset.mem_powerset_self {α : Type u_1} (s : Finset α) :
    s s.powerset
    theorem Finset.powerset_nonempty {α : Type u_1} (s : Finset α) :
    s.powerset.Nonempty
    @[simp]
    theorem Finset.powerset_mono {α : Type u_1} {s : Finset α} {t : Finset α} :
    s.powerset t.powerset s t
    theorem Finset.powerset_injective {α : Type u_1} :
    Function.Injective Finset.powerset
    @[simp]
    theorem Finset.powerset_inj {α : Type u_1} {s : Finset α} {t : Finset α} :
    s.powerset = t.powerset s = t
    @[simp]
    theorem Finset.powerset_empty {α : Type u_1} :
    .powerset = {}
    @[simp]
    theorem Finset.powerset_eq_singleton_empty {α : Type u_1} {s : Finset α} :
    s.powerset = {} s =
    @[simp]
    theorem Finset.card_powerset {α : Type u_1} (s : Finset α) :
    s.powerset.card = 2 ^ s.card

    Number of Subsets of a Set

    theorem Finset.not_mem_of_mem_powerset_of_not_mem {α : Type u_1} {s : Finset α} {t : Finset α} {a : α} (ht : t s.powerset) (h : as) :
    at
    theorem Finset.powerset_insert {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) :
    (insert a s).powerset = s.powerset Finset.image (insert a) s.powerset
    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
    • s.ssubsets = s.powerset.erase s
    Instances For
      @[simp]
      theorem Finset.mem_ssubsets {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} :
      t s.ssubsets t s
      theorem Finset.empty_mem_ssubsets {α : Type u_1} [DecidableEq α] {s : Finset α} (h : s.Nonempty) :
      s.ssubsets
      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 : Finset α} {t : Finset α} :
                s Finset.powersetCard n t s t s.card = n
                @[simp]
                theorem Finset.powersetCard_mono {α : Type u_1} {n : } {s : Finset α} {t : Finset α} (h : s t) :
                @[simp]
                theorem Finset.card_powersetCard {α : Type u_1} (n : ) (s : Finset α) :
                (Finset.powersetCard n s).card = s.card.choose n

                Formula for the Number of Combinations

                @[simp]
                theorem Finset.powersetCard_zero {α : Type u_1} (s : Finset α) :
                theorem Finset.powersetCard_empty_subsingleton {α : Type u_1} (n : ) :
                (↑(Finset.powersetCard n )).Subsingleton
                @[simp]
                theorem Finset.map_val_val_powersetCard {α : Type u_1} (s : Finset α) (i : ) :
                theorem Finset.powersetCard_one {α : Type u_1} (s : Finset α) :
                Finset.powersetCard 1 s = Finset.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) :
                Finset.powersetCard (s.card + n) s =
                theorem Finset.powersetCard_eq_filter {α : Type u_1} {n : } {s : Finset α} :
                Finset.powersetCard n s = Finset.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 α} :
                (Finset.powersetCard n s).Nonempty n s.card
                @[simp]
                theorem Finset.powersetCard_self {α : Type u_1} (s : Finset α) :
                Finset.powersetCard s.card s = {s}
                theorem Finset.powerset_card_disjiUnion {α : Type u_1} (s : Finset α) :
                s.powerset = (Finset.range (s.card + 1)).disjiUnion (fun (i : ) => Finset.powersetCard i s)
                theorem Finset.powerset_card_biUnion {α : Type u_1} [DecidableEq (Finset α)] (s : Finset α) :
                s.powerset = (Finset.range (s.card + 1)).biUnion fun (i : ) => Finset.powersetCard i s
                theorem Finset.powersetCard_sup {α : Type u_1} [DecidableEq α] (u : Finset α) (n : ) (hn : n < u.card) :
                (Finset.powersetCard n.succ u).sup id = u
                theorem Finset.powersetCard_map {α : Type u_1} {β : Type u_2} (f : α β) (n : ) (s : Finset α) :