enorm_div_le

Mathlib.Analysis.Normed.Group.Basic

URI: https://scilib.ai/kg/mathlib#enorm_div_le

English

In the ENNReal setting, the EN-norm of a/b is bounded by the sum of EN-norms: enorm(a/b) ≤ enorm(a) + enorm(b).

Русский

В окружении ENNReal имеет место ограничение enorm(a/b) ≤ enorm(a) + enorm(b).

LaTeX

$$$$ \\|a / b\\|_{e} \\leq \\|a\\|_{e} + \\|b\\|_{e} $$$$

Lean4

@[to_additive]
theorem enorm_div_le : ‖a / b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ := by simpa [enorm, ← ENNReal.coe_add] using nnnorm_div_le a b

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru