untrop_eq_iff_eq_trop

Mathlib.Algebra.Tropical.Basic

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

English

Equality of untrop images corresponds to equality of trop preimages: untrop x = y iff x = trop y.

Русский

Равенство untrop(x) и y эквивалентно равенству x и trop(y).

LaTeX

$$$\\mathrm{untrop\\_eq\\_iff\\_eq\\_trop} : (\\forall x,y, \\mathrm{untrop}(x) = y \\iff x = \\mathrm{trop}(y))$$$

Lean4

theorem untrop_eq_iff_eq_trop {x} {y : R} : untrop x = y ↔ x = trop y :=
  tropEquiv.symm.apply_eq_iff_eq_symm_apply

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

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

Разделы

Аффилиация

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