Parent Directory | Revision Log
Links to HEAD: | (view) (download) (annotate) |
Sticky Revision: |
1. Redefined inverse image. Previously it was defined by introduction and elimination rules; now it can be rewritten with "setbvd_prop". Actually, after "setbvd_prop" is defined, the "inv_image" is somewhat unnecessary. I keep it here just in case that people may want to use the concept of inverse image sometimes. 2. Fixed the error in the previous member elimination rule.
Added the module for the inverse image of set t in set s under function f: { x in s | f(x) in t } I didn't find a direct way to define it, so I define it using axioms.
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 |