The Number of Support Constraints for Overlapping Set Optimization with Nested Admissible Sets Is Equal to One

This paper reports on the formalization of a recent result by Crespo, et al., as found in the references. The formalized result bounds the number of support constraints in a particular type of optimization problem. The problem involves discovering an optimal member of a family of sets that overlaps each member of a constraining collection of sets. The particular case addressed here concerns optimizations in which the family of sets is nested. The primary results were formalized in the interactive theorem prover PVS and support the claim that a single support constraint exists in very general circumstances.