Parent Directory | Revision Log
Links to HEAD: | (view) (download) (annotate) |
Sticky Revision: |
Added the definition for setbvd_prop. "set_bvd" and "setbvd_prop" are both methods for building sets. The former builds set { a(x) | x in s } from set s where a(x) is a function; the latter builds set { x in s | p(x) } from all elements x in s satisfying p(x). Both of them are very useful. The former is defined by set induction on s; the latter is defined by member introduction and elimination rules.
Added the definition for "set builder", i.e., the image of a set s under some function f: { f(x) | x in s }. I consider this as a necessity for the set theory. The "set builder" is defined by a "set-induction" rewrite rule. Also added and proved properties for it.
This form allows you to request diffs between any two revisions of this file. For each of the two "sides" of the diff, enter a numeric revision.
ViewVC Help | |
Powered by ViewVC 1.1.26 |