Journal of Formalized Mathematics
Volume 9, 1997
University of Bialystok
Copyright (c) 1997 Association of Mizar Users

### Abian's Fixed Point Theorem

by
Piotr Rudnicki, and
Andrzej Trybulec

MML identifier: ABIAN
[ Mizar article, MML identifier index ]

```environ

vocabulary SETFAM_1, FUNCT_1, ARYTM, MATRIX_2, INT_1, ARYTM_1, FUNCT_4,
TRIANG_1, ZF_REFLE, FUNCOP_1, RELAT_1, SQUARE_1, BOOLE, KNASTER, TARSKI,
FINSET_1, EQREL_1, MCART_1, NAT_1, ABIAN;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
XREAL_0, MCART_1, DOMAIN_1, FINSET_1, SETFAM_1, CQC_SIM1, RELAT_1,
FUNCT_1, FUNCT_2, FUNCOP_1, INT_1, NAT_1, EQREL_1, TRIANG_1, FUNCT_7,
KNASTER;
constructors DOMAIN_1, CQC_SIM1, REAL_1, TRIANG_1, AMI_1, KNASTER, INT_1,
FUNCT_7, MEMBERED;
clusters SUBSET_1, INT_1, FINSET_1, RELSET_1, PRALG_3, PUA2MSS1, TRIANG_1,
MEMBERED, PARTFUN1, ORDINAL2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;

begin

reserve x, y, z, E, E1, E2, E3 for set,
sE for Subset-Family of E,
f for Function of E, E,
k, l, m, n for Nat;

definition
let i be number;
attr i is even means
:: ABIAN:def 1
ex j being Integer st i = 2*j;
antonym i is odd;
end;

definition
let n be Nat;
redefine attr n is even means
:: ABIAN:def 2
ex k st n = 2*k;
antonym n is odd;
end;

definition
cluster even Nat;
cluster odd Nat;
cluster even Integer;
cluster odd Integer;
end;

theorem :: ABIAN:1
for i being Integer
holds i is odd iff ex j being Integer st i = 2*j+1;

definition
let i be Integer;
cluster 2*i -> even;
end;

definition
let i be even Integer;
cluster i+1 -> odd;
end;

definition
let i be odd Integer;
cluster i+1 -> even;
end;

definition
let i be even Integer;
cluster i-1 -> odd;
end;

definition
let i be odd Integer;
cluster i-1 -> even;
end;

definition
let i be even Integer, j be Integer;
cluster i*j -> even;
cluster j*i -> even;
end;

definition
let i, j be odd Integer;
cluster i*j -> odd;
end;

definition
let i, j be even Integer;
cluster i+j -> even;
end;

definition
let i be even Integer, j be odd Integer;
cluster i+j -> odd;
cluster j+i -> odd;
end;

definition
let i, j be odd Integer;
cluster i+j -> even;
end;

definition
let i be even Integer, j be odd Integer;
cluster i-j -> odd;
cluster j-i -> odd;
end;

definition
let i, j be odd Integer;
cluster i-j -> even;
end;

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

definition
let A be set, B be with_non-empty_element set;
cluster non-empty Function of A, B;
end;

definition
let A be non empty set, B be with_non-empty_element set,
f be non-empty Function of A, B,
a be Element of A;
cluster f.a -> non empty;
end;

definition
let X be non empty set;
cluster bool X -> with_non-empty_element;
end;

theorem :: ABIAN:2
for S being non empty Subset of NAT st 0 in S
holds min S = 0;

theorem :: ABIAN:3
for E being non empty set, f being Function of E, E,
x being Element of E
holds iter(f,0).x = x;

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

definition
let f be Function;
pred f has_a_fixpoint means
:: ABIAN:def 3
ex x st x is_a_fixpoint_of f;
antonym f has_no_fixpoint;
end;

definition
let X be set, x be Element of X;
attr x is covering means
:: ABIAN:def 4
union x = union union X;
end;

theorem :: ABIAN:4
sE is covering iff union sE = E;

definition
let E;
cluster non empty finite covering Subset-Family of E;
end;

theorem :: ABIAN:5
for E being set, f being Function of E, E,
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;

definition
let E, f;
func =_f -> Equivalence_Relation of E means
:: ABIAN:def 5

for x, y st x in E & y in E
holds [x,y] in it iff ex k, l st iter(f,k).x = iter(f,l).y;
end;

theorem :: ABIAN:6
for E being non empty set, f being Function of E, E,
c being Element of Class =_f, e being Element of c holds f.e in c;

theorem :: ABIAN:7
for E being non empty set, f being Function of E, E,
c being Element of Class =_f, e being Element of c, n
holds iter(f, n).e in c;

theorem :: ABIAN:8
for E being non empty set, f being Function of E, E
st f has_no_fixpoint
ex E1, E2, E3 st E1 \/ E2 \/ E3 = E &
f.:E1 misses E1 & f.:E2 misses E2 & f.:E3 misses E3;

```