Positive Real Type

Stream: mathlib4

[Casavaca]

Should we have Positive Real Type {r : ℝ // r > 0} in Lean, it has some nice properties and some theorems could use it (for example, https://en.wikipedia.org/wiki/Titu's_lemma)

[Damiano Testa]

Currently, you can access is as

import Mathlib

open NNReal

#check ℝ≥0ˣ

[Casavaca]

ℝ≥0ˣ is Unit NNReal, but what is Unit NNReal?

[Damiano Testa]

It should be the invertible elements of the non-negative reals. Effectively, the strictly positive reals, since 0 is the only non-invertible non-negative real.