Why is `PMF.binomial` defined with `p : ℝ≥0∞`?

Stream: mathlib4

[TauTastic]

I was wondering why PMF.binomial is defined like this PMF.binomial (p : ℝ≥0∞) (h : p ≤ 1) (n : ℕ) : PMF (Fin (n + 1)), why is p : ℝ≥0∞ but then with the additional assumption h : p ≤ 1?

Why not just combine the two statements about p to p : [0,1] and just leave out the assumption h : p ≤ 1?

Somewhere I read something similar about the defintion of the square root function in Lean, that it also is defined over the reals but all theorems about the square root need the assumption that the input is not negative.

[Edward van de Meent]

i believe it is related to the fact that concepts involving probability are captured using the concept of a Measure, which is a function which takes values in ℝ≥0∞ (and satisfies certain properties).
As for the second example: that would be related to the fact that there is no "canonical" value for sqrt : ℝ -> ℝ on negative values, and so you probably only use it when you know that the parameter you feed it is nonnegative.