instPosSMulReflectLE — Mathlib

English

If α is ordered with scalar reflection of ≤, then finsupp inherits this via lifting.

Русский

Если существует отображение отражения ≤ для скаляра, то для Finsupp это свойство сохраняется через линейное поднятие.

LaTeX

$$PosSMulReflectLE α (ι →₀ β)$$

Lean4

instance instPosSMulReflectLE [PosSMulReflectLE α β] : PosSMulReflectLE α (ι →₀ β) :=
  PosSMulReflectLE.lift _ coe_le_coe coe_smul

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