[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

union variable binding operator

I'm pretty sure that PVS has a variable binding operator for unions (or
a function from set&function pairs to sets), like there is for summing:

	sum(S: set, f:[S -> int])

but I can't find it... Isn't there such a thing?

I.e. an operator 'union' so that where R is some set of sets

				       |   |
	union(S: set, f: [S -> set]) = |   | f(x)
				  forall x in S


Thanks, sorry if I'm missing something obvious...

Mark Aronszajn