theorem affine_image_and_preimage_convex {E : Type u} {F : Type v} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (T : E →ᵃ[ℝ] F) (C : Set E) (D : Set F) (hC : Convex ℝ C) (hD : Convex ℝ D) : Convex ℝ (⇑T '' C) ∧ Convex ℝ (⇑T ⁻¹' D)

Proposition 3.5: the image of a convex set under an affine map is convex, and the preimage of a convex set under an affine map is convex.