Theorems · Theorem · combinatorics

Finset.ruzsa_covering_mul

∀ {G : Type u_1} [inst : Group G] {K : ℝ} [inst_1 : DecidableEq G] {A B : Finset G},
  B.Nonempty → ↑(A * B).card ≤ K * ↑B.card → ∃ F ⊆ A, ↑F.card ≤ K ∧ A ⊆ F * (B / B)

Ruzsa's covering lemma.

Defined in

Mathlib.Combinatorics.Additive.RuzsaCovering

Cited by

2 results in Mathlib

Foundations

Depth 106 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupDecidableEq