Documentation

Mathlib.Algebra.Tropical.Lattice

Order on tropical algebraic structure #

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

Main declarations #

Implementation notes #

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

source
🔸 coverage
instance instSemilatticeInfTropical {R : Type u_1} [SemilatticeInf R] :
SemilatticeInf (Tropical R)
Equations
    source
    🔸 coverage
    instance instSemilatticeSupTropical {R : Type u_1} [SemilatticeSup R] :
    SemilatticeSup (Tropical R)
    Equations
      source
      🔸 coverage
      instance instLatticeTropical {R : Type u_1} [Lattice R] :
      Lattice (Tropical R)
      Equations
        source
        🔸 coverage
        instance instSupSetTropical {R : Type u_1} [SupSet R] :
        SupSet (Tropical R)
        Equations
          source
          🔸 coverage
          instance instInfSetTropical {R : Type u_1} [InfSet R] :
          InfSet (Tropical R)
          Equations
            source
            🔸 coverage
            instance instConditionallyCompleteLatticeTropical {R : Type u_1} [ConditionallyCompleteLattice R] :
            ConditionallyCompleteLattice (Tropical R)
            Equations
              source
              🔸 coverage
              instance instConditionallyCompleteLinearOrderTropical {R : Type u_1} [ConditionallyCompleteLinearOrder R] :
              ConditionallyCompleteLinearOrder (Tropical R)
              Equations