toPosMulReflectLT — Mathlib

English

If α has PosMulReflectLE, then it has PosMulReflectLT: left multiplication by a positive element reflects strict inequality in a contravariant manner.

Русский

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

LaTeX

$$$PosMulReflectLE\,\alpha \Rightarrow PosMulReflectLT\,\alpha$$$

Lean4

instance (priority := 100) toPosMulReflectLT [PosMulReflectLE α] : PosMulReflectLT α :=
  posMulReflectLT_iff_contravariant_pos.2
    ⟨fun a b c h =>
      (le_of_mul_le_mul_of_pos_left h.le a.2).lt_of_ne <|
        by
        rintro rfl
        simp at h⟩
      -- see Note [lower instance priority]

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