Mathlib.Algebra.Tropical.Basic._auxLemma.3
theorem Mathlib.Algebra.Tropical.Basic._auxLemma.3 :
∀ {R : Type u} [inst : LE R] {x y : Tropical R}, (x.untrop ≤ y.untrop) = (x ≤ y)
The theorem `Mathlib.Algebra.Tropical.Basic._auxLemma.3` states that for any type `R` that has an order (`inst : LE R`), and for any `x` and `y` of the tropicalized type `Tropical R`, the inequality `Tropical.untrop x ≤ Tropical.untrop y` is equivalent to the inequality `x ≤ y`. In other words, the process of "untropicalizing" does not change the order of elements.
More concisely: For any type `R` with an order and any `x, y` in the tropicalized type of `R`, `x ≤ y` if and only if `Tropical.untrop x ≤ Tropical.untrop y`.
|
Tropical.add_eq_left
theorem Tropical.add_eq_left : ∀ {R : Type u} [inst : LinearOrder R] ⦃x y : Tropical R⦄, x ≤ y → x + y = x
This theorem states that for any type `R` that has an instance of `LinearOrder` (a type of order that includes less and equal), and for any two elements `x` and `y` of the tropicalization of `R` (`Tropical R`), if `x` is less than or equal to `y`, then the sum of `x` and `y` is equal to `x`. In other words, in the tropicalized version of a type with a linear order, the sum of two elements is equal to the smallest of the two elements.
More concisely: For any type `R` with a linear order and any elements `x, y` in the tropicalization of `R`, if `x ≤ y`, then `x + y = x`.
|
Tropical.untrop_injective
theorem Tropical.untrop_injective : ∀ {R : Type u}, Function.Injective Tropical.untrop
The theorem `Tropical.untrop_injective` states that for any type `R`, the function `untrop`, which reinterprets an element `x` of `Tropical R` as an element of `R`, is injective. In other words, if `untrop` maps two elements of `Tropical R` to the same element of `R`, then those two elements of `Tropical R` were in fact the same. This is equivalent to saying that no two different elements of `Tropical R` are mapped to the same element of `R` by the `untrop` function.
More concisely: The `untrop` function mapping elements of `Tropical R` to `R` is injective.
|
Tropical.untrop_le_iff
theorem Tropical.untrop_le_iff : ∀ {R : Type u} [inst : LE R] {x y : Tropical R}, x.untrop ≤ y.untrop ↔ x ≤ y := by
sorry
The theorem `Tropical.untrop_le_iff` states that for any type `R` equipped with a less than or equal to relation (denoted `LE R`), and for any two elements `x` and `y` of the type `Tropical R`, the inequality of their underlying elements in `R` (obtained by `Tropical.untrop` method) is equivalent to the inequality of `x` and `y` in the tropicalized type `Tropical R`. In other words, the inequality holds in `Tropical R` if and only if it holds in `R` after applying the `untrop` function to `x` and `y`.
More concisely: For any type `R` with a total order and tropical semiring structure `Tropical R`, the inequality `x LE y` in `Tropical R` holds if and only if `Tropical.untrop x LE Tropical.untrop y` holds in `R`.
|
Tropical.trop_eq_iff_eq_untrop
theorem Tropical.trop_eq_iff_eq_untrop : ∀ {R : Type u} {x : R} {y : Tropical R}, Tropical.trop x = y ↔ x = y.untrop
The theorem `Tropical.trop_eq_iff_eq_untrop` states that for any type `R` and any elements `x` of `R` and `y` of `Tropical R`, `x` being interpreted as an element of `Tropical R` is equal to `y` if and only if `x` is equal to `y` being interpreted back as an element of `R`. In other words, it establishes an equivalence between the equality of `x` and `y` in their respective spaces and the equality of their tropicalizations.
More concisely: The theorem `Tropical.trop_eq_iff_eq_untrop` in Lean 4 states that the tropicalization of two elements in `Tropical R` is equal if and only if the original elements in `R` are equal.
|
Tropical.untrop_monotone
theorem Tropical.untrop_monotone : ∀ {R : Type u} [inst : Preorder R], Monotone Tropical.untrop
The theorem `Tropical.untrop_monotone` states that for any type `R` with a preorder (a structure where we can meaningfully say that one element is less than or equal to another), the function `Tropical.untrop` is monotone. In other words, if we have two elements `a` and `b` in the tropical semiring such that `a` is less than or equal to `b`, then the corresponding elements in `R` obtained by applying `untrop` also satisfy this order relation, i.e., `untrop a` is less than or equal to `untrop b`.
More concisely: For any preorder type `R`, the function `Tropical.untrop` from the tropical semiring to `R` is a monotone function, that is, if `a` is less than or equal to `b` in the tropical semiring, then `untrop a` is less than or equal to `untrop b` in `R`.
|
Tropical.trop_add_def
theorem Tropical.trop_add_def :
∀ {R : Type u} [inst : LinearOrder R] (x y : Tropical R), x + y = Tropical.trop (min x.untrop y.untrop)
The theorem `Tropical.trop_add_def` states that for any type `R` equipped with a linear order and any two elements `x` and `y` of the tropicalization of `R` (denoted `Tropical R`), the sum `x + y` is equal to the tropicalization of the minimum (in the sense of the given linear order) of the elements of type `R` corresponding to `x` and `y`. In other words, in the tropical addition operation, `x + y` is defined to be the element of `Tropical R` that corresponds to the smaller (or minimum) of the two elements `x` and `y` when they are considered as elements of the original type `R`.
More concisely: For any type `R` with a linear order and for any `x, y` in the tropicalization of `R`, the tropical addition `x + y` is the tropicalization of the minimum element in `R` of `{x, y}`.
|