to_contravariantClass_pos_mul_lt — Mathlib

English

If α has PosMulReflectLT, then left-multiplication by a positive element is strictly order-preserving: for b < c and a > 0, a·b < a·c.

Русский

Если α обладает PosMulReflectLT, то при a > 0 левая умножение сохраняет строгий порядок: b < c ⇒ a·b < a·c.

LaTeX

$$$\forall a,b,c \in \alpha,\ a > 0 \land b < c \Rightarrow a\cdot b < a\cdot c$$$

Lean4

instance to_contravariantClass_pos_mul_lt [PosMulReflectLT α] : ContravariantClass α>0 α (fun x y => x * y) (· < ·) :=
  ⟨fun a _ _ bc => @ContravariantClass.elim α≥0 α (fun x y => x * y) (· < ·) _ ⟨_, a.2.le⟩ _ _ bc⟩

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