instPreorderTropical — Mathlib

English

The tropical construction carries a preorder structure on Tropical R, extending the preorder on R.

Русский

Тропическая конструкция на Tropical R задаёт относительный порядок, совместимый с порядком на R.

LaTeX

$$$\\operatorname{Preorder}(\\operatorname{Tropical}(R))$$$

Lean4

instance instPreorderTropical [Preorder R] : Preorder (Tropical R) :=
  { instLETropical, instLTTropical with
    le_refl := fun x => le_refl (untrop x)
    le_trans := fun _ _ _ h h' => le_trans (α := R) h h'
    lt_iff_le_not_ge := fun _ _ => lt_iff_le_not_ge (α := R) }

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