[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] how to prove...
Hi Adem,
On Mon, 18 May 2009, Ozyavas, Adem wrote:
Dear All,
How does one go about proving that a real number is not a finite sequence:
for n being real number holds not n is FinSequence
Well, in general it's not true with the set-theoretic construction of real
numbers as used in MML - {} is both a real number (zero) and a finite
sequence (empty function)...
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/
=======================================================================