tropEquiv — Mathlib

English

There is a canonical equivalence between R and Tropical R given by trop and untrop; tropEquiv is the equivalence map.

Русский

Существует каноническое эквивалентное отображение между R и Tropical R, заданное trop и untrop; tropEquiv — это эквивалентность.

LaTeX

$$$\\mathrm{tropEquiv} : R \\simeq \\mathrm{Tropical}\\,R$$$

Lean4

/-- Reinterpret `x : R` as an element of `Tropical R`.
See `Tropical.tropOrderIso` for the order-preserving equivalence. -/
def tropEquiv : R ≃ Tropical R where
  toFun := trop
  invFun := untrop
  left_inv := untrop_trop
  right_inv := trop_untrop

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