toMulPosStrictMono — Mathlib

English

Left multiplication by a positive element is strictly increasing: if b < c then a b < a c (for a > 0).

Русский

Левое умножение на положительный элемент строго возрастает: если b < c, то a b < a c (при a > 0).

LaTeX

$$$\\\\forall a,b,c \\\\in \\\\alpha, \\\\ 0 < a \\\\Rightarrow (b < c \\\\Rightarrow a b < a c)$$$

Lean4

instance (priority := 100) toMulPosStrictMono : MulPosStrictMono α where
  elim a b c hbc := by dsimp only; by_contra! h; exact hbc.not_ge <| (mul_le_mul_iff_left₀ a.2).1 h

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