coe_sub_def

Mathlib.Data.NNReal.Defs

URI: https://scilib.ai/kg/mathlib#NNReal.coe_sub_def

English

For r,p ∈ ℝ≥0, the Real-coercion of r − p equals max(r − p, 0).

Русский

Для r,p ∈ ℝ≥0 сопряжение к Real от r − p равно max(r − p, 0).

LaTeX

$$$\forall r,p \in \mathbb{R}_{\ge 0},\ \uparrow (r - p) = \max(r - p, 0)\,.$$$

Lean4

theorem coe_sub_def {r p : ℝ≥0} : ↑(r - p) = max (r - p : ℝ) 0 :=
  rfl

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

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

Разделы

Аффилиация

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