mulLeft_bound — Mathlib

English

In a seminormed ring, left multiplication is bounded: ‖x*y‖ ≤ ‖x‖·‖y‖ for all y.

Русский

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

LaTeX

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

Lean4

/-- In a seminormed ring, the left-multiplication `AddMonoidHom` is bounded. -/
theorem mulLeft_bound (x : α) : ∀ y : α, ‖AddMonoidHom.mulLeft x y‖ ≤ ‖x‖ * ‖y‖ :=
  norm_mul_le x

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