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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• instSupSetTropical = { sSup := fun (s : Set (Tropical R)) => Tropical.trop (sSup (Tropical.untrop '' s)) }

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

Equations

• instInfSetTropical = { sInf := fun (s : Set (Tropical R)) => Tropical.trop (sInf (Tropical.untrop '' s)) }

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

Equations

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

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

Equations

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