Re: [mizar] How to properly do inductive sets in Mizar?

[Freek Wiedijk <freek@cs.kun.nl>]

Hi,

One additional remark about this:

>you can use the "Knaster" scheme

The scheme that I proved using "Knaster" was (of course this
is only part of the induction principle: maybe it should have
a different name):

  scheme Inductive
    {A() -> non empty set, P[set,set]}:
   ex X being Subset of A() st
    for x being Element of A() holds x in X iff P[x,X]
  provided
   for x,X,X' being set st X c= X' & P[x,X] holds P[x,X']

Is something like this already in the library?  If so: how
should I have found it?

Freek