Theorems · Theorem · combinatorics

Set.ruzsa_covering_mul

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

Ruzsa's covering lemma for sets. See also Finset.ruzsa_covering_mul.

Defined in

Mathlib.Combinatorics.Additive.RuzsaCovering

Cited by

0 results in Mathlib

Foundations

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

Assumes

Group