Casting NNReal to Set Real?

Stream: general

[Jack McCarthy]

Sorry if this is a bit of noobie question, but how can I get Lean to interpret NNReal as a Set Real? Specifically, I'm trying to get code like this to compile:

import Mathlib.Probability.Moments.Basic

example sq_convex : ConvexOn ℝ NNReal (fun (x : ℝ) ↦ x^2) := sorry

[Aaron Liu]

You want Set.Ici 0

[Aaron Liu]

that's the closed-infinite Interval with endpoint 0

[Aaron Liu]

actually probably you will need to write Set.Ici (0 : ℝ) since by default you will get the natural number zero

[Jack McCarthy]

Thanks I will try this!

[Kevin Buzzard]

Note that NNReal is a type but Ici 0 is a term.

[Yury G. Kudryashov]

Another option is to use ConvexOn NNReal Set.univ (fun x : NNReal => x ^ 2).