enorm_eq_ofReal

Mathlib.Analysis.Normed.Group.Basic

URI: https://scilib.ai/kg/mathlib#Real.enorm_eq_ofReal

English

If r ≥ 0, then the ENNorm of r equals the ENReal ofReal of r.

Русский

Если r ≥ 0, то enorm r = .ofReal r.

LaTeX

$$$$\|r\|_{e} = \operatorname{ofReal}(r)\quad (r \ge 0).$$$$

Lean4

theorem enorm_eq_ofReal (hr : 0 ≤ r) : ‖r‖ₑ = .ofReal r := by rw [← ofReal_norm_eq_enorm, norm_of_nonneg hr]

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

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

Разделы

Аффилиация

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