mulRightMono — Mathlib

English

If y ≤ z in Tropical R, then for any x, y*x ≤ z*x; i.e., right multiplication is monotone.

Русский

Если y ≤ z в Tropical R, то для любого x выполняется y·x ≤ z·x; то есть правое умножение монотонно.

LaTeX

$$$\forall x,y,z \in \mathrm{Tropical}(R),\ y \le z \Rightarrow y\,x \le z\,x$$$

Lean4

instance mulRightMono [LE R] [Add R] [AddRightMono R] : MulRightMono (Tropical R) :=
  ⟨fun _ y z h => add_le_add_right (show untrop y ≤ untrop z from h) _⟩

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