smul_le_smul — Mathlib

English

The action of a group G on a set P by a heterogeneous scalar product is covariant with respect to the order: a • c ≤ a • d whenever c ≤ d.

Русский

Действие группы G на множество P по неоднородному скаляру ковариантно по порядку: если c ≤ d, то a • c ≤ a • d.

LaTeX

$$∀ a ∈ G, ∀ c,d ∈ P, c ≤ d ⇒ a • c ≤ a • d$$

Lean4

@[to_additive]
theorem smul_le_smul [LE G] [Preorder P] [SMul G P] [IsOrderedSMul G P] {a b : G} {c d : P} (hab : a ≤ b)
    (hcd : c ≤ d) : a • c ≤ b • d :=
  (IsOrderedSMul.smul_le_smul_left _ _ hcd _).trans (IsOrderedSMul.smul_le_smul_right _ _ hab _)

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