:: Abian's Fixed Point Theorem
:: by Piotr Rudnicki and Andrzej Trybulec
::
:: Received February 22, 1997
:: Copyright (c) 1997-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SETFAM_1, FUNCT_1, SUBSET_1, INT_1, RELAT_1, CARD_1,
XXREAL_0, ARYTM_3, ARYTM_1, FUNCT_7, XBOOLE_0, TARSKI, ZFMISC_1,
FINSET_1, EQREL_1, FUNCOP_1, ABIAN, XCMPLX_0, NAT_1, RECDEF_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
MCART_1, DOMAIN_1, FINSET_1, SETFAM_1, SEQ_4, RELAT_1, FUNCT_1, FUNCT_2,
FUNCOP_1, INT_1, NAT_1, NAT_D, EQREL_1, FUNCT_7, XXREAL_0;
constructors SETFAM_1, XXREAL_0, REAL_1, NAT_1, NAT_D, EQREL_1, SEQ_4,
REALSET1, FUNCT_7, XXREAL_2, RELSET_1;
registrations XBOOLE_0, SUBSET_1, SETFAM_1, FUNCT_1, ORDINAL1, RELSET_1,
PARTFUN1, FINSET_1, XREAL_0, INT_1, MEMBERED, EQREL_1, XXREAL_2,
XXREAL_0, NAT_1;
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 Integer;
attr i is even means
:: ABIAN:def 1
2 divides i;
end;
notation
let i be Integer;
antonym i is odd for i is even;
end;
definition
let n be Nat;
redefine attr n is even means
:: ABIAN:def 2
ex k st n = 2*k;
end;
registration
cluster even for Nat;
cluster odd for Nat;
cluster even for Element of NAT;
cluster odd for Element of NAT;
cluster even for Integer;
cluster odd for Integer;
end;
theorem :: ABIAN:1
for i being Integer holds i is odd iff ex j being Integer st i = 2*j+1;
registration
let i be Integer;
cluster 2*i -> even;
end;
registration
let i be even Integer;
cluster i+1 -> odd;
end;
registration
let i be odd Integer;
cluster i+1 -> even;
end;
registration
let i be even Integer;
cluster i-1 -> odd;
end;
registration
let i be odd Integer;
cluster i-1 -> even;
end;
registration
let i be even Integer, j be Integer;
cluster i*j -> even;
cluster j*i -> even;
end;
registration
let i, j be odd Integer;
cluster i*j -> odd;
end;
registration
let i, j be even Integer;
cluster i+j -> even;
end;
registration
let i be even Integer, j be odd Integer;
cluster i+j -> odd;
cluster j+i -> odd;
end;
registration
let i, j be odd Integer;
cluster i+j -> even;
end;
registration
let i be even Integer, j be odd Integer;
cluster i-j -> odd;
cluster j-i -> odd;
end;
registration
let i, j be odd Integer;
cluster i-j -> even;
end;
registration
let m be even Integer;
cluster m + 2 -> even;
end;
registration
let m be odd Integer;
cluster m + 2 -> odd;
end;
definition
let E, f; let n be Nat;
redefine func iter(f, n) -> Function of E, E;
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;
:: from KNASTER, 2005.02.06, A.T.
definition
let x be object, f be Function;
pred x is_a_fixpoint_of f means
:: ABIAN:def 3
x in dom f & x = f.x;
end;
definition
let A be non empty set, a be Element of A, f be Function of A, A;
redefine pred a is_a_fixpoint_of f means
:: ABIAN:def 4
a = f.a;
end;
definition
let f be Function;
attr f is with_fixpoint means
:: ABIAN:def 5
ex x being object st x is_a_fixpoint_of f;
end;
notation
let f be Function;
antonym f is without_fixpoints for f is with_fixpoint;
end;
definition
let X be set, x be Element of X;
attr x is covering means
:: ABIAN:def 6
union x = union union X;
end;
theorem :: ABIAN:4
sE is covering iff union sE = E;
registration
let E;
cluster non empty finite covering for 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 is without_fixpoints;
definition
let E, f;
func =_f -> Equivalence_Relation of E means
:: ABIAN:def 7
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;
registration
cluster empty-membered -> trivial for set;
end;
registration
let A be set, B be with_non-empty_element set;
cluster non-empty for Function of A, B;
end;
registration
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;
registration
let X be non empty set;
cluster bool X -> with_non-empty_element;
end;
theorem :: ABIAN:8
for E being non empty set, f being Function of E, E st f
is without_fixpoints ex E1, E2, E3 st E1 \/ E2 \/ E3 = E &
f.:E1 misses E1 & f.:E2 misses E2 & f.:E3 misses E3;
begin :: Addenda
:: from SCMFSA9A, 2006.03.14, A.T.
theorem :: ABIAN:9
for n being Nat holds
n is odd iff ex k being Nat st n = 2*k+1;
:: missing, 2008.03.20, A.T.
theorem :: ABIAN:10
for A being non empty set, f being Function of A,A, x being Element of
A holds iter(f,n+1).x = f.(iter(f,n).x);
theorem :: ABIAN:11
for i being Integer holds i is even iff ex j being Integer st i = 2*j;
:: from HEYTING3, MOEBIUS1, 2010.02.13, A.T.
registration
cluster odd for Nat;
cluster even for Nat;
end;
theorem :: ABIAN:12
for n being odd Nat holds 1 <= n;
registration
cluster odd -> non zero for Integer;
end;