mathlib3 documentation

algebra.tropical.lattice

Order on tropical algebraic structure #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

@[protected, instance]
def tropical.has_sup {R : Type u_1} [has_sup R] :
Equations
@[protected, instance]
def tropical.has_inf {R : Type u_1} [has_inf R] :
Equations
@[protected, instance]
def tropical.has_Sup {R : Type u_1} [has_Sup R] :
Equations
@[protected, instance]
def tropical.has_Inf {R : Type u_1} [has_Inf R] :
Equations