Injective affine embeddings preserve vertex-edge diameter
ProvedHirsch.injective_affine_image_diameter_iffformalizationgraph-diameterpolyhedra
Let E and F be real vector spaces, let f:E→F be an injective affine map, let P be any subset of E, and let B be a natural number. The vertex-edge graph of f(P) has padded diameter at most B if and only if the vertex-edge graph of P does. Adjacency means that the distinct endpoints span an extreme segment in the set. No surjectivity onto F, equal ambient dimensions, convexity, boundedness, nonemptiness, or positive B is assumed.
Preamble
import Mathlib import Definitions.Def_Hirsch_model open Set
Formal statement
namespace Hirsch
theorem injective_affine_image_diameter_iff
{E F : Type} [AddCommGroup E] [Module ℝ E]
[AddCommGroup F] [Module ℝ F]
(f : E →ᵃ[ℝ] F) (hf : Function.Injective f)
(P : Set E) (B : ℕ) :
Hirsch.DiamLE (f '' P) B ↔ Hirsch.DiamLE P B := by sorry
end HirschSource