[isabelle] UNION_OF / INTERSECTION_OF
John Harrison recently added the following two operators to HOL Light. Should we follow suit?
Added two natural infix constants "UNION_OF" and "INTERSECTION_OF" for the
useful and otherwise longwinded idiom that a set is a suitable (e.g. finite or
countable or pairwise disjoint) union/intersection of "somethings". Typical
examples are topological: `fsigma = COUNTABLE UNION_OF closed` etc.
|- !P Q. P UNION_OF Q =
(\s. ?u. P u /\ (!c. c IN u ==> Q c) /\ UNIONS u = s)
|- !P Q. P INTERSECTION_OF Q =
(\s. ?u. P u /\ (!c. c IN u ==> Q c) /\ INTERS u = s)
This archive was generated by a fusion of
Pipermail (Mailman edition) and