How to define a set of functions satisfying some conditions

Stream: maths

[mty]

I'm learning LEAN and trying to formalize a paper. In one step, a set of all distributions with finite support is defined. I tried

variable {a : Type* }
variable (X : Set a)
open unitInterval
open BigOperators
def Y := {y: X  -> I | {x|y x ≠ 0}.Finite ∧ Σ^f x, y x =1 }

But I got the error AddCommMonoid ↑I. I'm wondering why. Does anyone know how to define the set correctly without more mathlib build-in functions?

[Kevin Buzzard]

The issue is that if I is the unit interval then there's no addition defined globally on it (because the sum of two things in the unit interval might not be in the unit interval). Perhaps the easiest way to fix it is just to consider functions taking values in the nonnegative reals, because if the sum is 1 then all of the values are guaranteed to be <= 1.

[mty]

Thank you Kevin! It works.