posSMulMono_iff_posSMulReflectLT — Mathlib

English

PosSMulMono α β is equivalent to PosSMulReflectLT α β: monotonic left scalar multiplication is equivalent to reflecting LT under left multiplication.

Русский

PosSMulMono α β эквивалентно PosSMulReflectLT α β: монотонность левого умножения на скаляре эквивалентна отражению отношения LT при лём умножения слева.

LaTeX

$$$PosSMulMono\\,\\alpha\\,\\beta \\leftrightarrow PosSMulReflectLT\\,\\alpha\\,\\beta$$

Lean4

theorem posSMulMono_iff_posSMulReflectLT : PosSMulMono α β ↔ PosSMulReflectLT α β :=
  ⟨fun _ ↦ PosSMulMono.toPosSMulReflectLT, fun _ ↦ PosSMulReflectLT.toPosSMulMono⟩

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