instLatticeTropical — Mathlib

English

If a lattice structure exists on R, then the tropical construction on R carries a lattice structure as well, i.e., Tropical(R) is a lattice when R is a lattice.

Русский

Если на R задана решётка, то на Tropical(R) также существует структура решётки; Tropical(R) образует решётку, когда R имеет решётку.

LaTeX

$$$Lattice\left(\mathrm{Tropical}(R)\right)$$$

Lean4

instance instLatticeTropical [Lattice R] : Lattice (Tropical R) :=
  { instSemilatticeInfTropical, instSemilatticeSupTropical with }

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