surjective_trop — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem surjective_trop : Function.Surjective (trop : R → Tropical R) :=
  tropEquiv.surjective

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