toNNReal_lt_toNNReal_iff

Mathlib.Data.NNReal.Defs

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

← MathLib Explorer

English

For real r,p with 0 < p, toNNReal r < toNNReal p iff r < p.

Русский

Для r ∈ ℝ и p > 0: toNNReal r < toNNReal p ⇔ r < p.

LaTeX

$$$$ (h: 0 < p) \\Rightarrow toNNReal r < toNNReal p \\iff r < p. $$$$

Lean4

theorem toNNReal_lt_toNNReal_iff {r p : ℝ} (h : 0 < p) : Real.toNNReal r < Real.toNNReal p ↔ r < p :=
  toNNReal_lt_toNNReal_iff'.trans (and_iff_left h)

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

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

Разделы

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

Аффилиация

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