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, Real.toNNReal r < Real.toNNReal p iff r < p and 0 < p.

Русский

Для действительных r, p: Real.toNNReal r < Real.toNNReal p ⇔ r < p и 0 < p.

LaTeX

$$$$ Real.toNNReal r < Real.toNNReal p \\iff r < p \\land 0 < p. $$$$

Lean4

@[simp]
theorem toNNReal_lt_toNNReal_iff' {r p : ℝ} : Real.toNNReal r < Real.toNNReal p ↔ r < p ∧ 0 < p :=
  NNReal.coe_lt_coe.symm.trans max_lt_max_left_iff

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

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

Разделы

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

Аффилиация

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