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.

ink

instance instSupTropical {R : Type u_1} [inst : Sup R] : Sup (Tropical R)

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

• instSupSetTropical = { supₛ := fun s => Tropical.trop (supₛ (Tropical.untrop '' s)) }

ink

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

Equations

• instInfSetTropical = { infₛ := fun s => Tropical.trop (infₛ (Tropical.untrop '' s)) }

ink

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

Equations

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

ink

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

Equations

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