:: by Piotr Rudnicki and Andrzej Trybulec

::

:: Received February 22, 1997

:: Copyright (c) 1997-2017 Association of Mizar Users

Lm1: for i being Integer holds

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

by INT_1:def 3;

definition
end;

:: deftheorem defines even ABIAN:def 2 :

for n being Nat holds

( n is even iff ex k being Nat st n = 2 * k );

for n being Nat holds

( n is even iff ex k being Nat st n = 2 * k );

registration

existence

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

ex b_{1} being Nat st b_{1} is odd

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

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

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

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

end;
ex b

proof end;

existence ex b

proof end;

cluster ext-real non negative V15() V16() V17() V21() complex V41() integer dim-like V64() even for Element of NAT ;

existence ex b

proof end;

cluster ext-real non negative V15() V16() V17() V21() complex V41() integer dim-like V64() odd for Element of NAT ;

existence ex b

proof end;

existence ex b

proof end;

existence ex b

proof end;

registration
end;

registration
end;

registration

let i be even Integer;

let j be Integer;

coherence

i * j is even

j * i is even ;

end;
let j be Integer;

coherence

i * j is even

proof end;

coherence j * i is even ;

registration
end;

registration
end;

registration

let i be even Integer;

let j be odd Integer;

coherence

not i + j is even

not j + i is even ;

end;
let j be odd Integer;

coherence

not i + j is even

proof end;

coherence not j + i is even ;

registration
end;

registration

let i be even Integer;

let j be odd Integer;

coherence

not i - j is even

not j - i is even

end;
let j be odd Integer;

coherence

not i - j is even

proof end;

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 Nat;

:: original: iter

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

coherence

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

end;
let f be Function of E,E;

let n be Nat;

:: original: iter

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

coherence

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

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;

:: from KNASTER, 2005.02.06, A.T.

:: deftheorem defines is_a_fixpoint_of ABIAN:def 3 :

for x being object

for f being Function holds

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

for x being object

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;

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;

compatibility

( a is_a_fixpoint_of f iff a = f . a )

proof end;

:: deftheorem 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 );

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 );

:: deftheorem defines with_fixpoint ABIAN:def 5 :

for f being Function holds

( f is with_fixpoint iff ex x being object st x is_a_fixpoint_of f );

for f being Function holds

( f is with_fixpoint iff ex x being object st x is_a_fixpoint_of f );

:: deftheorem 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) );

for X being set

for x being Element of X holds

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

registration

let E be set ;

existence

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

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

end;
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 is without_fixpoints

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 is without_fixpoints

proof end;

definition

let E be set ;

let f be Function of E,E;

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 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 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 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 Nat st (iter (f,k)) . x = (iter (f,l)) . y );

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

( [x,y] in it iff ex k, l being Nat st (iter (f,k)) . x = (iter (f,l)) . y );

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_{3} being Equivalence_Relation of E holds

( b_{3} = =_ f iff for x, y being set st x in E & y in E holds

( [x,y] in b_{3} iff ex k, l being Nat st (iter (f,k)) . x = (iter (f,l)) . y ) );

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 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 Nat holds (iter (f,n)) . e in c

proof end;

registration

let A be set ;

let B be with_non-empty_element set ;

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 V35(A,B) for 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;

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;

coherence

not f . a is empty

proof end;

theorem :: ABIAN:8

for E being non empty set

for f being Function of E,E st f is without_fixpoints 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 is without_fixpoints 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;

:: from SCMFSA9A, 2006.03.14, A.T.

:: missing, 2008.03.20, A.T.

theorem :: ABIAN:10

for n being 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

:: from HEYTING3, MOEBIUS1, 2010.02.13, A.T.

registration

existence

ex b_{1} being Nat st b_{1} is odd

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

end;
ex b

proof end;

existence ex b

proof end;

registration
end;