lt_of_toNNReal_lt

Mathlib.Data.NNReal.Defs

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

← MathLib Explorer

English

Let r, p be real numbers. If max(r, 0) < max(p, 0), then r < p.

Русский

Пусть r, p ∈ ℝ. Если max(r, 0) < max(p, 0), то r < p.

LaTeX

$$$$ \max(r,0) < \max(p,0) \implies r < p. $$$$

Lean4

theorem lt_of_toNNReal_lt {r p : ℝ} (h : r.toNNReal < p.toNNReal) : r < p :=
  (Real.toNNReal_lt_toNNReal_iff <| Real.toNNReal_pos.1 (ne_bot_of_gt h).bot_lt).1 h

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

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

Разделы

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

Аффилиация

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