:: by Piotr Rudnicki and Andrzej Trybulec

::

:: Received February 22, 1997

:: Copyright (c) 1997 Association of Mizar Users

begin

:: deftheorem Def1 defines even ABIAN:def 1 :

for i being Integer holds

( i is even iff 2 divides i );

Lm1: for i being Integer holds

( i is even iff ex j being Integer st i = 2 * j )

proof end;

definition

let n be Element of NAT ;

redefine attr n is even means :: ABIAN:def 2

ex k being Element of NAT st n = 2 * k;

compatibility

( n is even iff ex k being Element of NAT st n = 2 * k )

end;
redefine attr n is even means :: ABIAN:def 2

ex k being Element of NAT st n = 2 * k;

compatibility

( n is even iff ex k being Element of NAT st n = 2 * k )

proof end;

:: deftheorem defines even ABIAN:def 2 :

for n being Element of NAT holds

( n is even iff ex k being Element of NAT st n = 2 * k );

registration

cluster ext-real epsilon-transitive epsilon-connected ordinal natural complex V18() integer V56() V57() V58() V59() V60() V61() V62() V74() even Element of NAT ;

existence

ex b_{1} being Element of NAT st b_{1} is even

existence

not for b_{1} being Element of NAT holds b_{1} is even

existence

ex b_{1} being Integer st b_{1} is even

existence

not for b_{1} being Integer holds b_{1} is even

end;
existence

ex b

proof end;

cluster ext-real epsilon-transitive epsilon-connected ordinal natural complex V18() integer V56() V57() V58() V59() V60() V61() V62() V74() odd Element of NAT ;existence

not for b

proof end;

cluster ext-real complex V18() integer even set ;existence

ex b

proof end;

cluster ext-real complex V18() integer odd set ;existence

not for b

proof end;

theorem Th1: :: ABIAN:1

proof end;

registration
end;

registration
end;

registration

let i be even Integer;

let j be Integer;

cluster i * j -> even ;

coherence

i * j is even

coherence

j * i is even ;

end;
let j be Integer;

cluster i * j -> even ;

coherence

i * j is even

proof end;

cluster j * i -> even ;coherence

j * i is even ;

registration
end;

registration
end;

registration

let i be even Integer;

let j be odd Integer;

cluster i + j -> odd ;

coherence

not i + j is even

coherence

not j + i is even ;

end;
let j be odd Integer;

cluster i + j -> odd ;

coherence

not i + j is even

proof end;

cluster j + i -> odd ;coherence

not j + i is even ;

registration
end;

registration

let i be even Integer;

let j be odd Integer;

cluster i - j -> odd ;

coherence

not i - j is even

coherence

not j - i is even

end;
let j be odd Integer;

cluster i - j -> odd ;

coherence

not i - j is even

proof end;

cluster j - i -> odd ;coherence

not j - i is even

proof end;

registration
end;

registration
end;

definition

let E be set ;

let f be Function of E,E;

let n be Element of NAT ;

:: original: iter

redefine func iter (f,n) -> Function of E,E;

coherence

iter (f,n) is Function of E,E by FUNCT_7:85;

end;
let f be Function of E,E;

let n be Element of NAT ;

:: original: iter

redefine func iter (f,n) -> Function of E,E;

coherence

iter (f,n) is Function of E,E by FUNCT_7:85;

theorem Th2: :: ABIAN:2

proof end;

theorem Th3: :: ABIAN:3

for E being non empty set

for f being Function of E,E

for x being Element of E holds (iter (f,0)) . x = x

for f being Function of E,E

for x being Element of E holds (iter (f,0)) . x = x

proof end;

definition

let x be set ;

let f be Function;

pred x is_a_fixpoint_of f means :Def3: :: ABIAN:def 3

( x in dom f & x = f . x );

end;
let f be Function;

pred x is_a_fixpoint_of f means :Def3: :: ABIAN:def 3

( x in dom f & x = f . x );

:: deftheorem Def3 defines is_a_fixpoint_of ABIAN:def 3 :

for x being set

for f being Function holds

( x is_a_fixpoint_of f iff ( x in dom f & x = f . x ) );

definition

let A be non empty set ;

let a be Element of A;

let f be Function of A,A;

:: original: is_a_fixpoint_of

redefine pred a is_a_fixpoint_of f means :Def4: :: ABIAN:def 4

a = f . a;

compatibility

( a is_a_fixpoint_of f iff a = f . a )

end;
let a be Element of A;

let f be Function of A,A;

:: original: is_a_fixpoint_of

redefine pred a is_a_fixpoint_of f means :Def4: :: ABIAN:def 4

a = f . a;

compatibility

( a is_a_fixpoint_of f iff a = f . a )

proof end;

:: deftheorem Def4 defines is_a_fixpoint_of ABIAN:def 4 :

for A being non empty set

for a being Element of A

for f being Function of A,A holds

( a is_a_fixpoint_of f iff a = f . a );

definition

let f be Function;

pred f has_a_fixpoint means :Def5: :: ABIAN:def 5

ex x being set st x is_a_fixpoint_of f;

end;
pred f has_a_fixpoint means :Def5: :: ABIAN:def 5

ex x being set st x is_a_fixpoint_of f;

:: deftheorem Def5 defines has_a_fixpoint ABIAN:def 5 :

for f being Function holds

( f has_a_fixpoint iff ex x being set st x is_a_fixpoint_of f );

definition

let X be set ;

let x be Element of X;

attr x is covering means :Def6: :: ABIAN:def 6

union x = union (union X);

end;
let x be Element of X;

attr x is covering means :Def6: :: ABIAN:def 6

union x = union (union X);

:: deftheorem Def6 defines covering ABIAN:def 6 :

for X being set

for x being Element of X holds

( x is covering iff union x = union (union X) );

theorem Th4: :: ABIAN:4

proof end;

registration

let E be set ;

cluster non empty finite covering Element of bool (bool E);

existence

ex b_{1} being Subset-Family of E st

( not b_{1} is empty & b_{1} is finite & b_{1} is covering )

end;
cluster non empty finite covering Element of bool (bool E);

existence

ex b

( not b

proof end;

theorem :: ABIAN:5

for E being set

for f being Function of E,E

for sE being non empty covering Subset-Family of E st ( for X being Element of sE holds X misses f .: X ) holds

f has_no_fixpoint

for f being Function of E,E

for sE being non empty covering Subset-Family of E st ( for X being Element of sE holds X misses f .: X ) holds

f has_no_fixpoint

proof end;

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 b_{1} being Equivalence_Relation of E st

for x, y being set st x in E & y in E holds

( [x,y] in b_{1} iff ex k, l being Element of NAT st (iter (f,k)) . x = (iter (f,l)) . y )

for b_{1}, b_{2} being Equivalence_Relation of E st ( for x, y being set st x in E & y in E holds

( [x,y] in b_{1} 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 b_{2} iff ex k, l being Element of NAT st (iter (f,k)) . x = (iter (f,l)) . y ) ) holds

b_{1} = b_{2}

end;
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 b

for x, y being set st x in E & y in E holds

( [x,y] in b

proof end;

uniqueness for b

( [x,y] in b

( [x,y] in b

b

proof end;

:: deftheorem Def7 defines =_ ABIAN:def 7 :

for E being set

for f being Function of E,E

for b

( b

( [x,y] in b

theorem Th6: :: ABIAN:6

for E being non empty set

for f being Function of E,E

for c being Element of Class (=_ f)

for e being Element of c holds f . e in c

for f being Function of E,E

for c being Element of Class (=_ f)

for e being Element of c holds f . e in c

proof end;

theorem Th7: :: ABIAN:7

for E being non empty set

for f being Function of E,E

for c being Element of Class (=_ f)

for e being Element of c

for n being Element of NAT holds (iter (f,n)) . e in c

for f being Function of E,E

for c being Element of Class (=_ f)

for e being Element of c

for n being Element of NAT holds (iter (f,n)) . e in c

proof end;

registration

cluster empty-membered -> trivial set ;

coherence

for b_{1} being set st b_{1} is empty-membered holds

b_{1} is trivial
;

end;
coherence

for b

b

registration

let A be set ;

let B be with_non-empty_element set ;

cluster Relation-like non-empty A -defined B -valued Function-like V30(A,B) Element of bool [:A,B:];

existence

ex b_{1} being Function of A,B st b_{1} is non-empty

end;
let B be with_non-empty_element set ;

cluster Relation-like non-empty A -defined B -valued Function-like V30(A,B) Element of bool [:A,B:];

existence

ex b

proof end;

registration

let A be non empty set ;

let B be with_non-empty_element set ;

let f be non-empty Function of A,B;

let a be Element of A;

cluster f . a -> non empty ;

coherence

not f . a is empty

end;
let B be with_non-empty_element set ;

let f be non-empty Function of A,B;

let a be Element of A;

cluster f . a -> non empty ;

coherence

not f . a is empty

proof end;

registration

let X be non empty set ;

cluster bool X -> with_non-empty_element ;

coherence

not bool X is empty-membered

end;
cluster bool X -> with_non-empty_element ;

coherence

not bool X is empty-membered

proof end;

theorem :: ABIAN:8

for E being non empty set

for f being Function of E,E st f has_no_fixpoint holds

ex E1, E2, E3 being set st

( (E1 \/ E2) \/ E3 = E & f .: E1 misses E1 & f .: E2 misses E2 & f .: E3 misses E3 )

for f being Function of E,E st f has_no_fixpoint holds

ex E1, E2, E3 being set st

( (E1 \/ E2) \/ E3 = E & f .: E1 misses E1 & f .: E2 misses E2 & f .: E3 misses E3 )

proof end;

begin

theorem :: ABIAN:9

proof end;

theorem :: ABIAN:10

for n being Element of NAT

for A being non empty set

for f being Function of A,A

for x being Element of A holds (iter (f,(n + 1))) . x = f . ((iter (f,n)) . x)

for A being non empty set

for f being Function of A,A

for x being Element of A holds (iter (f,(n + 1))) . x = f . ((iter (f,n)) . x)

proof end;

theorem :: ABIAN:11

registration

cluster ext-real epsilon-transitive epsilon-connected ordinal natural complex V18() integer odd set ;

existence

not for b_{1} being natural number holds b_{1} is even

existence

ex b_{1} being natural number st b_{1} is even

end;
existence

not for b

proof end;

cluster ext-real epsilon-transitive epsilon-connected ordinal natural complex V18() integer even set ;existence

ex b

proof end;

theorem Th12: :: ABIAN:12

proof end;

registration

cluster integer odd -> non zero set ;

coherence

for b_{1} being Integer st not b_{1} is even holds

not b_{1} is empty
by Th12;

end;
coherence

for b

not b