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 R) => Tropical.trop (Tropical.untrop x ⊔ Tropical.untrop y) }
Equations
- instInfTropical = { inf := fun (x y : Tropical R) => Tropical.trop (Tropical.untrop x ⊓ Tropical.untrop y) }
Equations
- instSemilatticeInfTropical = SemilatticeInf.mk ⋯ ⋯ ⋯
Equations
- instSemilatticeSupTropical = SemilatticeSup.mk ⋯ ⋯ ⋯
Equations
- instLatticeTropical = Lattice.mk ⋯ ⋯ ⋯
Equations
- instConditionallyCompleteLatticeTropical = ConditionallyCompleteLattice.mk ⋯ ⋯ ⋯ ⋯
instance
instConditionallyCompleteLinearOrderTropical
{R : Type u_1}
[ConditionallyCompleteLinearOrder R]
:
Equations
- instConditionallyCompleteLinearOrderTropical = ConditionallyCompleteLinearOrder.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯