mulLeft — Mathlib

English

In a linearly ordered monoid, the map x ↦ m·x is an order-embedding: it preserves the order strictly, i.e., x < y implies m·x < m·y.

Русский

В линейно упорядоченном моноиде отображение x ↦ m·x является вложением по порядку: оно строго монотонно уменьшает, то есть x < y → m·x < m·y.

LaTeX

$$$\forall x,y \in \alpha\ (x

Lean4

/-- The order embedding sending `b` to `a * b`, for some fixed `a`.
See also `OrderIso.mulLeft` when working in an ordered group. -/
@[to_additive (attr := simps!) /-- The order embedding sending `b` to `a + b`, for some fixed `a`.
           See also `OrderIso.addLeft` when working in an additive ordered group. -/
    ]
def mulLeft {α : Type*} [Mul α] [LinearOrder α] [MulLeftStrictMono α] (m : α) : α ↪o α :=
  OrderEmbedding.ofStrictMono (fun n => m * n) fun _ _ w => mul_lt_mul_left' w m

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