Order on tropical algebraic structure #
This file defines the orders induced on tropical algebraic structures by the underlying type.
Main declarations #
ConditionallyCompleteLattice (Tropical R)
ConditionallyCompleteLinearOrder (Tropical R)
Implementation notes #
The order induced is the definitionally equal underlying order, which makes the proofs and constructions quicker to implement.
instance
instConditionallyCompleteLinearOrderTropical
{R : Type u_1}
[ConditionallyCompleteLinearOrder R]
: