mulRight_bound — Mathlib

English

Right multiplication is bounded: for all y, ‖y*x‖ ≤ ‖y‖·‖x‖.

Русский

Правая операция умножения ограничена: для всех y выполняется \|y x\| ≤ \|y\|·\|x\|.

LaTeX

$$$\forall y: \alpha,\ \|y x\| \leq \|y\| \|x\|$$$

Lean4

/-- In a seminormed ring, the right-multiplication `AddMonoidHom` is bounded. -/
theorem mulRight_bound (x : α) : ∀ y : α, ‖AddMonoidHom.mulRight x y‖ ≤ ‖x‖ * ‖y‖ := fun y =>
  by
  rw [mul_comm]
  exact norm_mul_le y x

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