NNReal

Mathlib.Data.NNReal.Defs

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

Lean4

/-- Nonnegative real numbers, denoted as `ℝ≥0` within the NNReal namespace -/
def NNReal :=
  { r : ℝ // 0 ≤ r }
deriving Zero, One, Semiring, CommMonoidWithZero, CommSemiring, PartialOrder, SemilatticeInf, SemilatticeSup,
  DistribLattice, Nontrivial, Inhabited

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

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

Разделы

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

Аффилиация

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