:: Abian's Fixed Point Theorem
:: by Piotr Rudnicki and Andrzej Trybulec
::
:: Received February 22, 1997
:: Copyright (c) 1997 Association of Mizar Users
:: deftheorem Def1 defines even ABIAN:def 1 :
:: deftheorem defines even ABIAN:def 2 :
theorem Th1: :: ABIAN:1
theorem Th2: :: ABIAN:2
theorem Th3: :: ABIAN:3
:: deftheorem Def3 defines is_a_fixpoint_of ABIAN:def 3 :
:: deftheorem Def4 defines is_a_fixpoint_of ABIAN:def 4 :
:: deftheorem Def5 defines has_a_fixpoint ABIAN:def 5 :
:: deftheorem Def6 defines covering ABIAN:def 6 :
theorem Th4: :: ABIAN:4
theorem :: ABIAN:5
definition
let E be
set ;
let f be
Function of
E,
E;
func =_ f -> Equivalence_Relation of
E means :
Def7:
:: ABIAN:def 7
for
x,
y being
set st
x in E &
y in E holds
(
[x,y] in it iff ex
k,
l being
Element of
NAT st
(iter f,k) . x = (iter f,l) . y );
existence
ex b1 being Equivalence_Relation of E st
for x, y being set st x in E & y in E holds
( [x,y] in b1 iff ex k, l being Element of NAT st (iter f,k) . x = (iter f,l) . y )
uniqueness
for b1, b2 being Equivalence_Relation of E st ( for x, y being set st x in E & y in E holds
( [x,y] in b1 iff ex k, l being Element of NAT st (iter f,k) . x = (iter f,l) . y ) ) & ( for x, y being set st x in E & y in E holds
( [x,y] in b2 iff ex k, l being Element of NAT st (iter f,k) . x = (iter f,l) . y ) ) holds
b1 = b2
end;
:: deftheorem Def7 defines =_ ABIAN:def 7 :
theorem Th6: :: ABIAN:6
theorem Th7: :: ABIAN:7
theorem :: ABIAN:8
theorem :: ABIAN:9
theorem :: ABIAN:10