toPosSMulMono — Mathlib

English

If α β has a PosSMulStrictMono structure, then it also has a PosSMulMono structure.

Русский

Если имеется структура PosSMulStrictMono на α β, то она также имеет структуру PosSMulMono.

LaTeX

$$$$ PosSMulStrictMono\,\alpha\beta \Rightarrow PosSMulMono\,\alpha\beta $$$$

Lean4

instance (priority := 100) toPosSMulMono [PosSMulStrictMono α β] : PosSMulMono α β :=
  PosSMulMono.of_pos fun _a ha ↦ (strictMono_smul_left_of_pos ha).monotone

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