Finset.slice_subset
theorem Finset.slice_subset : ∀ {α : Type u_1} {𝒜 : Finset (Finset α)} {r : ℕ}, 𝒜.slice r ⊆ 𝒜
The theorem states that for any type `α`, any finite set `𝒜` of finite sets of `α`, and any natural number `r`, the `r`-th slice of `𝒜` is a subset of `𝒜`. In other words, if we take a finite set of finite sets and partition it into slices based on some natural number, each of these slices will be contained within the original set.
More concisely: For any type `α`, any finite set `𝒜` of finite subsets of `α`, and any natural number `r`, the `r`-th slice of `𝒜` is a subset of `𝒜`. (In other words, for all `i` with `0 ≤ i < (card `𝒜`) / `r`, the `i`-th slice of `𝒜` is the set of sets in `𝒜` with index `i` modulo `(card `𝒜`) equal to `r`.)
|
Set.Sized.subset_powersetCard_univ
theorem Set.Sized.subset_powersetCard_univ :
∀ {α : Type u_1} [inst : Fintype α] {𝒜 : Finset (Finset α)} {r : ℕ},
Set.Sized r ↑𝒜 → 𝒜 ⊆ Finset.powersetCard r Finset.univ
The theorem `Set.Sized.subset_powersetCard_univ` states that for any type `α`, given an instance of `Fintype α` (which implies that `α` is a finite type), a finite set of finite sets `𝒜` (of type `Finset (Finset α)`), and a natural number `r`, if every set in `𝒜` has cardinality `r` (expressed as `Set.Sized r ↑𝒜`), then `𝒜` is a subset of the power set of `Finset.univ` (the universal finite set of type `α`), where only subsets of cardinality `r` are considered (expressed as `𝒜 ⊆ Finset.powersetCard r Finset.univ`). In other words, if all subsets in `𝒜` have `r` elements, then all subsets in `𝒜` are also subsets of the set of all `r`-element subsets of the universe.
More concisely: If `α` is a finite type, `𝒜` is a finite set of finite subsets of `α` of cardinality `r`, and every set in `𝒜` is a subset of the universal set of finite subsets of `α` of cardinality `r`, then `𝒜` is a subset of the power set of the universal set.
|
Set.sized.union
theorem Set.sized.union :
∀ {α : Type u_1} {A B : Set (Finset α)} {r : ℕ}, Set.Sized r A ∧ Set.Sized r B → Set.Sized r (A ∪ B)
The theorem `Set.sized.union` states that for all types `α`, sets `A` and `B` of finite sets (`Finset`) of elements of type `α`, and a natural number `r`, if every finite set in `A` has `r` elements and every finite set in `B` also has `r` elements (i.e., `A` and `B` are both `r`-sized), then every finite set in the union of `A` and `B` also has `r` elements. In other words, the union of two `r`-sized sets of finite sets is also an `r`-sized set of finite sets.
More concisely: If `A` and `B` are `r`-sized families of finite sets of elements of type `α`, then the union of `A` and `B` is also an `r`-sized family of finite sets.
|
Finset.sized_slice
theorem Finset.sized_slice : ∀ {α : Type u_1} {𝒜 : Finset (Finset α)} {r : ℕ}, Set.Sized r ↑(𝒜.slice r)
The theorem `Finset.sized_slice` states that for any type `α`, any finite set `𝒜` of finite sets of type `α`, and any natural number `r`, every finite set in the `r`-th slice of `𝒜` has size `r`. In other words, if we take the `r`-th slice of `𝒜` (which is a set of finite sets), each of these resulting sets has exactly `r` elements.
More concisely: For any type `α`, given a finite set `𝒜` of finite sets of `α` and a natural number `r`, every set in the `r`-th slice of `𝒜` has size `r`.
|
Finset.mem_slice
theorem Finset.mem_slice :
∀ {α : Type u_1} {𝒜 : Finset (Finset α)} {A : Finset α} {r : ℕ}, A ∈ 𝒜.slice r ↔ A ∈ 𝒜 ∧ A.card = r
The theorem `Finset.mem_slice` states that for any type `α`, any set `𝒜` of finite sets of `α`, any finite set `A` of `α`, and any natural number `r`, `A` belongs to the `r`-th slice of `𝒜` if and only if `A` belongs to `𝒜` and the cardinality of `A` is `r`. Here, the `r`-th slice of a set family is defined as the subset of its elements that have cardinality `r`.
More concisely: For any type `α` and set `𝒜` of finite sets of `α`, a finite set `A` belongs to the `r`-th slice of `𝒜` if and only if `A` is an element of `𝒜` with cardinality `r`.
|
Finset.ne_of_mem_slice
theorem Finset.ne_of_mem_slice :
∀ {α : Type u_1} {𝒜 : Finset (Finset α)} {A₁ A₂ : Finset α} {r₁ r₂ : ℕ},
A₁ ∈ 𝒜.slice r₁ → A₂ ∈ 𝒜.slice r₂ → r₁ ≠ r₂ → A₁ ≠ A₂
This theorem states that for any type `α` and a finset `𝒜` of finsets of this type, if `A₁` and `A₂` are finsets of `α` present in different slices (`r₁` and `r₂`) of `𝒜`, then `A₁` and `A₂` must be distinct provided that `r₁` and `r₂` are distinct. In other words, elements in different slices of a finset of finsets must be distinct.
More concisely: For any type `α` and finset `𝒜` of finsets of `α`, if `A₁` and `A₂` are distinct finsets of `α` in different slices of `𝒜`, then `A₁` and `A₂` are disparate (i.e., neither equal nor a subset of the other).
|