← Mathematical handbook

Compactness of the localized upper seeds and their convex hull

theorem Papers.AnsariRockel2026RhoFootrule.upper_seeds_compact : IsCompact upperSeeds

The countably many parameterized branches have just the included limit (1,1).

theorem Papers.AnsariRockel2026RhoFootrule.upper_convex_hull_compact : IsCompact ((convexHull ℝ) upperSeeds)

Finite-dimensional compactness makes the upper convexified maximum attainable.