injective_untrop — Mathlib

English

The inverse tropicalization map untrop: Tropical R → R is injective; i.e., untrop(x) = untrop(y) implies x = y.

Русский

Обратная карта untrop: Tropical R → R инъективна; то есть untrop(x) = untrop(y) ⇒ x = y.

LaTeX

$$$\\forall x,y \\in Tropical R,\\; \\operatorname{untrop}(x) = \\operatorname{untrop}(y) \\Rightarrow x = y$$$

Lean4

theorem injective_untrop : Function.Injective (untrop : Tropical R → R) :=
  tropEquiv.symm.injective

Похожие утверждения