ofReal_norm_eq_enorm'

Mathlib.Analysis.Normed.Group.Basic

URI: https://scilib.ai/kg/mathlib#ofReal_norm_eq_enorm'

English

The image of a real norm under the `ofReal` embedding matches ENNReal equality: ofReal ‖a‖ = ‖a‖ₑ.

Русский

Изображение нормы вещественного числа через вложение ofReal совпадает с ENNorm.

LaTeX

$$$$ \\operatorname{ofReal} \\|a\\| = \\|a\\|_{e} $$$$

Lean4

@[to_additive ofReal_norm_eq_enorm]
theorem ofReal_norm_eq_enorm' (a : E) : .ofReal ‖a‖ = ‖a‖ₑ :=
  ENNReal.ofReal_eq_coe_nnreal _

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

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

Разделы

Аффилиация

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