instCovariantClassHSMulLeOfIsOrderedSMul

English

The action of G on P is order-preserving in the left argument: if c ≤ d then a • c ≤ a • d for all a ∈ G.

Русский

Действие G на P сохраняет порядок слева: если c ≤ d, то a • c ≤ a • d для всех a ∈ G.

LaTeX

$$∀ a ∈ G, ∀ c,d ∈ P, c ≤ d ⇒ a \cdot c ≤ a \cdot d$$

Lean4

@[to_additive]
instance [LE G] [LE P] [SMul G P] [IsOrderedSMul G P] : CovariantClass G P (· • ·) (· ≤ ·) where
  elim := fun a _ _ bc ↦ IsOrderedSMul.smul_le_smul_left _ _ bc a

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