surjective_untrop — Mathlib

English

The inverse tropicalization map untrop: Tropical R → R is surjective; every element of R is untrop of some Tropical element.

Русский

Обратная карта untrop: Tropical R → R сюръективна; каждый элемент R равен untrop некоторого элемента Tropical.

LaTeX

$$$\\forall r \\in R,\\; \\exists t \\in Tropical R,\\; \\operatorname{untrop}(t) = r$$$

Lean4

theorem surjective_untrop : Function.Surjective (untrop : Tropical R → R) :=
  tropEquiv.symm.surjective

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