Finset.exists_subset_add_sub
theorem Finset.exists_subset_add_sub :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : AddCommGroup α] (s : Finset α) {t : Finset α},
t.Nonempty → ∃ u, u.card * t.card ≤ (s + t).card ∧ s ⊆ u + t - t
**Ruzsa's Covering Lemma** states that for any type `α` where `α` has decidable equality and is an additive commutative group, given a finite set `s` and a non-empty finite set `t`, there exists a finite set `u` such that the product of the cardinality of `u` and `t` is less than or equal to the cardinality of the set formed by adding `s` and `t`. Moreover, `s` is a subset of the set obtained by adding `u` and `t` and then subtracting `t`.
More concisely: For any finite, additive commutative group `α` with decidable equality, there exists a finite set `u` such that the product of `#u` and `#t` is less than or equal to `#(s + t)` and `s ⊆ u + t - t`, where `#` denotes cardinality and `+` denotes set union.
|
Set.exists_subset_add_sub
theorem Set.exists_subset_add_sub :
∀ {α : Type u_1} [inst : AddCommGroup α] {s t : Set α},
s.Finite →
t.Finite → t.Nonempty → ∃ u, Nat.card ↑u * Nat.card ↑t ≤ Nat.card ↑(s + t) ∧ s ⊆ u + t - t ∧ u.Finite
**Ruzsa's Covering Lemma for Sets**: For all types 'α' endowed with a commutative additive group structure, and for all sets 's' and 't' of this type, if 's' and 't' are finite sets and 't' is nonempty, then there exists a set 'u' such that the product of the cardinalities of 'u' and 't' is less than or equal to the cardinality of the sumset of 's' and 't', and 's' is a subset of the sumset of 'u' and 't' (with 't' subtracted from each element). Furthermore, the set 'u' is finite. The sumset of two sets 'A' and 'B' is the set of all possible sums of an element from 'A' and an element from 'B'. Similarly, the subtraction of a set 'B' from a sumset 'A + B' means subtracting an element of 'B' from each element in 'A + B'.
More concisely: Given a commutative additive group type 'α' and finite, nonempty sets 's' and 't' of this type, there exists a finite set 'u' such that the product of the cardinalities of 'u' and 't' is less than or equal to the cardinality of 's + t' and 's' is a subset of 'u + t - t'.
|
Set.exists_subset_mul_div
theorem Set.exists_subset_mul_div :
∀ {α : Type u_1} [inst : CommGroup α] {s t : Set α},
s.Finite →
t.Finite → t.Nonempty → ∃ u, Nat.card ↑u * Nat.card ↑t ≤ Nat.card ↑(s * t) ∧ s ⊆ u * t / t ∧ u.Finite
**Ruzsa's Covering Lemma** for sets states that for any type `α` that forms a commutative group, and any two finite sets `s` and `t` of this type, where `t` is nonempty, there exists another set `u` such that the natural number cardinality (or size) of `u` times the cardinality of `t` is less than or equal to the cardinality of the set formed by multiplying `s` and `t`. Furthermore, `s` is a subset of the set formed by multiplying `u` and `t` and then dividing, and `u` is also finite. The multiplication and division here are set operations, corresponding to all possible pairwise products and quotients.
More concisely: For any commutative group type `α` and finite nonempty sets `s` and `t` of `α`, there exists a finite set `u` such that `|u||t| <= |s × t|` and `s ⊆ u × t /{ (x, y) | y = 0 }`, where `|.|` denotes cardinality and `×` is the Cartesian product.
|
Finset.exists_subset_mul_div
theorem Finset.exists_subset_mul_div :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : CommGroup α] (s : Finset α) {t : Finset α},
t.Nonempty → ∃ u, u.card * t.card ≤ (s * t).card ∧ s ⊆ u * t / t
The theorem named "Ruzsa's covering lemma" defines that for any type `α` with decidable equality and commutative group structure, given a finite set `s` of `α` and a nonempty finite set `t` of `α`, there always exists another finite set `u` of `α` such that the size of `u` times the size of `t` is less than or equal to the size of the set obtained by multiplying `s` and `t`, and `s` is a subset of the set obtained by dividing the set obtained by multiplying `u` and `t` by `t`.
More concisely: For any commutative group `α` with decidable equality, given finite sets `s` and `t`, there exists a finite set `u` such that the product of their sizes satisfies `#u * #t <= #(s * t)` and `s` is a subset of `(u * t) / t`.
|