# 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.

## Equations

- instSupTropical = { sup := fun x y => Tropical.trop (Tropical.untrop x ⊔ Tropical.untrop y) }

## Equations

- instInfTropical = { inf := fun x y => Tropical.trop (Tropical.untrop x ⊓ Tropical.untrop y) }

## Equations

- One or more equations did not get rendered due to their size.

## Equations

- One or more equations did not get rendered due to their size.

instance
instConditionallyCompleteLatticeTropical
{R : Type u_1}
[inst : ConditionallyCompleteLattice R]
:

## Equations

- One or more equations did not get rendered due to their size.

instance
instConditionallyCompleteLinearOrderTropical
{R : Type u_1}
[inst : ConditionallyCompleteLinearOrder R]
:

## Equations

- One or more equations did not get rendered due to their size.