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

• instSemilatticeInfTropical = SemilatticeInf.mk (fun (x y : Tropical R) => Tropical.trop (Tropical.untrop x ⊓ Tropical.untrop y)) ⋯ ⋯ ⋯

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

Equations

• instSemilatticeSupTropical = SemilatticeSup.mk (fun (x y : Tropical R) => Tropical.trop (Tropical.untrop x ⊔ Tropical.untrop y)) ⋯ ⋯ ⋯

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

Equations

• instLatticeTropical = Lattice.mk SemilatticeInf.inf ⋯ ⋯ ⋯

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

• instConditionallyCompleteLatticeTropical = ConditionallyCompleteLattice.mk ⋯ ⋯ ⋯ ⋯

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

Equations

• instConditionallyCompleteLinearOrderTropical = ConditionallyCompleteLinearOrder.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯