Tropicalization of facets of polytopes

It is known that any tropical polytope is the image of ordinary polytopes over the Puiseux series field under the degree map. The latter polytopes are called lifts of the tropical polytope. We prove that any pure tropical polytope is the intersection of the tropical half-spaces given by the images under the degree map of the facet-defining half-spaces of a certain lift, which we construct explicitly taking into account geometric properties of the given polytope. Moreover, when the generators of the tropical polytope are in general position, we prove that the above property is satisfied for any lift. These results were conjectured by Develin and Yu.