trop_eq_iff_eq_untrop — Mathlib

English

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

Русский

Равенство образов trop эквивалентно равенству исходных элементов: trop x = y тогда и только если x = untrop y.

LaTeX

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

Lean4

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

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