norm_toNNReal'

Mathlib.Analysis.Normed.Group.Basic

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

English

The real norm and its NNReal version are related by toNNReal: ∥a∥.toNNReal = ∥a∥₊.

Русский

real-норма и её NNReal-версия связаны через toNNReal: ∥a∥.toNNReal = ∥a∥₊.

LaTeX

$$$\\|a\\|^{\\mathrm{toNNReal}} = \\|a\\|_+$$$

Lean4

@[to_additive (attr := simp) norm_toNNReal]
theorem norm_toNNReal' : ‖a‖.toNNReal = ‖a‖₊ :=
  @Real.toNNReal_coe ‖a‖₊

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

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

Разделы

Аффилиация

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