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]
Equations
- tropical.has_sup = {sup := λ (x y : tropical R), tropical.trop (tropical.untrop x ⊔ tropical.untrop y)}
@[protected, instance]
Equations
- tropical.has_inf = {inf := λ (x y : tropical R), tropical.trop (tropical.untrop x ⊓ tropical.untrop y)}
@[protected, instance]
Equations
- tropical.semilattice_inf = {inf := has_inf.inf tropical.has_inf, le := partial_order.le tropical.partial_order, lt := partial_order.lt tropical.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}
@[protected, instance]
Equations
- tropical.semilattice_sup = {sup := has_sup.sup tropical.has_sup, le := partial_order.le tropical.partial_order, lt := partial_order.lt tropical.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}
@[protected, instance]
Equations
- tropical.lattice = {sup := semilattice_sup.sup tropical.semilattice_sup, le := semilattice_inf.le tropical.semilattice_inf, lt := semilattice_inf.lt tropical.semilattice_inf, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf tropical.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}
@[protected, instance]
Equations
- tropical.has_Sup = {Sup := λ (s : set (tropical R)), tropical.trop (has_Sup.Sup (tropical.untrop '' s))}
@[protected, instance]
Equations
- tropical.has_Inf = {Inf := λ (s : set (tropical R)), tropical.trop (has_Inf.Inf (tropical.untrop '' s))}
@[protected, instance]
Equations
- tropical.conditionally_complete_lattice = {sup := lattice.sup tropical.lattice, le := lattice.le tropical.lattice, lt := lattice.lt tropical.lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf tropical.lattice, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := has_Sup.Sup tropical.has_Sup, Inf := has_Inf.Inf tropical.has_Inf, le_cSup := _, cSup_le := _, cInf_le := _, le_cInf := _}
@[protected, instance]
def
tropical.conditionally_complete_linear_order
{R : Type u_1}
[conditionally_complete_linear_order R] :
Equations
- tropical.conditionally_complete_linear_order = {sup := conditionally_complete_lattice.sup tropical.conditionally_complete_lattice, le := conditionally_complete_lattice.le tropical.conditionally_complete_lattice, lt := conditionally_complete_lattice.lt tropical.conditionally_complete_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := conditionally_complete_lattice.inf tropical.conditionally_complete_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := conditionally_complete_lattice.Sup tropical.conditionally_complete_lattice, Inf := conditionally_complete_lattice.Inf tropical.conditionally_complete_lattice, le_cSup := _, cSup_le := _, cInf_le := _, le_cInf := _, le_total := _, decidable_le := linear_order.decidable_le tropical.linear_order, decidable_eq := linear_order.decidable_eq tropical.linear_order, decidable_lt := linear_order.decidable_lt tropical.linear_order, max_def := _, min_def := _}