ViewVC logotype

Log of /metaprl/theories/czf/czf_itt_set_bvd.prla

Parent Directory Parent Directory | Revision Log Revision Log

Links to HEAD: (view) (download) (annotate)
Sticky Revision:

Revision 3568 - (view) (download) (annotate) - [select for diffs]
Modified Tue Apr 9 05:57:54 2002 UTC (19 years, 2 months ago) by xiny
File length: 64927 byte(s)
Diff to previous 3545
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.

Revision 3545 - (view) (download) (annotate) - [select for diffs]
Added Sun Mar 24 07:54:36 2002 UTC (19 years, 3 months ago) by xiny
File length: 60351 byte(s)
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.

  Diffs between and
  Type of Diff should be a

  ViewVC Help
Powered by ViewVC 1.1.26