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 instSupTropical {R : Type u_1} [Sup R] : Sup (Tropical R)

instance instInfTropical {R : Type u_1} [Inf R] : Inf (Tropical R)

instance instSemilatticeInfTropical {R : Type u_1} [SemilatticeInf R] : SemilatticeInf (Tropical R)

instance instSemilatticeSupTropical {R : Type u_1} [SemilatticeSup R] : SemilatticeSup (Tropical R)

instance instLatticeTropical {R : Type u_1} [Lattice R] : Lattice (Tropical R)

instance instSupSetTropical {R : Type u_1} [SupSet R] : SupSet (Tropical R)

instance instInfSetTropical {R : Type u_1} [InfSet R] : InfSet (Tropical R)

instance instConditionallyCompleteLatticeTropical {R : Type u_1} [ConditionallyCompleteLattice R] : ConditionallyCompleteLattice (Tropical R)

instance instConditionallyCompleteLinearOrderTropical {R : Type u_1} [ConditionallyCompleteLinearOrder R] : ConditionallyCompleteLinearOrder (Tropical R)