toMulPosReflectLT — Mathlib

English

If α has PosMulReflectLE, then MulPosReflectLT α holds: left multiplication by positive elements interacts with the LT relation in a reflected/contravariant way.

Русский

Пусть α имеет PosMulReflectLE; тогда выполняется MulPosReflectLT: умножение слева на положительный элемент взаимодействует с отношением LT в отражающем виде.

LaTeX

$$$MulPosReflectLT\,\alpha$$$

Lean4

instance (priority := 100) toMulPosReflectLT [MulPosReflectLE α] : MulPosReflectLT α :=
  mulPosReflectLT_iff_contravariant_pos.2
    ⟨fun a b c h =>
      (le_of_mul_le_mul_of_pos_right h.le a.2).lt_of_ne <|
        by
        rintro rfl
        simp at h⟩

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