Re: [mizar] non necessarily non empty types

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Josef Urban wrote:

> One more attempt. I forgot that in Mizar, Function of A,B already means a
> total (exactly quasi-total) Function, so what I had in mind above is
> called PartFunc of A,B . Less trivial example for Function (or PartFunc)
> of A,B, is e.g.:
>
> let A be set;
> let B be infinite set;
> surjective -> infinite Function of A,B;

OK You can of course to prove the coherence of such registration (see
Attach). For a function; for a partial function it is obviously false.
So, what's the problem?

Andrzej

environ
 vocabulary FINSET_1, ENS_1, RELAT_1, FUNCT_1, SGRAPH1, CARD_1;
 notation FINSET_1, RELAT_1, FUNCT_2, CARD_1;
 constructors FINSET_1, FUNCT_2, RELAT_1, CARD_1;
 definitions FUNCT_2;
 clusters CARD_5, RELSET_1;
 theorems CARD_4, PRE_CIRC, YELLOW_6, FINSET_1;
begin


definition let A be set, B be infinite set;
 cluster onto -> infinite Function of A,B;
 coherence
  proof let F be Function of A,B;
    Card dom F = Card F by PRE_CIRC:21;
    then
F:  Card rng F c= Card F by YELLOW_6:3;
   assume rng F = B;
    then Card rng F is infinite by CARD_4:1;
    then Card F is infinite by F,FINSET_1:13;
   hence F is infinite by CARD_4:1;
  end;
end;