nnnorm_natCast

Mathlib.Analysis.Normed.Group.Basic

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

English

The nonnegative norm of n (as a real) equals n: ‖(n:ℝ)‖₊ = n.

Русский

Положительная норма n, взятая как действительное, равна n: ‖(n:ℝ)‖₊ = n.

LaTeX

$$$\\|n\\|_+ = n$$$

Lean4

@[simp 1100]
theorem nnnorm_natCast (n : ℕ) : ‖(n : ℝ)‖₊ = n :=
  NNReal.eq <| norm_natCast _

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

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

Разделы

Аффилиация

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