trop_injective

Mathlib.Algebra.Tropical.Basic

URI: https://scilib.ai/kg/mathlib#Tropical.trop_injective

English

Another articulation of the injectivity of trop: trop x = trop y implies x = y.

Русский

Еще одно выражение инъективности trop: trop x = trop y тогда и только если x = y.

LaTeX

$$$\\text{trop}\\;\\text{injective} \\Rightarrow (\\forall x,y,\\mathrm{trop}(x)=\\mathrm{trop}(y) \\Rightarrow x=y)$$$

Lean4

theorem trop_injective : Function.Injective (trop : R → Tropical R) := fun _ _ => id

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru