instance instToStringWithTop_provenance {α : Type u_1} [ToString α] : ToString (WithTop α)

Equations

• instToStringWithTop_provenance = { toString := fun (x : WithTop α) => match x with | none => "⊤" | some x => toString x }

instance instToStringTropical_provenance {α : Type u_1} [ToString α] : ToString (Tropical α)

Equations

• instToStringTropical_provenance = { toString := fun (x : Tropical α) => toString (Tropical.untrop x) }

theorem tropical_order_ge {α : Type u_1} [LinearOrder α] (a b : Tropical α) : Tropical.untrop a ≥ Tropical.untrop b ↔ a + b = b

In the tropicalization of a linear order, a ≥ b if and only if a+b = b.

instance instSemiringWithMonusTropicalOfLinearOrderedAddCommMonoidWithTop {α : Type} [LinearOrderedAddCommMonoidWithTop α] : SemiringWithMonus (Tropical α)

The tropical semiring is an m-semiring. The natural order of the semiring is the reverse of the usual order. The monus a-b is defined as ⊤ if a≥b (for the usual order, not the natural semiring order), and as a otherwise.

Equations

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

instance instSemiringWithMonusTropicalWithTopNat : SemiringWithMonus (Tropical (WithTop ℕ))

The tropical semiring over ℕ ∪ {∞} is a semiring with monus.

Equations

• instSemiringWithMonusTropicalWithTopNat = inferInstance

instance instSemiringWithMonusTropicalWithTopRat : SemiringWithMonus (Tropical (WithTop ℚ))

The tropical semiring over ℚ ∪ {∞} is a semiring with monus.

Equations

• instSemiringWithMonusTropicalWithTopRat = inferInstance

noncomputable instance instSemiringWithMonusTropicalWithTopReal : SemiringWithMonus (Tropical (WithTop ℝ))

The tropical semiring over ℝ ∪ {∞} is a semiring with monus. Note that this contradicts Geerts & Poggi, On database query languages for K-relations, Example 4 which claims this semiring cannot be extended to a semiring with monus: indeed, that paper gives a wrong definition of the monus operator in the tropical semiring.

Equations

• instSemiringWithMonusTropicalWithTopReal = inferInstance

theorem Tropical.absorptive {α : Type} [LinearOrderedAddCommMonoidWithTop α] [CanonicallyOrderedAdd α] : _root_.absorptive (Tropical α)

The tropical semiring is absorptive, as long as the order in the addition monoid corresponds to a canonical order (e.g., as in ℕ) -

theorem TropicalN.absorptive : _root_.absorptive (Tropical (WithTop ℕ))

theorem Tropical.mul_sub_left_distributive {α : Type} [LinearOrder α] [AddCommMonoid α] [IsOrderedAddMonoid α] [AddLeftStrictMono α] : _root_.mul_sub_left_distributive (Tropical (WithTop α))

Times distributes over monus on tropical semirings made of an order strictly compatible with addition, with an additional top element.

theorem TropicalN.mul_sub_left_distributive : _root_.mul_sub_left_distributive (Tropical (WithTop ℕ))

theorem TropicalQ.mul_sub_left_distributive : _root_.mul_sub_left_distributive (Tropical (WithTop ℚ))

theorem TropicalR.mul_sub_left_distributive : _root_.mul_sub_left_distributive (Tropical (WithTop ℝ))

theorem Tropical.idempotent {α : Type} [LinearOrderedAddCommMonoidWithTop α] : _root_.idempotent (Tropical α)

The tropical semiring is idempotent -