sup_sdiff_injOn
theorem sup_sdiff_injOn :
∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] (u v : α),
Set.InjOn (fun x => (x ⊔ u) \ v) {x | Disjoint u x ∧ v ≤ x}
The theorem `sup_sdiff_injOn` states that for any type `α` that forms a `GeneralizedBooleanAlgebra`, and any two elements `u` and `v` of `α`, the function `x` maps to `(x ⊔ u) \ v` is injective on the set of elements `x` which are disjoint from `u` and greater than or equal to `v`. This is termed as UV-compression being injective on the elements it moves. Here, `\` operation indicates the difference of two elements in the Boolean algebra context, `⊔` denotes the supremum or join operation, and `Disjoint` refers to two elements whose infimum is the bottom element.
More concisely: For any `α` that is a `GeneralizedBooleanAlgebra` and for all `u, v ∈ α` with `u ⊥ v` and `v ≤ x`, the function `x ↦ (x ⊔ u) \ v` is injective.
|
UV.compress_injOn
theorem UV.compress_injOn :
∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint]
[inst_2 : DecidableRel fun x x_1 => x ≤ x_1] {s : Finset α} {u v : α} [inst_3 : DecidableEq α],
Set.InjOn (UV.compress u v) ↑(Finset.filter (fun x => UV.compress u v x ∉ s) s)
The given theorem states that the UV-compression function is injective on the sets that are not compressed by UV. Here, the UV-compression is a function used in the analysis of Boolean algebras.
The theorem is applicable in a generalized Boolean algebra, provided that there are decidable relations for disjointness and the less-than-or-equal-to operation. Given a finite set `s` and two elements `u` and `v` of the algebra, and provided that equality in the algebra is decidable, the theorem asserts that if we filter out elements of `s` that are compressed by UV, the remaining elements are distinct under the UV-compression - in other words, the UV-compression function does not map two different elements of this filtered set to the same element. Hence, UV-compression is injective on the sets that are not UV-compressed.
More concisely: In a generalized Boolean algebra with decidable equality, disjointness, and less-than-or-equal-to relations, the UV-compression function is injective on the sets of elements not compressed by UV.
|
UV.card_shadow_compression_le
theorem UV.card_shadow_compression_le :
∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} (u v : Finset α),
(∀ x ∈ u, ∃ y ∈ v, UV.IsCompressed (u.erase x) (v.erase y) 𝒜) →
(UV.compression u v 𝒜).shadow.card ≤ 𝒜.shadow.card
The theorem `UV.card_shadow_compression_le` states that for any type `α` with a decidable equality and any sets `𝒜`, `u`, and `v` of this type, if for every element `x` in `u` there exists an element `y` in `v` such that `𝒜` is compressed under the operation of erasing `x` from `u` and `y` from `v`, then the cardinality (size) of the "shadow" of the set `𝒜` under the UV-compression operation applied to `u` and `v` is less than or equal to the cardinality of the original "shadow" of `𝒜`. This is a key fact needed for the Kruskal-Katona theorem in combinatorial mathematics.
In this context, the "shadow" of a set is a specific derived set, and the UV-compression is an operation that transforms sets in a particular way. The concept of "compressed" used here refers to a set remaining the same after the UV-compression operation, as defined by `UV.IsCompressed`.
More concisely: If for all x in set u and y in set v, the set A is unchanged under the UV-compression of erasing x from u and y from v, then the cardinality of A's shadow under UV-compression of u and v is less than or equal to the cardinality of A's original shadow.
|
UV.compress_idem
theorem UV.compress_idem :
∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint]
[inst_2 : DecidableRel fun x x_1 => x ≤ x_1] (u v a : α),
UV.compress u v (UV.compress u v a) = UV.compress u v a
The theorem `UV.compress_idem` states that for any generalized Boolean algebra `α` (where `α` is a type), given the decidable relations `Disjoint` and `≤` (less than or equal), and for any elements `u`, `v`, and `a` of this algebra, applying the `UV.compress` function twice to `a` with the same `u` and `v` is the same as applying it once. In other words, the `UV.compress` function is idempotent on this algebra, meaning that applying it multiple times does not change the result after the first application.
More concisely: For any generalized Boolean algebra `α` with decidable relations `Disjoint` and `≤`, the `UV.compress` function is idempotent: `UV.compress (UV.compress a u v) = UV.compress a u v`.
|
UV.shadow_compression_subset_compression_shadow
theorem UV.shadow_compression_subset_compression_shadow :
∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} (u v : Finset α),
(∀ x ∈ u, ∃ y ∈ v, UV.IsCompressed (u.erase x) (v.erase y) 𝒜) →
(UV.compression u v 𝒜).shadow ⊆ UV.compression u v 𝒜.shadow
The theorem `UV.shadow_compression_subset_compression_shadow` states that for any type `α` with decidable equality, and for any finite sets `𝒜`, `u`, and `v` of elements of type `α`, if for every element `x` in `u` there exists an element `y` in `v` such that `𝒜` is compressed with respect to the sets `u` and `v` after erasing the elements `x` and `y`, then the shadow of the compressed version of `𝒜` with respect to `u` and `v` is a subset of the compression of the shadow of `𝒜` with respect to `u` and `v`. This theorem is a crucial part of the compression arguments in the Kruskal-Katona theorem, which is a fundamental result in combinatorics.
More concisely: If `α` has decidable equality, for finite sets `𝒜`, `u`, and `v` in `α` such that for each `x in u` there exists `y in v` with `𝒜` compressed with respect to `u` and `v` after erasing `x` and `y`, then the shadow of the compressed `𝒜` with respect to `u` and `v` is a subset of the compression of the shadow of `𝒜` with respect to `u` and `v`.
|
UV.card_compression
theorem UV.card_compression :
∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint]
[inst_2 : DecidableRel fun x x_1 => x ≤ x_1] [inst_3 : DecidableEq α] (u v : α) (s : Finset α),
(UV.compression u v s).card = s.card
The theorem `UV.card_compression` states that for any type `α` that is a generalized Boolean algebra, with a decidable relation of disjointness (`Disjoint`), a decidable relation of order (`x ≤ x_1`), and decidable equality (`DecidableEq α`), the cardinality or size of a set `s` remains unchanged after a compression operation `UV.compression u v s`. In other words, compressing a set using `UV.compression` does not change its size.
More concisely: For any generalized Boolean algebra `α` with decidable disjointness, order, and equality, the cardinality of a set is preserved under the compression operation `UV.compression`.
|
UV.card_compress
theorem UV.card_compress :
∀ {α : Type u_1} [inst : DecidableEq α] {u v : Finset α},
u.card = v.card → ∀ (a : Finset α), (UV.compress u v a).card = a.card
The theorem `UV.card_compress` states that for any type `α` with decidable equality, and given any two finite sets `u` and `v` of type `α`, if `u` and `v` have the same number of elements (i.e., `u.card = v.card`), then for any finite set `a` of type `α`, the operation `UV.compress u v a` does not change the number of elements in `a` (i.e., `(UV.compress u v a).card = a.card`). This theorem essentially guarantees that the `UV.compress` operation preserves the cardinality of the set on which it operates.
More concisely: For any type `α` with decidable equality, if two finite sets `u` and `v` of type `α` have the same number of elements, then applying the `UV.compress` operation to `u`, `v`, and any finite set `a` of type `α` results in a set with the same number of elements as `a`.
|
UV.mem_of_mem_compression
theorem UV.mem_of_mem_compression :
∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint]
[inst_2 : DecidableRel fun x x_1 => x ≤ x_1] {s : Finset α} {u v a : α} [inst_3 : DecidableEq α],
a ∈ UV.compression u v s → v ≤ a → (v = ⊥ → u = ⊥) → a ∈ s
This theorem states that for any type `α` that is a generalized boolean algebra with decidable relations for disjointness and order, a finite set `s` of `α`, and elements `u`, `v`, and `a` of `α` where `α` has decidable equality, if `a` is in the `u,v`-compression of `s` and `v` is less than or equal to `a`, then `a` must have been in the original set `s`. The assumption that `v` is less than or equal to `a` is further strengthened by an implication that if `v` is the bottom element, then `u` must also be the bottom element. The `u,v`-compression here likely refers to a specific operation applied to the set `s` with respect to elements `u` and `v`.
More concisely: If `α` is a finite, decidably ordered and boolean algebra with decidable disjointness, `s` is a finite subset of `α`, `a` is in the `u,v`-compression of `s` and `v` is less than or equal to `a` (or `v` is the bottom element and `u` is also the bottom element), then `a` was originally in `s`.
|
UV.compress_sdiff_sdiff
theorem UV.compress_sdiff_sdiff :
∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint]
[inst_2 : DecidableRel fun x x_1 => x ≤ x_1] (a b : α), UV.compress (a \ b) (b \ a) b = a
This theorem states that for any two elements `a` and `b` of a type `α` that forms a Generalized Boolean Algebra, and where the relations `Disjoint` and `≤` are decidable, we can transform `b` into `a` by applying the `UV.compress` function using the differences `a \ b` and `b \ a`. Here, `a \ b` and `b \ a` represent the elements in `a` that are not in `b`, and the elements in `b` that are not in `a`, respectively. Hence, the operation `UV.compress (a \ b) (b \ a) b` effectively removes from `b` what is only in `b` and adds to it what is only in `a`, thereby transforming `b` into `a`.
More concisely: For any two elements `a` and `b` in a decidably ordered and disjointed Generalized Boolean Algebra, `UV.compress (a \ b) (b \ a) b` equals `a`.
|
UV.isCompressed_self
theorem UV.isCompressed_self :
∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint]
[inst_2 : DecidableRel fun x x_1 => x ≤ x_1] [inst_3 : DecidableEq α] (u : α) (s : Finset α),
UV.IsCompressed u u s
The theorem `UV.isCompressed_self` states that for any type `α` that forms a generalized Boolean algebra, and where the relations "disjoint", "less than or equal to", and "equal to" are decidable, any finset `s` is considered to be compressed along two identical elements `u`. In other words, if you take any element `u` from this type and any finset `s`, the UV-compression of `s` with respect to `u` and `u` is equal to `s` itself.
More concisely: For any type `α` forming a generalized Boolean algebra with decidable disjointness, less than or equal to, and equality relations, the UV-compression of a finset `s` with respect to identical elements `u` is equal to `s` itself.
|
UV.compression_idem
theorem UV.compression_idem :
∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint]
[inst_2 : DecidableRel fun x x_1 => x ≤ x_1] [inst_3 : DecidableEq α] (u v : α) (s : Finset α),
UV.compression u v (UV.compression u v s) = UV.compression u v s
The theorem `UV.compression_idem` states that for any type `α` that forms a generalized boolean algebra, and where the relations 'disjointness', 'less than or equal to' and 'equality' are decidable, the operation `UV.compression` is idempotent. This means, applying the `UV.compression` operation twice to a finite set `s` with the same parameters `u` and `v` will yield the same result as applying it once. In mathematical terms, given any elements `u` and `v` in `α` and a finite set `s` of `α`, we have that `UV.compression u v (UV.compression u v s) = UV.compression u v s`.
More concisely: For any type `α` forming a generalized boolean algebra with decidable disjointness, less than or equal to, and equality relations, the `UV.compression` operation is idempotent, i.e., `UV.compression u v (UV.compression u v s) = UV.compression u v s`, for all `u`, `v`, and finite sets `s` in `α`.
|
UV.sup_sdiff_mem_of_mem_compression
theorem UV.sup_sdiff_mem_of_mem_compression :
∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint]
[inst_2 : DecidableRel fun x x_1 => x ≤ x_1] {s : Finset α} {u v a : α} [inst_3 : DecidableEq α],
a ∈ UV.compression u v s → v ≤ a → Disjoint u a → (a ⊔ u) \ v ∈ s
This theorem states that for any type `α`, which is an instance of a GeneralizedBooleanAlgebra, has decidable disjoint relation and decidable less than or equal to (`≤`) relation, given a finite set `s` of type `α`, and elements `u`, `v`, and `a` of type `α` with decidable equality, if `a` belongs to the compression of set `s` with respect to `u` and `v`, and `v` is less than or equal to `a`, and `u` is disjoint from `a`, then the element obtained by taking the supremum (join) of `a` and `u`, and then removing `v`, belongs to the original set `s`. The "compression" mentioned here is a specific operation in the context of GeneralizedBooleanAlgebra.
More concisely: Given a finite set `s` of a GeneralizedBooleanAlgebra type `α` with decidable equality, if `a` is in the compression of `s` with respect to `u` and `v`, `v` ≤ `a`, and `u` is disjoint from `a`, then the supremum of `a` and `u` minus `v` is still in `s`.
|
UV.mem_compression
theorem UV.mem_compression :
∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint]
[inst_2 : DecidableRel fun x x_1 => x ≤ x_1] {s : Finset α} {u v a : α} [inst_3 : DecidableEq α],
a ∈ UV.compression u v s ↔ a ∈ s ∧ UV.compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, UV.compress u v b = a
The theorem `UV.mem_compression` states that for any type `α` with a generalized Boolean algebra structure and decidable relations for disjointness, less than or equal to, and equality, a given element `a` belongs to the UV-compressed family of a finite set `s` if and only if either `a` is in `s` and its UV-compressed version is also in `s`, or `a` is not in `s` but is the UV-compressed version of some element which is in `s`. Here, `u` and `v` are specific elements of `α` used in the UV-compression process.
More concisely: For any type `α` with a generalized Boolean algebra structure and decidable relations for disjointness, less than or equal to, and equality, an element `a` is in the UV-compressed family of a finite set `s` if and only if `a` is in `s` with its UV-compressed version also in `s`, or `a` is not in `s` but the UV-compressed version of some element in `s` equals `a`.
|