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.

instance instSupTropical {R : Type u_1} [Sup R] :
Equations
instance instInfTropical {R : Type u_1} [Inf R] :
Equations
Equations
Equations
instance instLatticeTropical {R : Type u_1} [Lattice R] :
Equations
instance instSupSetTropical {R : Type u_1} [SupSet R] :
Equations
instance instInfSetTropical {R : Type u_1} [InfSet R] :
Equations
Equations
Equations