mulRightReflectLE — Mathlib

English

If α has right-reflecting left order, the dual αᵒᵈ inherits a corresponding right-reflecting property.

Русский

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

LaTeX

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

Lean4

@[to_additive]
instance mulRightReflectLE [LE α] [Mul α] [c : MulRightReflectLE α] : MulRightReflectLE αᵒᵈ :=
  ⟨c.1.flip⟩

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