:: Abian's Fixed Point Theorem
:: by Piotr Rudnicki and Andrzej Trybulec
::
:: Received February 22, 1997
:: Copyright (c) 1997-2026 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;
definitions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, SETFAM_1, INT_1;
equalities RELAT_1;
expansions XBOOLE_0, INT_1;
theorems TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, EQREL_1, NAT_1, INT_1, MCART_1,
SCHEME1, FUNCOP_1, SETFAM_1, XBOOLE_0, XBOOLE_1, FUNCT_7, XREAL_1,
XXREAL_0, NAT_D, XXREAL_2;
schemes EQREL_1, FUNCT_2, NAT_1, DOMAIN_1;
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
2 divides i;
end;
notation
let i be Integer;
antonym i is odd for i is even;
end;
Lm1:
for i being Integer holds i is even iff ex j being Integer st i = 2*j
by INT_1:def 3;
definition
let n be Nat;
redefine attr n is even means :: redefines even (ABIAN, definition)
ex k st n = 2*k;
compatibility
proof
hereby
assume n is even;
then 2 divides n;
then consider k being Integer such that
A1: n = 2*k;
0<=k by A1,XREAL_1:132;
then k in NAT by INT_1:3;
then reconsider k as Nat;
take k;
thus n = 2*k by A1;
end;
thus thesis by Lm1;
end;
end;
registration
cluster even for Nat;
existence
proof
take 0, 0;
thus thesis;
end;
cluster odd for Nat;
existence
proof
take 1;
let k be Nat;
thus thesis by NAT_1:15;
end;
cluster even for Element of NAT;
existence
proof
take 0, 0;
thus thesis;
end;
cluster odd for Element of NAT;
existence
proof
take 1;
let k be Nat;
thus thesis by NAT_1:15;
end;
cluster even for Integer;
existence
proof
take 0, 0;
thus thesis;
end;
cluster odd for Integer;
existence
proof
take 1;
assume 1 is even;
then ex k being Integer st 1 = 2*k;
hence contradiction by INT_1:9;
end;
end;
theorem Th1:
for i being Integer holds i is odd iff ex j being Integer st i = 2*j+1
proof
let i be Integer;
hereby
consider k such that
A1: i = k or i = -k by INT_1:2;
consider m being Element of NAT such that
A2: k = 2*m or k = 2*m+1 by SCHEME1:1;
assume
A3: i is odd;
assume
A4: for j being Integer holds i <> 2*j+1;
per cases by A1,A2;
suppose
i = k & k = 2*m;
hence contradiction by A3,Lm1;
end;
suppose
i = -k & k = 2*m;
then i = 2*(-m);
hence contradiction by A3,Lm1;
end;
suppose
i = k & k = 2*m+1;
hence contradiction by A4;
end;
suppose
i = -k & k = 2*m+1;
then i = 2*-(m+1)+1;
hence contradiction by A4;
end;
end;
given j being Integer such that
A5: i = 2*j+1;
given k being Integer such that
A6: i = 2*k;
1 = 2*(k - j) by A5,A6;
hence contradiction by INT_1:9;
end;
registration
let i be Integer;
cluster 2*i -> even;
coherence by Lm1;
end;
registration
let i be even Integer;
cluster i+1 -> odd;
coherence
proof
ex j being Integer st i = 2*j by Lm1;
hence thesis by Th1;
end;
end;
registration
let i be odd Integer;
cluster i+1 -> even;
coherence
proof
consider j being Integer such that
A1: i = 2*j+1 by Th1;
i+1 = 2*(j+1) by A1;
hence thesis;
end;
end;
registration
let i be even Integer;
cluster i-1 -> odd;
coherence
proof
consider j being Integer such that
A1: i = 2*j by Lm1;
i-1 = 2*(j-1)+1 by A1;
hence thesis;
end;
end;
registration
let i be odd Integer;
cluster i-1 -> even;
coherence
proof
ex j being Integer st i = 2*j+1 by Th1;
hence thesis;
end;
end;
registration
let i be even Integer, j be Integer;
cluster i*j -> even;
coherence
proof
consider k being Integer such that
A1: i = 2*k by Lm1;
i*j = 2*(k*j) by A1;
hence thesis;
end;
cluster j*i -> even;
coherence;
end;
registration
let i, j be odd Integer;
cluster i*j -> odd;
coherence
proof
consider l being Integer such that
A1: j = 2*l+1 by Th1;
consider k being Integer such that
A2: i = 2*k+1 by Th1;
i*j = 2*(k*(2*l)+(k*1)+(l*1))+1 by A2,A1;
hence thesis;
end;
end;
registration
let i, j be even Integer;
cluster i+j -> even;
coherence
proof
consider l being Integer such that
A1: j = 2*l by Lm1;
consider k being Integer such that
A2: i = 2*k by Lm1;
i+j = 2*(k+l) by A2,A1;
hence thesis;
end;
end;
registration
let i be even Integer, j be odd Integer;
cluster i+j -> odd;
coherence
proof
consider l being Integer such that
A1: j = 2*l+1 by Th1;
consider k being Integer such that
A2: i = 2*k by Lm1;
i+j = 2*(k+l)+1 by A2,A1;
hence thesis;
end;
cluster j+i -> odd;
coherence;
end;
registration
let i, j be odd Integer;
cluster i+j -> even;
coherence
proof
consider l being Integer such that
A1: j = 2*l+1 by Th1;
consider k being Integer such that
A2: i = 2*k+1 by Th1;
j+i = 2*(k+l+1) by A2,A1;
hence thesis;
end;
end;
registration
let i be even Integer, j be odd Integer;
cluster i-j -> odd;
coherence
proof
consider l being Integer such that
A1: j = 2*l+1 by Th1;
consider k being Integer such that
A2: i = 2*k by Lm1;
i-j = 2*(k-l)-1 by A2,A1;
hence thesis;
end;
cluster j-i -> odd;
coherence
proof
consider l being Integer such that
A3: j = 2*l+1 by Th1;
consider k being Integer such that
A4: i = 2*k by Lm1;
j-i = 2*(l-k)+1 by A4,A3;
hence thesis;
end;
end;
registration
let i, j be odd Integer;
cluster i-j -> even;
coherence
proof
consider l being Integer such that
A1: j = 2*l+1 by Th1;
consider k being Integer such that
A2: i = 2*k+1 by Th1;
i-j = 2*(k-l) by A2,A1;
hence thesis;
end;
end;
registration
let m be even Integer;
cluster m + 2 -> even;
coherence
proof
2 = 2*1;
then reconsider t = 2 as even Integer;
m + t is even;
hence thesis;
end;
end;
registration
let m be odd Integer;
cluster m + 2 -> odd;
coherence
proof
2 = 2*1;
then reconsider t = 2 as even Integer;
m + t is odd;
hence thesis;
end;
end;
definition
let E, f; let n be Nat;
redefine func iter(f, n) -> Function of E, E; :: redefines iter (FUNCT_7, definition)
coherence by FUNCT_7:83;
end;
theorem Th2:
for S being non empty Subset of NAT st 0 in S holds min S = 0
by XXREAL_2:def 7;
theorem Th3:
for E being non empty set, f being Function of E, E, x being
Element of E holds iter(f,0).x = x
proof
let E be non empty set, f be Function of E, E, x be Element of E;
dom f = E by FUNCT_2:def 1;
then
A1: x in dom f \/ rng f by XBOOLE_0:def 3;
thus iter(f,0).x = id(field f).x by FUNCT_7:68
.= x by A1,FUNCT_1:17;
end;
:: from KNASTER, 2005.02.06, A.T.
definition
let x be object, f be Function;
pred x is_a_fixpoint_of f means
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 :: redefines is_a_fixpoint_of (ABIAN, definition)
a = f.a;
compatibility
proof
thus a is_a_fixpoint_of f implies a = f.a;
assume
A1: a = f.a;
a in A;
hence a in dom f by FUNCT_2:52;
thus a = f.a by A1;
end;
end;
definition
let f be Function;
attr f is with_fixpoint means
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
union x = union union X;
end;
theorem Th4:
sE is covering iff union sE = E
proof
union union bool bool E = union bool E by ZFMISC_1:81
.= E by ZFMISC_1:81;
hence thesis;
end;
registration
let E;
cluster non empty finite covering for Subset-Family of E;
existence
proof
reconsider sE = {E} as Subset-Family of E by ZFMISC_1:68;
take sE;
thus sE is non empty finite;
union sE = E by ZFMISC_1:25;
hence thesis by Th4;
end;
end;
theorem
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
proof
let E be set, f be Function of E, E, sE be non empty covering Subset-Family
of E;
assume
A1: for X being Element of sE holds X misses f.:X;
given x being object such that
A2: x is_a_fixpoint_of f;
A3: f.x = x by A2;
A4: x in dom f by A2;
dom f = E by FUNCT_2:52;
then x in union sE by A4,Th4;
then consider X being set such that
A5: x in X and
A6: X in sE by TARSKI:def 4;
f.x in f.:X by A4,A5,FUNCT_1:def 6;
then X meets f.:X by A3,A5,XBOOLE_0:3;
hence contradiction by A1,A6;
end;
definition
let E, f;
func =_f -> Equivalence_Relation of E means
:Def7:
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;
existence
proof
defpred P[object,object] means
$1 in E & $2 in E & ex k, l st iter(f,k).$1 = iter(f,l).$2;
A1: now
let x be object;
A2: iter(f,0).x = iter(f,0).x;
assume x in E;
hence P[x,x] by A2;
end;
A3: now
let x,y,z be object;
assume that
A4: P[x,y] and
A5: P[y,z];
consider k, l such that
A6: iter(f,k).x = iter(f,l).y by A4;
consider m, n such that
A7: iter(f,m).y =iter(f,n).z by A5;
A8: dom iter(f,m) = E by FUNCT_2:52;
A9: dom iter(f,l) = E by FUNCT_2:52;
A10: dom iter(f,k) = E by FUNCT_2:52;
A11: dom iter(f,n) = E by FUNCT_2:52;
iter(f,k+m).x = (iter(f,m)*iter(f,k)).x by FUNCT_7:77
.= iter(f,m).(iter(f,l).y) by A4,A6,A10,FUNCT_1:13
.= (iter(f,m)*(iter(f,l))).y by A4,A9,FUNCT_1:13
.= (iter(f,m+l)).y by FUNCT_7:77
.= (iter(f,l)*iter(f,m)).y by FUNCT_7:77
.= iter(f,l).(iter(f,n).z) by A4,A7,A8,FUNCT_1:13
.= (iter(f,l)*iter(f,n)).z by A5,A11,FUNCT_1:13
.= iter(f,l+n).z by FUNCT_7:77;
hence P[x,z] by A4,A5;
end;
A12: for x,y being object st P[x,y] holds P[y,x];
consider EqR being Equivalence_Relation of E such that
A13: for x,y being object holds [x,y] in EqR iff x in E & y in E & P[x,y]
from
EQREL_1:sch 1(A1, A12, A3);
take EqR;
let x, y;
assume x in E & y in E;
hence thesis by A13;
end;
uniqueness
proof
let IT1, IT2 be Equivalence_Relation of E such that
A14: for x, y st x in E & y in E holds [x,y] in IT1 iff ex k, l st
iter(f,k).x = iter(f,l).y and
A15: for x, y st x in E & y in E holds [x,y] in IT2 iff ex k, l st
iter(f,k).x = iter(f,l).y;
let a, b be object;
hereby
assume
A16: [a, b] in IT1;
then
A17: a in E & b in E by ZFMISC_1:87;
then ex k, l st iter(f,k).a = iter(f,l).b by A14,A16;
hence [a, b] in IT2 by A15,A17;
end;
assume
A18: [a, b] in IT2;
then
A19: a in E & b in E by ZFMISC_1:87;
then ex k, l st iter(f,k).a = iter(f,l).b by A15,A18;
hence thesis by A14,A19;
end;
end;
theorem Th6:
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
proof
let E be non empty set, f be Function of E, E;
let c be Element of Class =_f, e be Element of c;
dom f = E by FUNCT_2:def 1;
then
A1: f.e in dom f \/ rng f by XBOOLE_0:def 3;
ex x9 being object st x9 in E & c = Class(=_f, x9) by EQREL_1:def 3;
then
A2: c = Class(=_f, e) by EQREL_1:23;
iter(f, 1).e = f.e by FUNCT_7:70
.= id(field f).(f.e) by A1,FUNCT_1:17
.= iter(f, 0).(f.e) by FUNCT_7:68;
then [f.e,e] in =_f by Def7;
hence thesis by A2,EQREL_1:19;
end;
theorem Th7:
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
proof
let E be non empty set, f be Function of E, E;
let c be Element of Class =_f, e be Element of c, n;
dom f = E by FUNCT_2:def 1;
then iter(f,n).e in dom f \/ rng f by XBOOLE_0:def 3;
then iter(f, n).e = id(field f).(iter(f,n).e) by FUNCT_1:17
.= iter(f, 0).(iter(f,n).e) by FUNCT_7:68;
then
A1: [iter(f,n).e,e] in =_f by Def7;
ex x9 being object st x9 in E & c = Class(=_f, x9) by EQREL_1:def 3;
then c = Class(=_f, e) by EQREL_1:23;
hence thesis by A1,EQREL_1:19;
end;
registration
cluster empty-membered -> trivial for set;
coherence;
end;
registration
let A be set, B be with_non-empty_element set;
cluster non-empty for Function of A, B;
existence
proof
consider X being non empty set such that
A1: X in B by SETFAM_1:def 10;
reconsider f = A --> X as Function of A, B by A1,FUNCOP_1:45;
take f;
let n be object;
assume n in dom f;
then n in A by FUNCOP_1:13;
hence thesis by FUNCOP_1:7;
end;
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;
coherence
proof
dom f = A by FUNCT_2:def 1;
then f.a in rng f by FUNCT_1:def 3;
hence thesis;
end;
end;
registration
let X be non empty set;
cluster bool X -> with_non-empty_element;
coherence
proof
take X;
thus thesis by ZFMISC_1:def 1;
end;
end;
theorem
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
proof
let E be non empty set, f be Function of E, E;
defpred P[set,Element of [:bool E qua set, bool E, bool E:]] means
$2`1_3 \/ $2`2_3 \/ $2`3_3 = $1 &
f.:($2`1_3) misses $2`1_3 & f.:($2`2_3) misses $2`2_3 & f.:($2`3_3)
misses $2`3_3;
deffunc i(Nat) = iter(f, $1);
assume
A1: f is without_fixpoints;
A2: for a being Element of Class =_f ex b being Element of [:bool E, bool E,
bool E:] st P[a,b]
proof
reconsider c3 = {} as Subset of E by XBOOLE_1:2;
let c be Element of Class =_f;
consider x0 being object such that
A3: x0 in E and
A4: c = Class(=_f, x0) by EQREL_1:def 3;
reconsider x0 as Element of c by A3,A4,EQREL_1:20;
defpred P[set] means ex k, l st i(k).$1 = i(l).x0 & k is even & l is even;
set c1 = { x where x is Element of c : P[x] };
c1 is Subset of c from DOMAIN_1:sch 7;
then reconsider c1 as Subset of E by XBOOLE_1:1;
defpred P[set] means ex k, l st i(k).$1 = i(l).x0 & k is odd & l is even;
set c2 = { x where x is Element of c : P[x] };
c2 is Subset of c from DOMAIN_1:sch 7;
then reconsider c2 as Subset of E by XBOOLE_1:1;
per cases;
suppose
A5: c1 misses c2;
take b = [c1,c2,c3];
A6: b`2_3 = c2 by MCART_1:def 6;
A7: b`3_3 = c3 by MCART_1:def 7;
A8: b`1_3 = c1 by MCART_1:def 5;
thus b`1_3 \/ b`2_3 \/ b`3_3 = c
proof
hereby
let x be object;
assume
A9: x in b`1_3 \/ b`2_3 \/ b`3_3;
per cases by A8,A6,A7,A9,XBOOLE_0:def 3;
suppose
x in c1;
then
ex xx being Element of c st x = xx & ex k, l st i(k).xx = i(l)
.x0 & k is even & l is even;
hence x in c;
end;
suppose
x in c2;
then
ex xx being Element of c st x = xx & ex k, l st i(k).xx = i(l)
.x0 & k is odd & l is even;
hence x in c;
end;
suppose
x in c3;
hence x in c;
end;
end;
let x be object;
assume x in c;
then reconsider xc = x as Element of c;
[xc,x0] in =_f by A4,EQREL_1:19;
then consider k, l such that
A10: i(k).xc = i(l).x0 by Def7;
A11: dom i(l) = E by FUNCT_2:def 1;
A12: dom i(k) = E by FUNCT_2:def 1;
per cases;
suppose
A13: k is even;
then reconsider k as even Nat;
thus x in b`1_3 \/ b`2_3 \/ b`3_3
proof
per cases;
suppose
l is even;
then xc in c1 by A10,A13;
hence thesis by A8,A7,XBOOLE_0:def 3;
end;
suppose
l is odd;
then reconsider l as odd Nat;
i(k+1).xc = (f*i(k)).xc by FUNCT_7:71
.= f.(i(l).x0) by A10,A12,FUNCT_1:13
.= (f*i(l)).x0 by A11,FUNCT_1:13
.= i(l+1).x0 by FUNCT_7:71;
then xc in c2;
hence thesis by A6,A7,XBOOLE_0:def 3;
end;
end;
end;
suppose
A14: k is odd;
then reconsider k as odd Nat;
thus x in b`1_3 \/ b`2_3 \/ b`3_3
proof
per cases;
suppose
l is even;
then xc in c2 by A10,A14;
hence thesis by A6,A7,XBOOLE_0:def 3;
end;
suppose
l is odd;
then reconsider l as odd Nat;
i(k+1).xc = (f*i(k)).xc by FUNCT_7:71
.= f.(i(l).x0) by A10,A12,FUNCT_1:13
.= (f*i(l)).x0 by A11,FUNCT_1:13
.= i(l+1).x0 by FUNCT_7:71;
then xc in c1;
hence thesis by A8,A7,XBOOLE_0:def 3;
end;
end;
end;
end;
f.:c1 c= c2
proof
let y be object;
A15: dom f = E by FUNCT_2:def 1;
assume y in f.:c1;
then consider x being object such that
x in dom f and
A16: x in c1 and
A17: y = f.x by FUNCT_1:def 6;
consider xx being Element of c such that
A18: x = xx and
A19: ex k, l st i(k).xx = i(l).x0 & k is even & l is even by A16;
consider k, l such that
A20: i(k).xx = i(l).x0 and
A21: k is even & l is even by A19;
reconsider k, l as even Nat by A21;
reconsider k1 = k+1 as odd Element of NAT;
reconsider l1 = l+1 as odd Element of NAT;
reconsider l2 = l1+1 as even Element of NAT;
A22: dom i(k) = E by FUNCT_2:def 1;
reconsider yc = y as Element of c by A17,A18,Th6;
A23: dom i(l) = E by FUNCT_2:def 1;
A24: dom i(k1) = E by FUNCT_2:def 1;
A25: i(k1+1).xx = (i(k1)*f).xx by FUNCT_7:69
.= i(k1).(f.xx) by A15,FUNCT_1:13;
A26: dom i(l1) = E by FUNCT_2:def 1;
i(k1+1).xx = (f*i(k1)).xx by FUNCT_7:71
.= f.(i(k1).xx) by A24,FUNCT_1:13
.= f.((f*i(k)).xx) by FUNCT_7:71
.= f.(f.(i(l).x0)) by A20,A22,FUNCT_1:13
.= f.((f*i(l)).x0) by A23,FUNCT_1:13
.= f.(i(l1).x0) by FUNCT_7:71
.= (f*i(l1)).x0 by A26,FUNCT_1:13
.= i(l2).x0 by FUNCT_7:71;
then yc in c2 by A17,A18,A25;
hence thesis;
end;
hence f.:(b`1_3) misses b`1_3 by A5,A8,XBOOLE_1:63;
f.:c2 c= c1
proof
let y be object;
A27: dom f = E by FUNCT_2:def 1;
assume y in f.:c2;
then consider x being object such that
x in dom f and
A28: x in c2 and
A29: y = f.x by FUNCT_1:def 6;
consider xx being Element of c such that
A30: x = xx and
A31: ex k, l st i(k).xx = i(l).x0 & k is odd & l is even by A28;
consider k, l such that
A32: i(k).xx = i(l).x0 and
A33: k is odd and
A34: l is even by A31;
reconsider l as even Nat by A34;
reconsider k as odd Nat by A33;
reconsider k1 = k+1 as even Element of NAT;
reconsider l1 = l+1 as odd Element of NAT;
reconsider l2 = l1+1 as even Element of NAT;
A35: dom i(k) = E by FUNCT_2:def 1;
reconsider yc = y as Element of c by A29,A30,Th6;
A36: dom i(l) = E by FUNCT_2:def 1;
A37: dom i(k1) = E by FUNCT_2:def 1;
A38: i(k1+1).xx = (i(k1)*f).xx by FUNCT_7:69
.= i(k1).(f.xx) by A27,FUNCT_1:13;
A39: dom i(l1) = E by FUNCT_2:def 1;
i(k1+1).xx = (f*i(k1)).xx by FUNCT_7:71
.= f.(i(k1).xx) by A37,FUNCT_1:13
.= f.((f*i(k)).xx) by FUNCT_7:71
.= f.(f.(i(l).x0)) by A32,A35,FUNCT_1:13
.= f.((f*i(l)).x0) by A36,FUNCT_1:13
.= f.(i(l1).x0) by FUNCT_7:71
.= (f*i(l1)).x0 by A39,FUNCT_1:13
.= i(l2).x0 by FUNCT_7:71;
then yc in c1 by A29,A30,A38;
hence thesis;
end;
hence f.:(b`2_3) misses b`2_3 by A5,A6,XBOOLE_1:63;
thus thesis by A7;
end;
suppose
c1 meets c2;
then consider x1 being object such that
A40: x1 in c1 and
A41: x1 in c2 by XBOOLE_0:3;
consider x11 being Element of c such that
A42: x1 = x11 and
A43: ex k, l st i(k).x11 = i(l).x0 & k is even & l is even by A40;
consider x12 being Element of c such that
A44: x1 = x12 and
A45: ex k, l st i(k).x12 = i(l).x0 & k is odd & l is even by A41;
consider k2, l2 being Nat such that
A46: i(k2).x12 = i(l2).x0 and
A47: k2 is odd and
A48: l2 is even by A45;
reconsider x1 as Element of c by A42;
consider k1, l1 being Nat such that
A49: i(k1).x11 = i(l1).x0 and
A50: k1 is even & l1 is even by A43;
A51: dom i(k1) = E by FUNCT_2:def 1;
A52: dom i(l1) = E by FUNCT_2:def 1;
A53: i(l2+k1).x1 = (i(l2)*i(k1)).x1 by FUNCT_7:77
.= i(l2).(i(l1).x0) by A42,A49,A51,FUNCT_1:13
.= (i(l2)*i(l1)).x0 by A52,FUNCT_1:13
.= i(l1+l2).x0 by FUNCT_7:77;
A54: dom i(l2) = E by FUNCT_2:def 1;
A55: dom i(k2) = E by FUNCT_2:def 1;
A56: i(l1+k2).x1 = (i(l1)*i(k2)).x1 by FUNCT_7:77
.= i(l1).(i(l2).x0) by A44,A46,A55,FUNCT_1:13
.= (i(l1)*i(l2)).x0 by A54,FUNCT_1:13
.= i(l1+l2).x0 by FUNCT_7:77;
ex r being Element of E, k being odd Element of NAT st i(k).r = r &
r in c
proof
reconsider k2 as odd Nat by A47;
reconsider k1, l1, l2 as even Nat by A50,A48;
A57: dom i(k1+l2) = E by FUNCT_2:def 1;
A58: dom i(k2+l1) = E by FUNCT_2:def 1;
per cases by XXREAL_0:1;
suppose
k1+l2 < k2+l1;
then reconsider k = k2+l1-(k1+l2) as Element of NAT by INT_1:5;
take r = i(k1+l2).x1;
reconsider k as odd Element of NAT;
take k;
i(k).(i(k1+l2).x1) = (i(k)*i(k1+l2)).x1 by A57,FUNCT_1:13
.= i(k+(k1+l2)).x1 by FUNCT_7:77
.= i(k1+l2).x1 by A56,A53;
hence i(k).r = r;
thus thesis by Th7;
end;
suppose
k1+l2 > k2+l1;
then reconsider k = k1+l2-(k2+l1) as Element of NAT by INT_1:5;
take r = i(k2+l1).x1;
reconsider k as odd Element of NAT;
take k;
i(k).(i(k2+l1).x1) = (i(k)*i(k2+l1)).x1 by A58,FUNCT_1:13
.= i(k+(k2+l1)).x1 by FUNCT_7:77
.= i(k2+l1).x1 by A56,A53;
hence i(k).r = r;
thus thesis by Th7;
end;
end;
then consider r being Element of E, k being odd Element of NAT such that
A59: i(k).r = r and
A60: r in c;
reconsider r as Element of c by A60;
deffunc F(set) = {l where l is Element of NAT : i(l).$1 = r};
A61: for x being Element of c holds F(x) in bool NAT
proof
let x be Element of c;
defpred P1[Element of NAT] means i($1).x = r;
{ l where l is Element of NAT : P1[l]} is Subset of NAT from
DOMAIN_1:sch 7;
hence thesis;
end;
consider Odl being Function of c, bool NAT such that
A62: for x being Element of c holds Odl.x = F(x) from FUNCT_2:sch 8(
A61);
now
defpred P[Nat] means i(k*$1).r = r;
let n be object;
assume n in dom Odl;
then reconsider nc = n as Element of c by FUNCT_2:def 1;
A63: Odl.nc = {l where l is Element of NAT : i(l).nc = r} by A62;
A64: now
let i be Nat;
assume
A65: P[i];
A66: dom i(k) = E by FUNCT_2:def 1;
i(k*(i+1)).r = i(k*i+k*1).r .= (i(k*i)*i(k)).r by FUNCT_7:77
.= r by A59,A65,A66,FUNCT_1:13;
hence P[i+1];
end;
A67: P[0] by Th3;
A68: for i being Nat holds P[i] from NAT_1:sch 2(A67,A64);
ex x9 being object st x9 in E & c = Class(=_f, x9) by EQREL_1:def 3;
then [nc, r] in =_f by EQREL_1:22;
then consider kn, ln being Nat such that
A69: iter(f,kn).nc = iter(f,ln).r by Def7;
A70: dom i(ln) = E by FUNCT_2:def 1;
set mk = ln mod k;
set dk = ln div k;
A71: dom i(kn) = E by FUNCT_2:def 1;
A72: 2*0 <> k;
then mk < k by NAT_D:1;
then reconsider kmk = k - mk as Element of NAT by INT_1:5;
ln = k*dk+mk by A72,NAT_D:2;
then
A73: ln+kmk = k*(dk+1);
i(kmk+kn).nc = (i(kmk)*i(kn)).nc by FUNCT_7:77
.= i(kmk).(i(ln).r) by A69,A71,FUNCT_1:13
.= (i(kmk)*i(ln)).r by A70,FUNCT_1:13
.= i(k*(dk+1)).r by A73,FUNCT_7:77
.= r by A68;
then kn+kmk in Odl.n by A63;
hence Odl.n is non empty;
end;
then reconsider Odl as non-empty Function of c, bool NAT by FUNCT_1:def 9
;
deffunc F(Element of c) = min (Odl.$1);
consider odl being Function of c, NAT such that
A74: for x being Element of c holds odl.x = F(x) from FUNCT_2:sch 4;
defpred P1[Element of c] means odl.$1 is even;
set c1 = { x where x is Element of c : P1[x]};
set d1 = c1 \ {r};
c1 is Subset of c from DOMAIN_1:sch 7;
then
A75: d1 c= c by XBOOLE_1:1;
i(0).r = r by Th3;
then 0 in {l where l is Element of NAT : i(l).r = r};
then 0 in Odl.r by A62;
then min (Odl.r) = 0 by Th2;
then
A76: odl.r = 2*0 by A74;
then
A77: r in c1;
reconsider d1 as Subset of E by A75,XBOOLE_1:1;
defpred P2[Element of c] means odl.$1 is odd;
set d2 = { x where x is Element of c : P2[x]};
d2 is Subset of c from DOMAIN_1:sch 7;
then reconsider d2 as Subset of E by XBOOLE_1:1;
A78: for x being Element of c st x <> r holds odl.(f.x) = (odl.x qua
Element of NAT)-1
proof
let x be Element of c;
reconsider fx = f.x as Element of c by Th6;
reconsider ofx = odl.(fx), ox = odl.x as Element of NAT;
assume
A79: x <> r;
now
assume odl.x = 0;
then 0 = min (Odl.x) by A74;
then 0 in Odl.x by XXREAL_2:def 7;
then 0 in {l where l is Element of NAT : i(l).x = r} by A62;
then ex l being Element of NAT st l = 0 & i(l).x = r;
hence contradiction by A79,Th3;
end;
then reconsider ox1 = ox-1 as Element of NAT by INT_1:5,NAT_1:14;
ox = min (Odl.x) by A74;
then ox in Odl.x by XXREAL_2:def 7;
then ox in {l where l is Element of NAT : i(l).x = r} by A62;
then
A80: ex l being Element of NAT st l = ox & i(l).x = r;
A81: dom f = E by FUNCT_2:def 1;
then i(ox1).fx = (i(ox1)*f).x by FUNCT_1:13
.= i(ox1+1).x by FUNCT_7:69
.= i(ox).x;
then ox1 in {l where l is Element of NAT : i(l).fx = r} by A80;
then
A82: ox1 in Odl.fx by A62;
ofx = min (Odl.fx) by A74;
then ofx in Odl.fx by XXREAL_2:def 7;
then ofx in {l where l is Element of NAT : i(l).fx = r} by A62;
then
A83: ex l being Element of NAT st l = ofx & i(l).fx = r;
i(ofx+1).x = (i(ofx)*f).x by FUNCT_7:69
.= i(ofx).fx by A81,FUNCT_1:13;
then ofx+1 in {l where l is Element of NAT : i(l).x = r} by A83;
then
A84: ofx+1 in Odl.x by A62;
ox = min (Odl.x) by A74;
then ofx+1 >= ox by A84,XXREAL_2:def 7;
then
A85: ofx >= ox-1 by XREAL_1:20;
ofx = min (Odl.fx) by A74;
then ofx <= ox-1 by A82,XXREAL_2:def 7;
hence thesis by A85,XXREAL_0:1;
end;
A86: f.:d1 c= d2
proof
let y be object;
assume y in f.:d1;
then consider x being object such that
x in dom f and
A87: x in d1 and
A88: y = f.x by FUNCT_1:def 6;
x in c1 by A87;
then consider xx being Element of c such that
A89: x = xx and
A90: odl.xx is even;
reconsider ox = odl.xx as even Element of NAT by A90;
reconsider yc = y as Element of c by A88,A89,Th6;
r <> xx by A87,A89,ZFMISC_1:56;
then odl.yc = ox-1 by A78,A88,A89;
hence thesis;
end;
A91: c1 \/ d2 = c
proof
hereby
let x be object;
assume
A92: x in c1 \/ d2;
per cases by A92,XBOOLE_0:def 3;
suppose
x in c1;
then ex xc being Element of c st xc = x & odl.xc is even;
hence x in c;
end;
suppose
x in d2;
then ex xc being Element of c st xc = x & odl.xc is odd;
hence x in c;
end;
end;
let x be object;
assume x in c;
then reconsider xc = x as Element of c;
odl.xc is even or odl.xc is odd;
then x in c1 or x in d2;
hence thesis by XBOOLE_0:def 3;
end;
reconsider d3 = {r} as Subset of E by ZFMISC_1:31;
take b = [d1,d2,d3];
A93: b`1_3 = d1 by MCART_1:def 5;
A94: b`2_3 = d2 by MCART_1:def 6;
A95: b`3_3 = d3 by MCART_1:def 7;
d1 \/ d3 = c1 \/ d3 by XBOOLE_1:39
.= c1 by A77,ZFMISC_1:40;
hence b`1_3 \/ b`2_3 \/ b`3_3 = c by A93,A94,A95,A91,XBOOLE_1:4;
A96: c1 misses d2
proof
assume c1 meets d2;
then consider z being object such that
A97: z in c1 & z in d2 by XBOOLE_0:3;
( ex x being Element of c st z = x & odl.x is even)& ex x being
Element of c st z = x & odl.x is odd by A97;
hence contradiction;
end;
then d1 misses d2 by XBOOLE_1:63;
hence f.:(b`1_3) misses b`1_3 by A93,A86,XBOOLE_1:63;
f.:d2 c= c1
proof
let y be object;
assume y in f.:d2;
then consider x being object such that
x in dom f and
A98: x in d2 and
A99: y = f.x by FUNCT_1:def 6;
consider xx being Element of c such that
A100: x = xx and
A101: odl.xx is odd by A98;
reconsider ox = odl.xx as odd Element of NAT by A101;
reconsider yc = y as Element of c by A99,A100,Th6;
odl.yc = ox-1 by A76,A78,A99,A100;
hence thesis;
end;
hence f.:(b`2_3) misses b`2_3 by A94,A96,XBOOLE_1:63;
thus f.:(b`3_3) misses b`3_3
proof
assume f.:(b`3_3) meets b`3_3;
then consider y being object such that
A102: y in f.:(b`3_3) and
A103: y in b`3_3 by XBOOLE_0:3;
A104: y = r by A95,A103,TARSKI:def 1;
consider x being object such that
x in dom f and
A105: x in {r} and
A106: y = f.x by A95,A102,FUNCT_1:def 6;
x = r by A105,TARSKI:def 1;
then r is_a_fixpoint_of f by A104,A106;
hence contradiction by A1;
end;
end;
end;
consider F being Function of Class =_f, [:bool E, bool E, bool E:] such that
A107: for a being Element of Class =_f holds P[a,F.a] from FUNCT_2:sch 3
(A2);
set E3c = the set of all (F.c)`3_3 where c is Element of Class =_f;
set E2c = the set of all (F.c)`2_3 where c is Element of Class =_f;
set E1c = the set of all (F.c)`1_3 where c is Element of Class =_f;
set E1 = union E1c;
set E2 = union E2c;
set E3 = union E3c;
take E1, E2, E3;
thus E1 \/ E2 \/ E3 = E
proof
hereby
let x be object;
assume x in E1 \/ E2 \/ E3;
then
A108: x in E1 \/ E2 or x in E3 by XBOOLE_0:def 3;
per cases by A108,XBOOLE_0:def 3;
suppose
x in E1;
then consider Y being set such that
A109: x in Y and
A110: Y in E1c by TARSKI:def 4;
ex c being Element of Class =_f st Y = (F.c)`1_3 by A110;
hence x in E by A109;
end;
suppose
x in E2;
then consider Y being set such that
A111: x in Y and
A112: Y in E2c by TARSKI:def 4;
ex c being Element of Class =_f st Y = (F.c)`2_3 by A112;
hence x in E by A111;
end;
suppose
x in E3;
then consider Y being set such that
A113: x in Y and
A114: Y in E3c by TARSKI:def 4;
ex c being Element of Class =_f st Y = (F.c)`3_3 by A114;
hence x in E by A113;
end;
end;
let x be object;
set c = Class(=_f,x);
assume
A115: x in E;
then
A116: x in c by EQREL_1:20;
reconsider c as Element of Class =_f by A115,EQREL_1:def 3;
x in (F.c)`1_3 \/ (F.c)`2_3 \/ (F.c)`3_3 by A107,A116;
then
A117: x in (F.c)`1_3 \/ (F.c)`2_3 or x in (F.c)`3_3 by XBOOLE_0:def 3;
per cases by A117,XBOOLE_0:def 3;
suppose
A118: x in (F.c)`1_3;
(F.c)`1_3 in E1c;
then x in E1 by A118,TARSKI:def 4;
then x in E1 \/ E2 by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
suppose
A119: x in (F.c)`2_3;
(F.c)`2_3 in E2c;
then x in E2 by A119,TARSKI:def 4;
then x in E1 \/ E2 by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
suppose
A120: x in (F.c)`3_3;
(F.c)`3_3 in E3c;
then x in E3 by A120,TARSKI:def 4;
hence thesis by XBOOLE_0:def 3;
end;
end;
thus f.:E1 misses E1
proof
assume not thesis;
then consider x being object such that
A121: x in f.:E1 and
A122: x in E1 by XBOOLE_0:3;
consider Y being set such that
A123: x in Y and
A124: Y in E1c by A122,TARSKI:def 4;
consider c being Element of Class =_f such that
A125: Y = (F.c)`1_3 by A124;
x in (F.c)`1_3 \/ (F.c)`2_3 by A123,A125,XBOOLE_0:def 3;
then x in (F.c)`1_3 \/ (F.c)`2_3 \/ (F.c)`3_3 by XBOOLE_0:def 3;
then
A126: x in c by A107;
ex x9 being object st x9 in E & c = Class(=_f, x9) by EQREL_1:def 3;
then
A127: c = Class(=_f, x) by A126,EQREL_1:23;
dom f = E by FUNCT_2:def 1;
then
A128: x in dom f \/ rng f by A123,A125,XBOOLE_0:def 3;
consider xx being object such that
A129: xx in dom f and
A130: xx in E1 and
A131: x = f.xx by A121,FUNCT_1:def 6;
consider YY being set such that
A132: xx in YY and
A133: YY in E1c by A130,TARSKI:def 4;
consider cc being Element of Class =_f such that
A134: YY = (F.cc)`1_3 by A133;
xx in (F.cc)`1_3 \/ (F.cc)`2_3 by A132,A134,XBOOLE_0:def 3;
then xx in (F.cc)`1_3 \/ (F.cc)`2_3 \/ (F.cc)`3_3 by XBOOLE_0:def 3;
then
A135: xx in cc by A107;
ex xx9 being object st xx9 in E & cc = Class(=_f, xx9) by EQREL_1:def 3;
then
A136: cc = Class(=_f, xx) by A135,EQREL_1:23;
iter(f, 1).xx = x by A131,FUNCT_7:70
.= id(field f).x by A128,FUNCT_1:17
.= iter(f, 0).x by FUNCT_7:68;
then [x,xx] in =_f by A123,A125,A132,A134,Def7;
then
A137: Class(=_f, x) = Class(=_f, xx) by A123,A125,EQREL_1:35;
A138: f.xx in f.:YY by A129,A132,FUNCT_1:def 6;
f.:YY misses YY by A107,A134;
hence contradiction by A123,A125,A131,A134,A127,A136,A137,A138,XBOOLE_0:3;
end;
thus f.:E2 misses E2
proof
assume not thesis;
then consider x being object such that
A139: x in f.:E2 and
A140: x in E2 by XBOOLE_0:3;
consider Y being set such that
A141: x in Y and
A142: Y in E2c by A140,TARSKI:def 4;
consider c being Element of Class =_f such that
A143: Y = (F.c)`2_3 by A142;
x in (F.c)`1_3 \/ (F.c)`2_3 by A141,A143,XBOOLE_0:def 3;
then x in (F.c)`1_3 \/ (F.c)`2_3 \/ (F.c)`3_3 by XBOOLE_0:def 3;
then
A144: x in c by A107;
ex x9 being object st x9 in E & c = Class(=_f, x9) by EQREL_1:def 3;
then
A145: c = Class(=_f, x) by A144,EQREL_1:23;
dom f = E by FUNCT_2:def 1;
then
A146: x in dom f \/ rng f by A141,A143,XBOOLE_0:def 3;
consider xx being object such that
A147: xx in dom f and
A148: xx in E2 and
A149: x = f.xx by A139,FUNCT_1:def 6;
consider YY being set such that
A150: xx in YY and
A151: YY in E2c by A148,TARSKI:def 4;
consider cc being Element of Class =_f such that
A152: YY = (F.cc)`2_3 by A151;
xx in (F.cc)`1_3 \/ (F.cc)`2_3 by A150,A152,XBOOLE_0:def 3;
then xx in (F.cc)`1_3 \/ (F.cc)`2_3 \/ (F.cc)`3_3 by XBOOLE_0:def 3;
then
A153: xx in cc by A107;
ex xx9 being object st xx9 in E & cc = Class(=_f, xx9) by EQREL_1:def 3;
then
A154: cc = Class(=_f, xx) by A153,EQREL_1:23;
iter(f, 1).xx = x by A149,FUNCT_7:70
.= id(field f).x by A146,FUNCT_1:17
.= iter(f, 0).x by FUNCT_7:68;
then [x,xx] in =_f by A141,A143,A150,A152,Def7;
then
A155: Class(=_f, x) = Class(=_f, xx) by A141,A143,EQREL_1:35;
A156: f.xx in f.:YY by A147,A150,FUNCT_1:def 6;
f.:YY misses YY by A107,A152;
hence contradiction by A141,A143,A149,A152,A145,A154,A155,A156,XBOOLE_0:3;
end;
thus f.:E3 misses E3
proof
assume not thesis;
then consider x being object such that
A157: x in f.:E3 and
A158: x in E3 by XBOOLE_0:3;
consider Y being set such that
A159: x in Y and
A160: Y in E3c by A158,TARSKI:def 4;
consider c being Element of Class =_f such that
A161: Y = (F.c)`3_3 by A160;
x in (F.c)`1_3 \/ (F.c)`2_3 \/ (F.c)`3_3 by A159,A161,XBOOLE_0:def 3;
then
A162: x in c by A107;
ex x9 being object st x9 in E & c = Class(=_f, x9) by EQREL_1:def 3;
then
A163: c = Class(=_f, x) by A162,EQREL_1:23;
dom f = E by FUNCT_2:def 1;
then
A164: x in dom f \/ rng f by A159,A161,XBOOLE_0:def 3;
consider xx being object such that
A165: xx in dom f and
A166: xx in E3 and
A167: x = f.xx by A157,FUNCT_1:def 6;
consider YY being set such that
A168: xx in YY and
A169: YY in E3c by A166,TARSKI:def 4;
consider cc being Element of Class =_f such that
A170: YY = (F.cc)`3_3 by A169;
xx in (F.cc)`1_3 \/ (F.cc)`2_3 \/ (F.cc)`3_3 by A168,A170,XBOOLE_0:def 3;
then
A171: xx in cc by A107;
ex xx9 being object st xx9 in E & cc = Class(=_f, xx9) by EQREL_1:def 3;
then
A172: cc = Class(=_f, xx) by A171,EQREL_1:23;
iter(f, 1).xx = x by A167,FUNCT_7:70
.= id(field f).x by A164,FUNCT_1:17
.= iter(f, 0).x by FUNCT_7:68;
then [x,xx] in =_f by A159,A161,A168,A170,Def7;
then
A173: Class(=_f, x) = Class(=_f, xx) by A159,A161,EQREL_1:35;
A174: f.xx in f.:YY by A165,A168,FUNCT_1:def 6;
f.:YY misses YY by A107,A170;
hence contradiction by A159,A161,A167,A170,A163,A172,A173,A174,XBOOLE_0:3;
end;
end;
begin :: Addenda
:: from SCMFSA9A, 2006.03.14, A.T.
theorem
for n being Nat holds
n is odd iff ex k being Nat st n = 2*k+1
proof
let n be Nat;
hereby
assume
A1: n is odd;
then consider j being Integer such that
A2: n = 2*j+1 by Th1;
now
assume j < 0;
then
A3: 2*j + 1 <= 2*0 by INT_1:7,XREAL_1:68;
per cases by A3;
suppose
2*j+1 < 0;
hence contradiction by A2;
end;
suppose
2*j+1 = 0;
then n = 2*0;
hence contradiction by A1;
end;
end;
then j in NAT by INT_1:3;
then reconsider j as Nat;
take j;
thus n = 2*j+1 by A2;
end;
thus thesis;
end;
:: missing, 2008.03.20, A.T.
theorem
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)
proof
let A be non empty set, f be Function of A,A, x be Element of A;
thus iter(f,n+1).x = (f*iter(f,n)).x by FUNCT_7:71
.= f.(iter(f,n).x) by FUNCT_2:15;
end;
theorem
for i being Integer holds i is even iff ex j being Integer st i = 2*j by Lm1;
:: from HEYTING3, MOEBIUS1, 2010.02.13, A.T.
registration
cluster odd for Nat;
existence
proof
take 1;
1 = 2*0+1;
hence thesis;
end;
cluster even for Nat;
existence
proof
take 0;
0 = 2*0;
hence thesis;
end;
end;
theorem Th12:
for n being odd Nat holds 1 <= n
proof
let n be odd Nat;
2 * 0 < n;
then 0 + 1 <= n by NAT_1:13;
hence thesis;
end;
registration
cluster odd -> non zero for Integer;
coherence by Th12;
end;