mulLECancellable_val — Mathlib

English

Let M be a monoid with a compatible order and MulLeftMono. Then for any unit u ∈ Mˣ, left multiplication by u preserves order: for all a,b ∈ M, a ≤ b implies (↑u) a ≤ (↑u) b.

Русский

Пусть M — моноид с совместимым порядком и свойством монотонности слева. Тогда для любого единичного элемента u ∈ Mˣ умножение слева на u сохраняет порядок: для всех a,b ∈ M, a ≤ b ⇒ u a ≤ u b.

LaTeX

$$$\forall a,b \in M, \ a \le b \Rightarrow (↑u)\,a \le (↑u)\,b$$$

Lean4

theorem mulLECancellable_val : MulLECancellable (↑u : M) := fun _ _ h ↦ by simpa using mul_le_mul_left' h ↑u⁻¹

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