Order on tropical algebraic structure #

This file defines the orders induced on tropical algebraic structures by the underlying type.

Main declarations #

Implementation notes #

The order induced is the definitionally equal underlying order, which makes the proofs and constructions quicker to implement.

instance instSupTropical {R : Type u_1} [Sup R] :
instance instInfTropical {R : Type u_1} [Inf R] :
instance instSupSetTropical {R : Type u_1} [SupSet R] :
instance instInfSetTropical {R : Type u_1} [InfSet R] :