mul_le_of_mul_le_left — Mathlib

English

If left multiplication is monotone, and a·b ≤ c with b ≤ d, then a·d ≤ c.

Русский

Если левая монотонна, и a·b ≤ c при b ≤ d, то a·d ≤ c.

LaTeX

$$$$ \\forall a,b,c,d \\in \\alpha,\; a \\cdot b \\le c \\land d \\le b \\Rightarrow a \\cdot d \\le c $$$$

Lean4

@[to_additive]
theorem mul_le_of_mul_le_left [MulLeftMono α] {a b c d : α} (h : a * b ≤ c) (hle : d ≤ b) : a * d ≤ c :=
  @act_rel_of_rel_of_act_rel _ _ _ (· ≤ ·) _ _ a _ _ _ hle h

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