mulLeftReflectLT — Mathlib

English

If α has left-reflecting less-than with multiplication, the dual αᵒᵈ inherits the corresponding left-reflecting less-than property.

Русский

Если в α имеется слева отражение порядка для < с умножением, то в двойственном αᵒᵈ сохраняется соответствующее свойство для < слева.

LaTeX

$$MulLeftReflectLT(α) ⇒ MulLeftReflectLT(α^{op})$$

Lean4

@[to_additive]
instance mulLeftReflectLT [LT α] [Mul α] [c : MulLeftReflectLT α] : MulLeftReflectLT αᵒᵈ :=
  ⟨c.1.flip⟩

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