Order on tropical algebraic structure

This file defines the orders induced on tropical algebraic structures by the underlying type.

Main declarations

• ConditionallyCompleteLattice (MinTropical R)/ConditionallyCompleteLattice (MaxTropical R)
• ConditionallyCompleteLinearOrder (MinTropical R)/ ConditionallyCompleteLinearOrder (MaxTropical R)

Implementation notes

The order induced is the definitionally equal underlying order, which makes the proofs and constructions quicker to implement.

@[instance_reducible]

instance MinTropical.instSemilatticeInf {R : Type u_1} [SemilatticeInf R] : SemilatticeInf (MinTropical R)

Equations

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

@[instance_reducible]

instance MaxTropical.instSemilatticeSup {R : Type u_1} [SemilatticeSup R] : SemilatticeSup (MaxTropical R)

Equations

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

@[instance_reducible]

instance MinTropical.instSemilatticeSup {R : Type u_1} [SemilatticeSup R] : SemilatticeSup (MinTropical R)

Equations

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

@[instance_reducible]

instance MaxTropical.instSemilatticeInf {R : Type u_1} [SemilatticeInf R] : SemilatticeInf (MaxTropical R)

Equations

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

@[instance_reducible]

instance MinTropical.instLattice {R : Type u_1} [Lattice R] : Lattice (MinTropical R)

Equations

• MinTropical.instLattice = { toSemilatticeSup := MinTropical.instSemilatticeSup, inf := SemilatticeInf.inf, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }

@[instance_reducible]

instance MaxTropical.instLattice {R : Type u_1} [Lattice R] : Lattice (MaxTropical R)

Equations

• MaxTropical.instLattice = Lattice.mkDual SemilatticeSup.sup ⋯ ⋯ ⋯

@[instance_reducible]

instance MinTropical.instSupSet {R : Type u_1} [SupSet R] : SupSet (MinTropical R)

Equations

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

@[instance_reducible]

instance MaxTropical.instInfSet {R : Type u_1} [InfSet R] : InfSet (MaxTropical R)

Equations

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

@[instance_reducible]

instance MinTropical.instInfSet {R : Type u_1} [InfSet R] : InfSet (MinTropical R)

Equations

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

@[instance_reducible]

instance MaxTropical.instSupSet {R : Type u_1} [SupSet R] : SupSet (MaxTropical R)

Equations

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

@[instance_reducible]

instance MinTropical.instConditionallyCompleteLattice {R : Type u_1} [ConditionallyCompleteLattice R] : ConditionallyCompleteLattice (MinTropical R)

Equations

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

@[instance_reducible]

instance MaxTropical.instConditionallyCompleteLattice {R : Type u_1} [ConditionallyCompleteLattice R] : ConditionallyCompleteLattice (MaxTropical R)

Equations

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

@[instance_reducible]

instance MinTropical.instConditionallyCompleteLinearOrder {R : Type u_1} [ConditionallyCompleteLinearOrder R] : ConditionallyCompleteLinearOrder (MinTropical R)

Equations

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