nnnorm_nnratCast

Mathlib.Analysis.RCLike.Basic

URI: https://scilib.ai/kg/mathlib#RCLike.nnnorm_nnratCast

English

For any q ∈ ℚ≥0, the nnnorm of (q:K) equals q.

Русский

Для любого q ∈ ℚ≥0 nnnorm от (q:K) равен q.

LaTeX

$$$$\| (q : K) \|_{NN} = q.$$$$

Lean4

@[simp, rclike_simps, norm_cast]
theorem nnnorm_nnratCast (q : ℚ≥0) : ‖(q : K)‖₊ = q := by simp [nnnorm]

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

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

Разделы

Аффилиация

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