Email Gateway (Aug 22 2022 at 16:52): Email Gateway (Aug 22 2022 at 16:52):From: Lawrence Paulson <lp15@cam.ac.uk>
John Harrison recently added the following two operators to HOL Light. Should we follow suit?
Larry
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.
UNION_OF =
|- !P Q. P UNION_OF Q =
(\s. ?u. P u /\ (!c. c IN u ==> Q c) /\ UNIONS u = s)
INTERSECTION_OF =
|- !P Q. P INTERSECTION_OF Q =
(\s. ?u. P u /\ (!c. c IN u ==> Q c) /\ INTERS u = s)
Last updated: Apr 19 2024 at 16:20 UTC