Down.card_compression
theorem Down.card_compression :
∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (𝒜 : Finset (Finset α)), (Down.compression a 𝒜).card = 𝒜.card := by
sorry
The theorem `Down.card_compression` states that for any type `α` that has decidable equality and for any element `a` of type `α` and any family of finite sets `𝒜` of type `α`, the process of down-compressing the family `𝒜` with respect to the element `a` does not change the size/cardinality of the family. In other words, down-compressing a family of finite sets, a process which involves removing an element from the sets that contain it (if the resulting set is not already in the family), does not affect the total number of sets within the family.
More concisely: For any type `α` with decidable equality and any family `𝒜` of finite sets of `α` with respect to an element `a` in `α`, the down-compression of `𝒜` does not alter the cardinality of `𝒜`.
|
Mathlib.Combinatorics.SetFamily.Compression.Down._auxLemma.4
theorem Mathlib.Combinatorics.SetFamily.Compression.Down._auxLemma.4 :
∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} {a : α},
(s ∈ Finset.memberSubfamily a 𝒜) = (insert a s ∈ 𝒜 ∧ a ∉ s)
This theorem states that for any type `α` with decidable equality, a given set `𝒜` of finite sets of `α`, a finite set `s` of `α`, and an element `a` of `α`, the set `s` belongs to the subfamily of `𝒜` obtained by removing `a` from its members (as defined by `Finset.memberSubfamily`) if and only if the set `s` with `a` inserted into it belongs to `𝒜` and `a` is not an element of `s`. This highlights a relation between the original family of sets `𝒜` and the derived family where `a` has been removed from each set.
More concisely: For any decidably equal type `α` and finite set `𝒜` of subsets of `α`, an element `a` in `α` belongs to the subfamily of `𝒜` obtained by removing `a` from its members if and only if the set `a ∪ s` belongs to `𝒜` for some finite `s` in `𝒜` without `a`.
|
Finset.memberFamily_induction_on
theorem Finset.memberFamily_induction_on :
∀ {α : Type u_1} [inst : DecidableEq α] {p : Finset (Finset α) → Prop} (𝒜 : Finset (Finset α)),
p ∅ →
p {∅} →
(∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄,
p (Finset.nonMemberSubfamily a 𝒜) → p (Finset.memberSubfamily a 𝒜) → p 𝒜) →
p 𝒜
This is a theorem that establishes the induction principle for families of finite sets. In order to prove a statement for every family of finite sets, the theorem states that it is sufficient to prove it for:
- the family that consists of no finite sets,
- the family that only contains the empty set,
- the family obtained by taking the union of two families `ℬ` and `{s ∪ {a} | s ∈ 𝒞}`, under the assumption that the statement holds for `ℬ` and `𝒞`, where `a` is an element of the ground type and `𝒜` and `ℬ` are families of finite sets that do not contain `a`.
Instead of directly providing `ℬ` and `𝒞`, the `subfamily` case in the theorem gives the equality `𝒜 = ℬ ∪ {s ∪ {a} | s ∈ 𝒞}`, which implies `ℬ = 𝒜.nonMemberSubfamily` and `𝒞 = 𝒜.memberSubfamily`.
This theorem can be seen as a formalization of induction on `n` where `𝒜` is a family of finite sets with `n` elements.
More concisely: The theorem states that to prove a statement for every family of finite sets, it suffices to verify it for the empty family, the family containing only the empty set, and the family obtained by adding an element to a family, under the assumption that the statement holds for the subfamilies of sets not containing that element.
|
Down.compression_idem
theorem Down.compression_idem :
∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (𝒜 : Finset (Finset α)),
Down.compression a (Down.compression a 𝒜) = Down.compression a 𝒜
This theorem states that the operation of down-compressing a family is idempotent. In other words, for any type `α` with decidable equality, any element `a` of type `α`, and any finset `𝒜` of finsets of type `α`, applying the down-compression operation to `𝒜` twice with the same element `a` will yield the same result as applying it once. This means that once `𝒜` has been down-compressed with `a`, subsequent down-compressions with `a` do not modify `𝒜` any further.
More concisely: For any type `α` with decidable equality, any element `a` of type `α`, and any finset `𝒜` of finsets of `α`, down-compressing `𝒜` twice with `a` yields the same result as down-compressing it once.
|
Mathlib.Combinatorics.SetFamily.Compression.Down._auxLemma.2
theorem Mathlib.Combinatorics.SetFamily.Compression.Down._auxLemma.2 :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α} {b : β},
(b ∈ Finset.image f s) = ∃ a ∈ s, f a = b
This theorem states that for any types `α` and `β` with a decidable equality on `β`, a function `f` from `α` to `β`, a finite set `s` of elements of type `α`, and an element `b` of type `β`, `b` is in the image of `s` under `f` if and only if there exists an element `a` in `s` such that `f(a)` equals `b`. This theorem thus characterizes the image of a finite set under a function in terms of the function's values on the elements of the set.
More concisely: For any decidable type `β`, finite set `s` of elements from type `α`, and function `f` from `α` to `β`, an element `b` is in the image of `s` under `f` if and only if there exists an element `a` in `s` such that `f(a) = b`.
|
Finset.family_induction_on
theorem Finset.family_induction_on :
∀ {α : Type u_1} [inst : DecidableEq α] {p : Finset (Finset α) → Prop} (𝒜 : Finset (Finset α)),
p ∅ →
p {∅} →
(∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, (∀ s ∈ 𝒜, a ∉ s) → p 𝒜 → p (Finset.image (insert a) 𝒜)) →
(∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄,
p (Finset.filter (fun x => a ∉ x) 𝒜) → p (Finset.filter (fun x => a ∈ x) 𝒜) → p 𝒜) →
p 𝒜
This theorem provides an induction principle for families of finite sets. To demonstrate a property `p` for all families of finite sets `𝒜`, it is enough to show:
1. Property `p` holds for the empty family.
2. Property `p` holds for the family that only includes the empty set.
3. If `p` holds for a family `𝒜` where `𝒜` does not contain a specific element `a` in any of its sets, then `p` also holds for the family created by adding `a` to every set in `𝒜`.
4. If `p` holds for a family `ℬ` and a family `𝒞`, where `ℬ` is a family not containing `a` in any of its sets and `𝒞` is a family that contains `a` in all of its sets, then `p` holds for the union of `ℬ` and `𝒞`.
This forms a means of structuring induction on `n` where `𝒜` is a family of finite sets with `n` elements. Note that the families `ℬ` and `𝒞` are derived from `𝒜` by filtering out sets according to whether they contain `a` or not.
More concisely: The theorem states that to prove a property for all families of finite sets, it suffices to verify it for the empty family, the family consisting only of the empty set, and show that if the property holds for families without a specific element and with that element in every set, then it holds for their union.
|
Mathlib.Combinatorics.SetFamily.Compression.Down._auxLemma.3
theorem Mathlib.Combinatorics.SetFamily.Compression.Down._auxLemma.3 :
∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Finset α} {a : α},
(a ∈ Finset.filter p s) = (a ∈ s ∧ p a)
This theorem states that for any type `α`, any decidable predicate `p` on `α`, any finite set `s` of `α`, and any element `a` of `α`, the element `a` is in the filtered set `s` under predicate `p` if and only if `a` is in the original set `s` and `a` satisfies the predicate `p`. In other words, the filtered set contains exactly those elements of the original set which satisfy the predicate.
More concisely: For any type `α`, decidable predicate `p` on `α`, and finite set `s` of `α`, the filtered set `s` under `p` equals the set of elements in `s` that satisfy `p`.
|
Down.mem_compression
theorem Down.mem_compression :
∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} {a : α},
s ∈ Down.compression a 𝒜 ↔ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s ∉ 𝒜 ∧ insert a s ∈ 𝒜
The theorem `Down.mem_compression` states that for any type `α` with decidable equality, any `𝒜` which is a finite set of finite sets of α, any finite set `s` of α, and any element `a` of `α`, `s` belongs to the down-compressed family of `𝒜` by `a` if and only if either `s` is in `𝒜` and the set obtained by removing `a` from `s` is in `𝒜`, or `s` is not in `𝒜` but the set obtained by adding `a` to `s` is in `𝒜`. In simpler terms, it gives the conditions under which a set `s` is in the down-compressed family produced by applying a down-compression operation to `𝒜` by `a`.
More concisely: For any decidably equal type `α` and finite set `𝒜` of finite sets of `α`, an element `a` of `α` belongs to the down-compressed family of `𝒜` by `a` if and only if `s` is in `𝒜` with `a` removed or not in `𝒜` with `a` added.
|
Mathlib.Combinatorics.SetFamily.Compression.Down._auxLemma.1
theorem Mathlib.Combinatorics.SetFamily.Compression.Down._auxLemma.1 :
∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} {a : α},
(s ∈ Finset.nonMemberSubfamily a 𝒜) = (s ∈ 𝒜 ∧ a ∉ s)
This theorem states that for any type `α` with decidable equality, any finite set `𝒜` of finite sets of `α`, and any finite set `s` of `α` and element `a` of `α`, the set `s` is in the subfamily of `𝒜` that does not contain `a` (i.e., `Finset.nonMemberSubfamily a 𝒜`) if and only if `s` is in `𝒜` and `a` is not in `s`. In mathematical terms, this theorem is asserting that membership in the subfamily of sets not containing a particular element is equivalent to membership in the original set family and non-membership of the specified element.
More concisely: For any decidably equated type `α` and finite sets `𝒜` of finite sets of `α`, and `s ∈ 𝒜` and `a ∈ α`, `Finset.nonMemberSubfamily a 𝒜` holds if and only if `s ∈ 𝒜` and `a ∉ s`.
|