# Ruzsa's covering lemma #

This file proves the Ruzsa covering lemma. This says that, for s, t finsets, we can cover s with at most (s + t).card / t.card copies of t - t.

## TODO #

Merge this file with other prerequisites to Freiman's theorem once we have them.

theorem Finset.exists_subset_add_sub {α : Type u_1} [] [] (s : ) {t : } (ht : t.Nonempty) :
∃ (u : ), u.card * t.card (s + t).card s u + t - t

Ruzsa's covering lemma

theorem Finset.exists_subset_mul_div {α : Type u_1} [] [] (s : ) {t : } (ht : t.Nonempty) :
∃ (u : ), u.card * t.card (s * t).card s u * t / t

Ruzsa's covering lemma.

theorem Set.exists_subset_add_sub {α : Type u_1} [] {s : Set α} {t : Set α} (hs : s.Finite) (ht' : t.Finite) (ht : t.Nonempty) :
∃ (u : Set α), Nat.card u * Nat.card t Nat.card (s + t) s u + t - t u.Finite

Ruzsa's covering lemma. Version for sets. For finsets, see Finset.exists_subset_add_sub.

theorem Set.exists_subset_mul_div {α : Type u_1} [] {s : Set α} {t : Set α} (hs : s.Finite) (ht' : t.Finite) (ht : t.Nonempty) :
∃ (u : Set α), Nat.card u * Nat.card t Nat.card (s * t) s u * t / t u.Finite

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