Finset.pairwise_disjoint_powersetCard
theorem Finset.pairwise_disjoint_powersetCard :
∀ {α : Type u_1} (s : Finset α), Pairwise fun i j => Disjoint (Finset.powersetCard i s) (Finset.powersetCard j s)
The theorem `Finset.pairwise_disjoint_powersetCard` states that for any type `α` and any finset `s` of type `α`, the property `Pairwise` holds for two subsets of `s` generated by `Finset.powersetCard`. In other words, any two distinct subsets of `s` of given cardinalities are `Disjoint`. This means that for any element of the powerset of `s` with cardinality `i` and any element of the powerset of `s` with cardinality `j`, where `i` and `j` are distinct, the greatest element that is less than or equal to both subsets is the bottom element of the lattice structure, i.e., they have no common elements.
More concisely: For any type `α` and finset `s` of `α`, any two distinct subsets of `s` with different cardinalities have no common elements.
|
Finset.mem_powerset
theorem Finset.mem_powerset : ∀ {α : Type u_1} {s t : Finset α}, s ∈ t.powerset ↔ s ⊆ t
This theorem states that for any types `α` and finsets `s` and `t` of type `α`, `s` is a member of the powerset of `t` if and only if `s` is a subset of `t`. In other words, a set is in the powerset of `t` if all its elements also belong to `t`.
More concisely: For any type `α` and finsets `s` and `t` of type `α`, `s` is a subset of `t` if and only if `s` is an element of the powerset of `t`.
|
Finset.card_powersetCard
theorem Finset.card_powersetCard :
∀ {α : Type u_1} (n : ℕ) (s : Finset α), (Finset.powersetCard n s).card = s.card.choose n
This is a theorem stating the formula for the number of combinations. For any given type `α`, natural number `n`, and finite set `s` of type `α`, the cardinality of the power set of `s` with subsets of cardinality `n` (represented by `Finset.powersetCard n s`) is equal to the binomial coefficient of `s`'s cardinality choose `n`, denoted by `Nat.choose s.card n`. In essence, it is specifying the count of all possible `n`-element subsets that can be formed from an `n`-element set `s`.
More concisely: The cardinality of the set of subsets of a finite type `α` with cardinality `n` is equal to the binomial coefficient `Nat.choose n (cardinality of the set)`.
|
Finset.mem_powersetCard
theorem Finset.mem_powersetCard :
∀ {α : Type u_1} {n : ℕ} {s t : Finset α}, s ∈ Finset.powersetCard n t ↔ s ⊆ t ∧ s.card = n
The theorem `Finset.mem_powersetCard` states that for any given type `α`, integer `n` and finsets `s` and `t`, the finset `s` is an element of `Finset.powersetCard n t` if and only if `s` is a subset of `t` and the cardinality of `s` is `n`. In other words, a finset `s` belongs to the set of all subsets of `t` of size `n` precisely when `s` is a subset of `t` and has `n` elements.
More concisely: A finset `s` is an element of `Finset.powersetCard n` of a type `α` if and only if `s` is a subset of size `n` of another finset `t`.
|
Mathlib.Data.Finset.Powerset._auxLemma.6
theorem Mathlib.Data.Finset.Powerset._auxLemma.6 : ∀ {α : Type u_1} {s t : Finset α}, (s ∈ t.powerset) = (s ⊆ t) := by
sorry
This theorem states that for any type `α` and for any two finite sets `s` and `t` of type `α`, `s` is a member of the power set of `t` if and only if `s` is a subset of `t`. Here, the power set of a set `t` is the set of all possible subsets of `t`. In other words, a finite set `s` belongs to the power set of another finite set `t` precisely when all elements of `s` are also elements of `t`.
More concisely: For any types `α` and finite sets `s` and `t` of type `α`, `s` is a subset of `t` if and only if `s` is an element of the power set of `t`.
|
Finset.powersetCard.proof_1
theorem Finset.powersetCard.proof_1 :
∀ {α : Type u_1} (n : ℕ) (s : Finset α), ∀ _t ∈ Multiset.powersetCard n s.val, _t.Nodup
The theorem `Finset.powersetCard.proof_1` states that for any type `α`, any natural number `n`, and any Finset `s` of this type, any element `_t` in the multiset of all submultisets of `s` of length `n` (as obtained from the `Multiset.powersetCard` function) has no duplicates. In other words, the multiplicity of any element in `_t` is at most 1, as defined by `Multiset.Nodup`.
More concisely: For any type `α`, natural number `n`, and Finset `s` of type `α`, the multiset of all submultisets of `s` of length `n` as obtained from `Multiset.powersetCard` has no duplicate elements.
|
Finset.powerset_card_disjiUnion
theorem Finset.powerset_card_disjiUnion :
∀ {α : Type u_1} (s : Finset α),
s.powerset = (Finset.range (s.card + 1)).disjiUnion (fun i => Finset.powersetCard i s) ⋯
This theorem states that for any given finite set `s` of any type `α`, the powerset of `s` (i.e., the set of all subsets of `s`) is equal to the disjoint union of the sets of all subsets of `s` with cardinality `i`, where `i` ranges over the set of natural numbers less than or equal to the size of `s`. In other words, it partitions the powerset of `s` into subsets based on their sizes, and shows that their disjoint union is the entire powerset.
More concisely: The powerset of a finite set `s` is equal to the disjoint union of the sets of all subsets of `s` with a given cardinality, where the cardinality ranges over natural numbers less than or equal to the size of `s`.
|
Finset.powerset_insert
theorem Finset.powerset_insert :
∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α) (a : α),
(insert a s).powerset = s.powerset ∪ Finset.image (insert a) s.powerset
This theorem states that for any type `α` with decidable equality, a given finite set `s` of `α` and an element `a` of `α`, the powerset of the finite set resulting from inserting `a` into `s` is equal to the union of the powerset of `s` and the image of the finite set obtained by inserting `a` into each subset of the powerset of `s`. In other words, adding a new element to a set yields a powerset that contains all subsets of the original set, both with and without the new element.
More concisely: For any decidably equal type `α` and finite set `s` of `α`, the powerset of `s ∪ {a}` is equal to the set-union of the powerset of `s` and the images of each subset of `s` under the function x => x ∪ {a}.
|
Finset.mem_ssubsets
theorem Finset.mem_ssubsets : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, t ∈ s.ssubsets ↔ t ⊂ s := by
sorry
This theorem states that for any two finite sets `s` and `t` of an arbitrary type `α` with decidable equality, `t` is a member of the set of strict subsets of `s` (i.e., `t` is in `Finset.ssubsets s`) if and only if `t` is a strict subset of `s` (denoted as `t ⊂ s`). In other words, `t` is considered a strict subset of `s` (meaning `t` is contained in `s` but `t` and `s` are not equal) exactly when `t` is in the collection of strict subsets of `s`. This theorem provides a characterization of the membership in the collection of all strict subsets of a given finite set.
More concisely: For any finite sets `s` and `t` of type `α` with decidable equality, `t` is a strict subset of `s` if and only if `t` is an element of the set of strict subsets of `s` (`Finset.ssubsets s`).
|
Mathlib.Data.Finset.Powerset._auxLemma.15
theorem Mathlib.Data.Finset.Powerset._auxLemma.15 :
∀ {α : Type u_1} {n : ℕ} {s t : Finset α}, (s ∈ Finset.powersetCard n t) = (s ⊆ t ∧ s.card = n)
The theorem `Mathlib.Data.Finset.Powerset._auxLemma.15` states that for any type `α`, natural number `n`, and finsets `s` and `t` of type `α`, `s` is an element of the finset generated by the `powersetCard n t` function if and only if two conditions are met: (1) `s` is a subset of `t`, and (2) the cardinality (or size) of `s` is `n`. In other words, this theorem connects the concept of a powerset of a certain size with the properties of being a subset and having a specific cardinality.
More concisely: A finset of type `α` is an element of the finset generated by `powersetCard n t` if and only if it has size `n` and is a subset of `t`.
|
Finset.card_powerset
theorem Finset.card_powerset : ∀ {α : Type u_1} (s : Finset α), s.powerset.card = 2 ^ s.card
This theorem, referred to as the "Number of Subsets of a Set", states that for any finite set `s` of arbitrary type `α`, the number of subsets of `s` (captured by `(Finset.powerset s).card`) is equal to 2 raised to the power of the number of elements in `s` (expressed as `2 ^ s.card`). In mathematical terms, if `s` is a finite set with `n` elements, then the number of subsets of `s` is `2^n`.
More concisely: The number of subsets of a finite set `s` with `n` elements is equal to 2 raised to the power of `n`.
|