[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] I am trying to figure out...
Hi Adem,
On Sat, 24 Oct 2009, Ozyavas, Adem wrote:
There are two user-defined sets A and B. The first theorem to be proved is:
for a,A being set st a being Element of A holds a in A; ::Q1
It holds if (and only if) A is non-empty.
and the second:
for f being Function of A,B holds dom f = A; ::Q2
For Q2 I tried to use
definition
let X,Y;
let R be Relation of X,Y;
attr R is quasi_total means
:: FUNCT_2:def 1
X = dom R if Y = {} implies X = {}
otherwise R = {};
end;
and looked into the theorems in FUNCT_2 article. The hypothesis "Y = {}
implies X = {}" seems a lot of work and I was wondering if there is
another way.
As in the former case, the statement is clearly accepted if Y is
non-empty. The condition is formulated in this form just to allow
defining functions from X to Y even in a slightly more general situation.
Best,
Adam Naumowicz
=======================================================================
Dept. of Programming and Formal Methods Fax: +48(85)7457662
Institute of Informatics Tel: +48(85)7457559 (office)
University of Bialystok E-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland http://math.uwb.edu.pl/~adamn/
=======================================================================