mul_le_mul_iff_left — Mathlib

English

Let a be such that left multiplication by a is order-preserving and strictly monotone, i.e., a · b ≤ a · c iff b ≤ c. This holds under the given cancellability and monotonicity assumptions.

Русский

Пусть a таков, что левое умножение на a сохраняет порядок и строго монотонно: a · b ≤ a · c тогда и только тогда b ≤ c. Это выполняется при данных предпосылках о ковалянности и монотонности.

LaTeX

$$MulLECancellable a → (a · b ≤ a · c ↔ b ≤ c)$$

Lean4

@[to_additive]
protected theorem mul_le_mul_iff_left [Mul α] [MulLeftMono α] {a b c : α} (ha : MulLECancellable a) :
    a * b ≤ a * c ↔ b ≤ c :=
  ⟨fun h => ha h, fun h => mul_le_mul_left' h a⟩

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