Finset.mem_powersetCard_univ
theorem Finset.mem_powersetCard_univ :
∀ {α : Type u_1} [inst : Fintype α] {s : Finset α} {k : ℕ}, s ∈ Finset.powersetCard k Finset.univ ↔ s.card = k := by
sorry
This theorem states that for any given type `α`, assumed to be a finite type, and any finite set `s` of this type along with a natural number `k`, `s` is a member of the power set of all `α` with cardinality `k` if and only if the cardinality of `s` equals `k`. In other words, a subset `s` of the universe set `α` is in the collection of all subsets of `α` of size `k` if and only if the size of `s` is `k`. This theorem essentially connects the properties of elements in the power set of a finite set with cardinality.
More concisely: For a finite type `α` and a finite subset `s` of `α`, `s` belongs to the power set of `α` with cardinality `k` if and only if the cardinality of `s` equals `k`.
|
Fintype.card_finset
theorem Fintype.card_finset : ∀ {α : Type u_1} [inst : Fintype α], Fintype.card (Finset α) = 2 ^ Fintype.card α := by
sorry
This theorem states that for any type `α` which is finite (represented by `[inst : Fintype α]`), the number of distinct finite subsets (or `Finset`s) of `α` is equal to 2 raised to the power of the number of elements in `α`. In mathematical terms, if `α` is a finite set with `n` elements, then the number of all possible subsets of `α` is `2^n`.
More concisely: For any finite type `α` with `n` elements, the number of distinct finite subsets of `α` is `2^n`.
|
Finset.powerset_univ
theorem Finset.powerset_univ : ∀ {α : Type u_1} [inst : Fintype α], Finset.univ.powerset = Finset.univ
This theorem states that, for any finite type `α`, the powerset of the universal set (denoted as `Finset.univ`) is equivalent to the universal set itself. In mathematical terms, if we consider all subsets (the powerset operation) of a universal set (which contains all objects of a particular type `α`), we end up with the universal set itself.
More concisely: For any finite type `α`, the powerset of `Finset.univ` (universal set) equals `Finset.univ`.
|