toNNRat_add

Mathlib.Data.NNRat.Defs

URI: https://scilib.ai/kg/mathlib#Rat.toNNRat_add

← MathLib Explorer

English

For p,q ∈ ℚ≥0 with p,q ≥ 0, toNNRat(q+p) = toNNRat q + toNNRat p.

Русский

Для p,q ∈ ℚ≥0 выполняется toNNRat(q+p) = toNNRat q + toNNRat p.

LaTeX

$$$\operatorname{toNNRat}(q+p) = \operatorname{toNNRat}(q) + \operatorname{toNNRat}(p)\quad( p,q \ge 0 ).$$$

Lean4

@[simp]
theorem toNNRat_add (hq : 0 ≤ q) (hp : 0 ≤ p) : toNNRat (q + p) = toNNRat q + toNNRat p :=
  NNRat.ext <| by simp [toNNRat, hq, hp, add_nonneg]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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