English
Let A,B be finite sets in a group G. If |A B| ≤ K|B|, then there exists a finite F ⊆ A with F ⊆ A and A ⊆ F(B/B) and |F| ≤ K.
Русский
Пусть A,B — конечные множества в группе G. Если |A B| ≤ K|B|, существует конечное F ⊆ A такое, что A ⊆ F(B/B) и |F| ≤ K.
LaTeX
$$$\exists F\subseteq A:\; |F| \le K \land A \subseteq F \cdot (B / B)$$$
Lean4
/-- **Ruzsa's covering lemma** for sets. See also `Finset.ruzsa_covering_mul`. -/
@[to_additive /-- **Ruzsa's covering lemma** for sets. See also `Finset.ruzsa_covering_add`. -/
]
theorem ruzsa_covering_mul (hA : A.Finite) (hB : B.Finite) (hB₀ : B.Nonempty) (hK : Nat.card (A * B) ≤ K * Nat.card B) :
∃ F ⊆ A, Nat.card F ≤ K ∧ A ⊆ F * (B / B) ∧ F.Finite :=
by
lift A to Finset G using hA
lift B to Finset G using hB
classical
obtain ⟨F, hFA, hF, hAF⟩ := Finset.ruzsa_covering_mul hB₀ (by simpa [← Finset.coe_mul] using hK)
exact ⟨F, by norm_cast; simp [*]⟩
