enorm_mul_le' — Mathlib

English

In any ESeminormedMonoid, the EN-norm is subadditive with respect to multiplication: ‖a*b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ.

Русский

В любой ESeminormedMonoid норма EN под аддитивностью по умножению: ‖a*b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ.

LaTeX

$$$\\|a \\cdot b\\|_\\varepsilon \\leq \\|a\\|_\\varepsilon + \\|b\\|_\\varepsilon$$$

Lean4

@[to_additive enorm_add_le]
theorem enorm_mul_le' (a b : E) : ‖a * b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ :=
  ESeminormedMonoid.enorm_mul_le a b

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