Abstract
We formalise Plünnecke's inequality and the Plünnecke-Ruzsa
inequality, following the notes by Timothy Gowers: "Introduction
to Additive Combinatorics" (2022) for the University of
Cambridge. To this end, we first introduce basic definitions and prove
elementary facts on sumsets and difference sets. Then, we show two
versions of the Ruzsa triangle inequality. We follow with a proof due
to Petridis.