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
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem Finset.mem_powerset {α : Type u_1} {s : Finset α} {t : Finset α} :
    @[simp]
    theorem Finset.coe_powerset {α : Type u_1} (s : Finset α) :
    (Finset.powerset s) = Finset.toSet ⁻¹' 𝒫s
    theorem Finset.powerset_nonempty {α : Type u_1} (s : Finset α) :
    (Finset.powerset s).Nonempty
    @[simp]
    theorem Finset.powerset_mono {α : Type u_1} {s : Finset α} {t : Finset α} :
    theorem Finset.powerset_injective {α : Type u_1} :
    Function.Injective Finset.powerset
    @[simp]
    theorem Finset.powerset_inj {α : Type u_1} {s : Finset α} {t : Finset α} :
    @[simp]
    @[simp]
    theorem Finset.card_powerset {α : Type u_1} (s : Finset α) :
    (Finset.powerset s).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 Finset.powerset s) (h : as) :
    at
    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
    • One or more equations did not get rendered due to their size.
    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
    • One or more equations did not get rendered due to their size.
    def Finset.decidableExistsOfDecidableSubsets' {α : Type u_1} {s : Finset α} {p : Finset αProp} (hu : (t : Finset α) → t sDecidable (p t)) :
    Decidable (∃ (t : Finset α) (_ : t s), p t)

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

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

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

      Equations
      Instances For
        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 : Finset α} {t : Finset α} :
          theorem Finset.empty_mem_ssubsets {α : Type u_1} [DecidableEq α] {s : Finset α} (h : s.Nonempty) :
          instance 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
          • One or more equations did not get rendered due to their size.
          instance 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
          • One or more equations did not get rendered due to their size.
          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
              • One or more equations did not get rendered due to their size.
              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 = Nat.choose s.card n

                Formula for the Number of Combinations

                @[simp]
                theorem Finset.powersetCard_zero {α : Type u_1} (s : Finset α) :
                @[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' := (_ : Function.Injective singleton) } 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) (Finset.powerset s)
                theorem Finset.powersetCard_nonempty {α : Type u_1} {n : } {s : Finset α} (h : n s.card) :
                (Finset.powersetCard n s).Nonempty
                @[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 α) :
                Finset.powerset s = Finset.disjiUnion (Finset.range (s.card + 1)) (fun (i : ) => Finset.powersetCard i s) (_ : Set.Pairwise (Finset.range (s.card + 1)) fun (i j : ) => Disjoint (Finset.powersetCard i s) (Finset.powersetCard j 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 α) :