:: Chains on a Grating in Euclidean Space
:: by Freek Wiedijk
::
:: Received January 27, 2003
:: Copyright (c) 2003-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, SUBSET_1, XREAL_0, ARYTM_3, REAL_1, XXREAL_0, CARD_1,
XBOOLE_0, TARSKI, ZFMISC_1, SETFAM_1, XCMPLX_0, FINSEQ_1, FINSET_1,
ABIAN, FUNCT_1, FINSEQ_2, FUNCT_2, RELAT_1, CARD_3, GOBOARD5, MCART_1,
ARYTM_1, TREES_2, POLYNOM1, WAYBEL25, GRAPH_1, NAT_1, ORDERS_2, STRUCT_0,
VECTSP_1, SUPINF_2, BINOP_1, ALGSTR_0, RLVECT_1, GROUP_6, CHAIN_1,
MSSUBFAM;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, ORDINAL1,
XCMPLX_0, XXREAL_0, XREAL_0, FUNCT_1, REAL_1, EUCLID, FUNCT_2, ABIAN,
CARD_1, DOMAIN_1, MOD_4, CARD_3, BINOP_1, VECTSP_1, NAT_1, NUMBERS,
FINSET_1, STRUCT_0, ALGSTR_0, FINSEQ_1, FINSEQ_2, RLVECT_1;
constructors REAL_1, CARD_3, REALSET1, ABIAN, EUCLID, RELSET_1, MOD_4,
BINOP_1;
registrations XBOOLE_0, SUBSET_1, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1,
MEMBERED, FINSEQ_1, ABIAN, STRUCT_0, VECTSP_1, CARD_1, VALUED_0, RELAT_1,
EUCLID, CARD_2, RELSET_1, ORDINAL1;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
definitions TARSKI, FUNCT_1, RLVECT_1, ALGSTR_0, ZFMISC_1, FINSET_1;
equalities SUBSET_1, BINOP_1, STRUCT_0, ALGSTR_0;
expansions TARSKI, SUBSET_1;
theorems TARSKI, ZFMISC_1, FINSEQ_1, SUBSET_1, XBOOLE_0, CARD_1, FINSEQ_2,
FUNCT_2, EUCLID, NAT_1, XBOOLE_1, CARD_2, MCART_1, FUNCT_1, DOMAIN_1,
ENUMSET1, CARD_3, XREAL_0, XREAL_1, XXREAL_0, ORDINAL1, VECTSP_1,
XTUPLE_0;
schemes CLASSES1, FRAENKEL, FUNCT_2, FINSET_1, LMOD_7, BINOP_1;
begin :: stuff I could not find in MML
reserve X,x,y,z for set;
reserve n,m,k,k9,d9 for Nat;
theorem Th1:
for x,y being Real st x < y
ex z being Element of REAL st x < z & z < y
proof
let x,y be Real;
assume x < y;
then consider z being Real such that
A1: x < z and
A2: z < y by XREAL_1:5;
reconsider z as Element of REAL by XREAL_0:def 1;
take z;
thus thesis by A1,A2;
end;
theorem Th2:
for x,y being Real ex z being Element of REAL st x < z & y < z
proof
let x,y be Real;
reconsider x,y as Real;
reconsider z = max(x,y) + 1 as Element of REAL by XREAL_0:def 1;
take z;
A1: x + 0 < z by XREAL_1:8,XXREAL_0:25;
y + 0 < z by XREAL_1:8,XXREAL_0:25;
hence thesis by A1;
end;
scheme FrSet12 { D()->non empty set, A()->non empty set, P[set,set],
F(set,set)->Element of D() } :
{ F(x,y) where x,y is Element of A() : P[x,y] } c= D()
proof
let z be object;
assume z in { F(x,y) where x,y is Element of A() : P[x,y] };
then ex x,y being Element of A() st z = F(x,y) & P[x,y];
hence thesis;
end;
:: Subset A -> Subset B
definition
let B be set;
let A be Subset of B;
redefine func bool A -> Subset-Family of B; :: redefines bool (ZFMISC_1, definition)
coherence by ZFMISC_1:67;
end;
:: non-zero numbers
definition
let d be real Element of NAT;
redefine attr d is zero means :: redefines zero (ORDINAL1, definition)
not d > 0;
compatibility;
end;
definition
let d be Nat;
redefine attr d is zero means :: redefines zero (ORDINAL1, definition)
:Def2:
not d >= 1;
compatibility
proof
d is non zero iff d >= 1 + 0 by NAT_1:13;
hence thesis;
end;
end;
reserve d for non zero Nat;
reserve i,i0,i1 for Element of Seg d;
:: non trivial sets
theorem Th3:
for x,y being object holds {x,y} is trivial iff x = y
proof
let x,y be object;
hereby
A1: x in {x,y} by TARSKI:def 2;
y in {x,y} by TARSKI:def 2;
hence {x,y} is trivial implies x = y by A1;
end;
{x,x} = {x} by ENUMSET1:29;
hence thesis;
end;
registration
cluster non trivial finite for set;
existence
proof
take {0,1};
thus thesis by Th3;
end;
end;
registration
let X be non trivial set;
let Y be set;
cluster X \/ Y -> non trivial;
coherence
proof
consider x,y being object such that
A1: x in X and
A2: y in X and
A3: x <> y by ZFMISC_1:def 10;
take x,y;
thus thesis by A1,A2,A3,XBOOLE_0:def 3;
end;
cluster Y \/ X -> non trivial;
coherence;
end;
registration
let X be non trivial set;
cluster non trivial finite for Subset of X;
existence
proof
consider x,y being object such that
A1: x in X and
A2: y in X and
A3: x <> y by ZFMISC_1:def 10;
take {x,y};
thus thesis by A1,A2,A3,Th3,ZFMISC_1:32;
end;
end;
theorem Th4:
X is trivial & X \/ {y} is non trivial implies
ex x being object st X = {x}
proof
assume that
A1: X is trivial and
A2: X \/ {y} is non trivial;
X is empty or ex x being object st X = {x} by A1,ZFMISC_1:131;
hence thesis by A2;
end;
scheme NonEmptyFinite
{ X()->non empty set, A()->non empty finite Subset of X(), P[set] } : P[A()]
provided
A1: for x being Element of X() st x in A() holds P[{x}] and
A2: for x being Element of X(), B being non empty finite Subset of X()
st x in A() & B c= A() & not x in B & P[B] holds P[B \/ {x}]
proof
defpred Q[set] means $1 is empty or P[$1];
A3: A() is finite;
A4: Q[{}];
A5: for x,B being set st x in A() & B c= A() & Q[B] holds Q[B \/ {x}]
proof
let x,B be set;
assume that
A6: x in A() and
A7: B c= A() and
A8: Q[B];
reconsider B as Subset of X() by A7,XBOOLE_1:1;
per cases;
suppose x in B;
then {x} c= B by ZFMISC_1:31;
hence thesis by A8,XBOOLE_1:12;
end;
suppose
B is non empty & not x in B;
hence thesis by A2,A6,A7,A8;
end;
suppose B is empty;
hence thesis by A1,A6;
end;
end;
Q[A()] from FINSET_1:sch 2(A3,A4,A5);
hence thesis;
end;
scheme NonTrivialFinite
{ X()->non trivial set, A()->non trivial finite Subset of X(), P[set] } :
P[A()]
provided
A1: for x,y being Element of X() st x in A() & y in A() & x <> y
holds P[{x,y}] and
A2: for x being Element of X(), B being non trivial finite Subset of X()
st x in A() & B c= A() & not x in B & P[B] holds P[B \/ {x}]
proof
defpred Q[set] means $1 is trivial or P[$1];
A3: A() is finite;
A4: Q[{}];
A5: for x,B being set st x in A() & B c= A() & Q[B] holds Q[B \/ {x}]
proof
let x,B be set;
assume that
A6: x in A() and
A7: B c= A() and
A8: Q[B];
reconsider B as Subset of X() by A7,XBOOLE_1:1;
per cases;
suppose B \/ {x} is trivial;
hence thesis;
end;
suppose x in B;
then {x} c= B by ZFMISC_1:31;
hence thesis by A8,XBOOLE_1:12;
end;
suppose
B is non trivial & not x in B;
hence thesis by A2,A6,A7,A8;
end;
suppose
A9: B is trivial & B \/ {x} is non trivial;
then consider y being object such that
A10: B = {y} by Th4;
A11: x <> y by A9,A10;
A12: B \/ {x} = {x,y} by A10,ENUMSET1:1;
y in B by A10,TARSKI:def 1;
hence thesis by A1,A6,A7,A11,A12;
end;
end;
Q[A()] from FINSET_1:sch 2(A3,A4,A5);
hence thesis;
end;
:: sets of cardinality 2
theorem Th5:
card X = 2 iff
ex x,y st x in X & y in X & x <> y & for z st z in X holds z = x or z = y
proof
hereby
assume
A1: card X = 2;
then reconsider X9 = X as finite set;
consider x,y being object such that
A2: x <> y and
A3: X9 = {x,y} by A1,CARD_2:60;
reconsider x,y as set by TARSKI:1;
take x,y;
thus x in X & y in X & x <> y &
for z st z in X holds z = x or z = y by A2,A3,TARSKI:def 2;
end;
given x,y such that
A4: x in X and
A5: y in X and
A6: x <> y and
A7: for z st z in X holds z = x or z = y;
for z be object holds z in X iff z = x or z = y by A4,A5,A7;
then X = {x,y} by TARSKI:def 2;
hence thesis by A6,CARD_2:57;
end;
::$CT
theorem Th6:
for X,Y being finite set st X misses Y holds
(card X is even iff card Y is even) iff card(X \/ Y) is even
proof
let X,Y be finite set;
assume X misses Y;
then card(X \/ Y) = card X + card Y by CARD_2:40;
hence thesis;
end;
theorem Th7:
for X,Y being finite set holds
(card X is even iff card Y is even) iff card(X \+\ Y) is even
proof
let X,Y be finite set;
A1: X \ Y misses X /\ Y by XBOOLE_1:89;
A2: X = (X \ Y) \/ (X /\ Y) by XBOOLE_1:51;
A3: Y \ X misses X /\ Y by XBOOLE_1:89;
A4: Y = (Y \ X) \/ (X /\ Y) by XBOOLE_1:51;
A5: X \ Y misses Y \ X by XBOOLE_1:82;
A6: X \+\ Y = (X \ Y) \/ (Y \ X) by XBOOLE_0:def 6;
A7: (card(X \ Y) is even iff card(X /\ Y) is even) iff card X is even by A1,A2
,Th6;
(card(Y \ X) is even iff card(X /\ Y) is even) iff card Y is even by A3,A4
,Th6;
hence thesis by A5,A6,A7,Th6;
end;
:: elements of REAL d as functions to REAL
definition
let n;
redefine func REAL n means :: redefines REAL (EUCLID, definition)
:Def3:
for x being object holds x in it iff x is Function of Seg n,REAL;
compatibility
proof
A1: for x holds x in REAL n iff x is Function of Seg n,REAL
proof
let x;
hereby
assume x in REAL n;
then x in n-tuples_on REAL by EUCLID:def 1;
then x in Funcs(Seg n,REAL) by FINSEQ_2:93;
hence x is Function of Seg n,REAL by FUNCT_2:66;
end;
assume x is Function of Seg n,REAL;
then x in Funcs(Seg n,REAL) by FUNCT_2:8;
then x in n-tuples_on REAL by FINSEQ_2:93;
hence thesis by EUCLID:def 1;
end;
let X be FinSequenceSet of REAL;
thus
X = REAL n implies
for x being object holds x in X iff x is Function of Seg n,REAL
by A1;
assume
A2: for x being object holds x in X iff x is Function of Seg n,REAL;
now
let x be object;
x in X iff x is Function of Seg n,REAL by A2;
hence x in X iff x in REAL n by A1;
end;
hence thesis by TARSKI:2;
end;
end;
reserve l,r,l9,r9,l99,r99,x,x9,l1,r1,l2,r2 for Element of REAL d;
reserve Gi for non trivial finite Subset of REAL;
reserve li,ri,li9,ri9,xi,xi9 for Real;
begin :: gratings, cells, chains, cycles
:: gratings
definition
let d;
mode Grating of d -> Function of Seg d,bool REAL means
:Def4:
for i holds it.i is non trivial finite;
existence
proof
defpred P[object,object] means $2 is non trivial finite Subset of REAL;
A1: for i being object st i in Seg d ex X being object st P[i,X]
proof
let i being object;
assume i in Seg d;
set X = the non trivial finite Subset of REAL;
take X;
thus thesis;
end;
consider G being Function such that
A2: dom G = Seg d &
for i being object st i in Seg d holds P[i,G.i] from CLASSES1:sch 1(A1);
for i being object st i in Seg d holds G.i in bool REAL
proof
let i be object;
assume i in Seg d;
then G.i is Subset of REAL by A2;
hence thesis;
end;
then reconsider G as Function of Seg d,bool REAL by A2,FUNCT_2:3;
take G;
thus thesis by A2;
end;
end;
reserve G for Grating of d;
registration
let d;
cluster -> finite-yielding for Grating of d;
coherence
proof let G;
let i be object;
assume i in Seg d;
hence G.i is finite by Def4;
end;
end;
definition
let d,G,i;
redefine func G.i -> non trivial finite Subset of REAL; :: redefines . (FUNCT_1, definition)
coherence by Def4;
end;
theorem Th8:
x in product G iff for i holds x.i in G.i
proof
x is Function of Seg d,REAL by Def3;
then
A1: dom x = Seg d by FUNCT_2:def 1;
A2: dom G = Seg d by FUNCT_2:def 1;
hence x in product G implies for i holds x.i in G.i by CARD_3:9;
assume for i holds x.i in G.i;
then for i being object st i in Seg d holds x.i in G.i;
hence thesis by A1,A2,CARD_3:9;
end;
:: gaps
::$CT
theorem Th9:
for X being non empty finite Subset of REAL holds
ex ri being Element of REAL st ri in X & for xi st xi in X holds ri >= xi
proof
defpred P[set] means
ex ri being Element of REAL st ri in $1 &
for xi st xi in $1 holds ri >= xi;
let X be non empty finite Subset of REAL;
A1: for xi being Element of REAL st xi in X holds P[{xi}]
proof
let xi be Element of REAL;
assume xi in X;
take xi;
thus thesis by TARSKI:def 1;
end;
A2: for x being Element of REAL, B being non empty finite Subset of REAL st
x in X & B c= X & not x in B & P[B] holds P[B \/ {x}]
proof
let x be Element of REAL;
let B be non empty finite Subset of REAL;
assume that x in X and B c= X
and not x in B and
A3: P[B];
consider ri such that
A4: ri in B and
A5: for xi st xi in B holds ri >= xi by A3;
set B9 = B \/ {x};
A6: now
let xi;
xi in {x} iff xi = x by TARSKI:def 1;
hence xi in B9 iff xi in B or xi = x by XBOOLE_0:def 3;
end;
per cases;
suppose
A7: x <= ri;
reconsider ri as Element of REAL by XREAL_0:def 1;
take ri;
thus ri in B9 by A4,A6;
let xi;
assume xi in B9;
then xi in B or xi = x by A6;
hence thesis by A5,A7;
end;
suppose
A8: ri < x;
take x;
thus x in B9 by A6;
let xi;
assume xi in B9;
then xi in B or xi = x by A6;
then ri >= xi or xi = x by A5;
hence thesis by A8,XXREAL_0:2;
end;
end;
thus P[X] from NonEmptyFinite(A1,A2);
end;
theorem Th10:
for X being non empty finite Subset of REAL holds
ex li being Element of REAL st li in X & for xi st xi in X holds li <= xi
proof
defpred P[set] means
ex li being Element of REAL st li in $1 & for xi st xi in $1 holds li <= xi;
let X be non empty finite Subset of REAL;
A1: for xi being Element of REAL st xi in X holds P[{xi}]
proof
let xi be Element of REAL;
assume xi in X;
take xi;
thus thesis by TARSKI:def 1;
end;
A2: for x being Element of REAL, B being non empty finite Subset of REAL st
x in X & B c= X & not x in B & P[B] holds P[B \/ {x}]
proof
let x be Element of REAL;
let B be non empty finite Subset of REAL;
assume that x in X and B c= X
and not x in B and
A3: P[B];
consider li such that
A4: li in B and
A5: for xi st xi in B holds li <= xi by A3;
set B9 = B \/ {x};
A6: now
let xi;
xi in {x} iff xi = x by TARSKI:def 1;
hence xi in B9 iff xi in B or xi = x by XBOOLE_0:def 3;
end;
per cases;
suppose
A7: li <= x;
reconsider li as Element of REAL by XREAL_0:def 1;
take li;
thus li in B9 by A4,A6;
let xi;
assume xi in B9;
then xi in B or xi = x by A6;
hence thesis by A5,A7;
end;
suppose
A8: x < li;
take x;
thus x in B9 by A6;
let xi;
assume xi in B9;
then xi in B or xi = x by A6;
then li <= xi or xi = x by A5;
hence thesis by A8,XXREAL_0:2;
end;
end;
thus P[X] from NonEmptyFinite(A1,A2);
end;
theorem Th11:
ex li,ri st li in Gi & ri in Gi &
li < ri & for xi st xi in Gi holds not (li < xi & xi < ri)
proof
defpred P[set] means ex li,ri st li in $1 & ri in $1 &
li < ri & for xi st xi in $1 holds not (li < xi & xi < ri);
A1: now
let li,ri be Element of REAL;
assume that
li in Gi and ri in Gi and
A2: li <> ri;
A3: now
let li,ri;
assume
A4: li < ri;
thus P[{li,ri}]
proof
take li,ri;
thus thesis by A4,TARSKI:def 2;
end;
end;
li < ri or ri < li by A2,XXREAL_0:1;
hence P[{li,ri}] by A3;
end;
A5: for x being Element of REAL, B being non trivial finite Subset of REAL
st x in Gi & B c= Gi & not x in B & P[B] holds P[B \/ {x}]
proof
let x be Element of REAL;
let B be non trivial finite Subset of REAL;
assume that
x in Gi and B c= Gi and
A6: not x in B and
A7: P[B];
consider li,ri such that
A8: li in B and
A9: ri in B and
A10: li < ri and
A11: for xi st xi in B holds not (li < xi & xi < ri) by A7;
per cases by A6,A8,A9,XXREAL_0:1;
suppose
A12: x < li;
take li,ri;
thus li in B \/ {x} & ri in B \/ {x} & li < ri by A8,A9,A10,
XBOOLE_0:def 3;
let xi;
assume xi in B \/ {x};
then xi in B or xi in {x} by XBOOLE_0:def 3;
hence thesis by A11,A12,TARSKI:def 1;
end;
suppose
A13: li < x & x < ri;
take li,x;
x in {x} by TARSKI:def 1;
hence li in B \/ {x} & x in B \/ {x} & li < x by A8,A13,XBOOLE_0:def 3;
let xi;
assume xi in B \/ {x};
then xi in B or xi in {x} by XBOOLE_0:def 3;
then not (li < xi & xi < ri) or xi = x by A11,TARSKI:def 1;
hence thesis by A13,XXREAL_0:2;
end;
suppose
A14: ri < x;
take li,ri;
thus li in B \/ {x} & ri in B \/ {x} & li < ri by A8,A9,A10,
XBOOLE_0:def 3;
let xi;
assume xi in B \/ {x};
then xi in B or xi in {x} by XBOOLE_0:def 3;
hence thesis by A11,A14,TARSKI:def 1;
end;
end;
thus P[Gi] from NonTrivialFinite(A1,A5);
end;
::$CT
theorem
ex li,ri st li in Gi & ri in Gi &
ri < li & for xi st xi in Gi holds not (xi < ri or li < xi)
proof
consider li being Element of REAL such that
A1: li in Gi and
A2: for xi st xi in Gi holds li >= xi by Th9;
consider ri being Element of REAL such that
A3: ri in Gi and
A4: for xi st xi in Gi holds ri <= xi by Th10;
take li,ri;
A5: ri <= li by A2,A3;
now
assume
A6: li = ri;
consider x1,x2 be object such that
A7: x1 in Gi and
A8: x2 in Gi and
A9: x1 <> x2 by ZFMISC_1:def 10;
reconsider x1,x2 as Element of REAL by A7,A8;
A10: ri <= x1 by A4,A7;
A11: x1 <= li by A2,A7;
A12: ri <= x2 by A4,A8;
A13: x2 <= li by A2,A8;
x1 = li by A6,A10,A11,XXREAL_0:1;
hence contradiction by A6,A9,A12,A13,XXREAL_0:1;
end;
hence thesis by A1,A2,A3,A4,A5,XXREAL_0:1;
end;
definition
let Gi;
mode Gap of Gi -> Element of [:REAL,REAL:] means
:Def5:
ex li,ri st it = [li,ri] & li in Gi & ri in Gi &
((li < ri & for xi st xi in Gi holds not (li < xi & xi < ri)) or
(ri < li & for xi st xi in Gi holds not (li < xi or xi < ri)));
existence
proof
consider li,ri such that
A1: li in Gi and
A2: ri in Gi and
A3: li < ri and
A4: for xi st xi in Gi holds not (li < xi & xi < ri) by Th11;
reconsider ri, li as Element of REAL by XREAL_0:def 1;
take [li,ri],li,ri;
thus thesis by A1,A2,A3,A4;
end;
end;
theorem Th13:
[li,ri] is Gap of Gi iff li in Gi & ri in Gi &
((li < ri & for xi st xi in Gi holds not (li < xi & xi < ri)) or
(ri < li & for xi st xi in Gi holds not (li < xi or xi < ri)))
proof
thus [li,ri] is Gap of Gi implies li in Gi & ri in Gi &
((li < ri & for xi st xi in Gi holds not (li < xi & xi < ri)) or
(ri < li & for xi st xi in Gi holds not (li < xi or xi < ri)))
proof
assume [li,ri] is Gap of Gi;
then consider li9,ri9 such that
A1: [li,ri] = [li9,ri9] and
A2: li9 in Gi and
A3: ri9 in Gi and
A4: (li9 < ri9 & for xi st xi in Gi holds not (li9 < xi & xi < ri9)) or
(ri9 < li9 & for xi st xi in Gi holds not (li9 < xi or xi < ri9))
by Def5;
A5: li9 = li by A1,XTUPLE_0:1;
ri9 = ri by A1,XTUPLE_0:1;
hence thesis by A2,A3,A4,A5;
end;
li in REAL & ri in REAL by XREAL_0:def 1;
then [li,ri] in [:REAL,REAL:] by ZFMISC_1:87;
hence thesis by Def5;
end;
theorem
Gi = {li,ri} implies
([li9,ri9] is Gap of Gi iff li9 = li & ri9 = ri or li9 = ri & ri9 = li)
proof
assume
A1: Gi = {li,ri};
hereby
assume
A2: [li9,ri9] is Gap of Gi;
then
A3: li9 in Gi by Th13;
A4: ri9 in Gi by A2,Th13;
A5: li9 = li or li9 = ri by A1,A3,TARSKI:def 2;
li9 <> ri9 by A2,Th13;
hence li9 = li & ri9 = ri or li9 = ri & ri9 = li by A1,A4,A5,TARSKI:def 2;
end;
assume
A6: li9 = li & ri9 = ri or li9 = ri & ri9 = li;
li9 in REAL & ri9 in REAL by XREAL_0:def 1;
then [li9,ri9] in [:REAL,REAL:] by ZFMISC_1:87;
then reconsider liri = [li9,ri9] as Element of [:REAL,REAL:];
liri is Gap of Gi
proof
take li9,ri9;
li <> ri by A1,Th3;
hence thesis by A1,TARSKI:def 2,XXREAL_0:1,A6;
end;
hence thesis;
end;
deffunc f(set) = $1;
theorem Th15:
xi in Gi implies ex ri being Element of REAL st [xi,ri] is Gap of Gi
proof
assume
A1: xi in Gi;
defpred P[Element of REAL] means $1 > xi;
set Gi9 = { f(ri9) where ri9 is Element of REAL : f(ri9) in Gi & P[ri9]};
A2: Gi9 c= Gi from FRAENKEL:sch 17;
then reconsider Gi9 as finite Subset of REAL by XBOOLE_1:1;
per cases;
suppose
A3: Gi9 is empty;
A4: now
let xi9;
assume that
A5: xi9 in Gi and
A6: xi9 > xi;
xi9 in Gi9 by A5,A6;
hence contradiction by A3;
end;
consider li being Element of REAL such that
A7: li in Gi and
A8: for xi9 st xi9 in Gi holds li <= xi9 by Th10;
take li;
A9: now
assume
A10: li = xi;
for xi9 being object holds xi9 in Gi iff xi9 = xi
proof
let xi9 be object;
hereby
assume
A11: xi9 in Gi;
then reconsider xi99 = xi9 as Element of REAL;
A12: li <= xi99 by A8,A11;
xi99 <= xi by A4,A11;
hence xi9 = xi by A10,A12,XXREAL_0:1;
end;
thus thesis by A1;
end;
hence Gi = {xi} by TARSKI:def 1;
hence contradiction;
end;
li <= xi by A1,A8;
then
A13: li < xi by A9,XXREAL_0:1;
for xi9 st xi9 in Gi holds not (xi < xi9 or xi9 < li) by A4,A8;
hence thesis by A1,A7,A13,Th13;
end;
suppose Gi9 is non empty;
then reconsider Gi9 as non empty finite Subset of REAL;
consider ri being Element of REAL such that
A14: ri in Gi9 and
A15: for ri9 st ri9 in Gi9 holds ri9 >= ri by Th10;
take ri;
now
thus xi in Gi by A1;
thus ri in Gi by A2,A14;
ex ri9 being Element of REAL st ri9 = ri & ri9 in Gi & xi < ri9 by A14;
hence xi < ri;
hereby
let xi9;
assume xi9 in Gi;
then xi9 <= xi or xi9 in Gi9;
hence not (xi < xi9 & xi9 < ri) by A15;
end;
end;
hence thesis by Th13;
end;
end;
theorem Th16:
xi in Gi implies ex li being Element of REAL st [li,xi] is Gap of Gi
proof
assume
A1: xi in Gi;
defpred P[Element of REAL] means $1 < xi;
set Gi9 = { f(li9) where li9 is Element of REAL : f(li9) in Gi & P[li9]};
A2: Gi9 c= Gi from FRAENKEL:sch 17;
then reconsider Gi9 as finite Subset of REAL by XBOOLE_1:1;
per cases;
suppose
A3: Gi9 is empty;
A4: now
let xi9;
assume that
A5: xi9 in Gi and
A6: xi9 < xi;
xi9 in Gi9 by A5,A6;
hence contradiction by A3;
end;
consider ri being Element of REAL such that
A7: ri in Gi and
A8: for xi9 st xi9 in Gi holds ri >= xi9 by Th9;
take ri;
A9: now
assume
A10: ri = xi;
for xi9 being object holds xi9 in Gi iff xi9 = xi
proof
let xi9 be object;
hereby
assume
A11: xi9 in Gi;
then reconsider xi99 = xi9 as Element of REAL;
A12: ri >= xi99 by A8,A11;
xi99 >= xi by A4,A11;
hence xi9 = xi by A10,A12,XXREAL_0:1;
end;
thus thesis by A1;
end;
hence Gi = {xi} by TARSKI:def 1;
hence contradiction;
end;
ri >= xi by A1,A8;
then
A13: ri > xi by A9,XXREAL_0:1;
for xi9 st xi9 in Gi holds not (xi9 > ri or xi > xi9) by A4,A8;
hence thesis by A1,A7,A13,Th13;
end;
suppose Gi9 is non empty;
then reconsider Gi9 as non empty finite Subset of REAL;
consider li being Element of REAL such that
A14: li in Gi9 and
A15: for li9 st li9 in Gi9 holds li9 <= li by Th9;
take li;
now
thus xi in Gi by A1;
thus li in Gi by A2,A14;
ex li9 being Element of REAL st li9 = li & li9 in Gi & xi > li9 by A14;
hence xi > li;
hereby
let xi9;
assume xi9 in Gi;
then xi9 >= xi or xi9 in Gi9;
hence not (xi9 > li & xi > xi9) by A15;
end;
end;
hence thesis by Th13;
end;
end;
theorem Th17:
[li,ri] is Gap of Gi & [li,ri9] is Gap of Gi implies ri = ri9
proof
A1: ri <= ri9 & ri9 <= ri implies ri = ri9 by XXREAL_0:1;
assume that
A2: [li,ri] is Gap of Gi and
A3: [li,ri9] is Gap of Gi;
A4: ri in Gi by A2,Th13;
A5: ri9 in Gi by A3,Th13;
per cases by A2,Th13;
suppose
A6: li < ri & for xi st xi in Gi holds not (li < xi & xi < ri);
ri9 <= li or li < ri9 & ri9 < ri or ri <= ri9;
hence thesis by A1,A3,A4,A5,A6,Th13;
end;
suppose
A7: ri < li & for xi st xi in Gi holds not (li < xi or xi < ri);
ri9 < ri or ri <= ri9 & ri9 <= li or li < ri9;
hence thesis by A1,A3,A4,A5,A7,Th13;
end;
end;
theorem Th18:
[li,ri] is Gap of Gi & [li9,ri] is Gap of Gi implies li = li9
proof
A1: li <= li9 & li9 <= li implies li = li9 by XXREAL_0:1;
assume that
A2: [li,ri] is Gap of Gi and
A3: [li9,ri] is Gap of Gi;
A4: li in Gi by A2,Th13;
A5: li9 in Gi by A3,Th13;
per cases by A2,Th13;
suppose
A6: li < ri & for xi st xi in Gi holds not (li < xi & xi < ri);
li9 <= li or li < li9 & li9 < ri or ri <= li9;
hence thesis by A1,A3,A4,A5,A6,Th13;
end;
suppose
A7: ri < li & for xi st xi in Gi holds not (li < xi or xi < ri);
li9 < ri or ri <= li9 & li9 <= li or li < li9;
hence thesis by A1,A3,A4,A5,A7,Th13;
end;
end;
theorem Th19:
ri < li & [li,ri] is Gap of Gi & ri9 < li9 & [li9,ri9] is Gap of Gi implies
li = li9 & ri = ri9
proof
assume that
A1: ri < li and
A2: [li,ri] is Gap of Gi and
A3: ri9 < li9 and
A4: [li9,ri9] is Gap of Gi;
A5: li in Gi by A2,Th13;
A6: ri in Gi by A2,Th13;
A7: li9 in Gi by A4,Th13;
A8: ri9 in Gi by A4,Th13;
hereby
assume li <> li9;
then li < li9 or li9 < li by XXREAL_0:1;
hence contradiction by A1,A2,A3,A4,A5,A7,Th13;
end;
hereby
assume ri <> ri9;
then ri < ri9 or ri9 < ri by XXREAL_0:1;
hence contradiction by A1,A2,A3,A4,A6,A8,Th13;
end;
end;
:: cells, chains
definition
let d,l,r;
func cell(l,r) -> non empty Subset of REAL d equals
{ x : (for i holds l.i <= x.i & x.i <= r.i) or
(ex i st r.i < l.i & (x.i <= r.i or l.i <= x.i)) };
coherence
proof
defpred P[Element of REAL d] means
(for i holds l.i <= $1.i & $1.i <= r.i) or
(ex i st r.i < l.i & ($1.i <= r.i or l.i <= $1.i));
set CELL = { x : P[x] };
P[l];
then
A1: l in CELL;
CELL c= REAL d from FRAENKEL:sch 10;
hence thesis by A1;
end;
end;
theorem Th20:
x in cell(l,r) iff ((for i holds l.i <= x.i & x.i <= r.i) or
ex i st r.i < l.i & (x.i <= r.i or l.i <= x.i) )
proof
defpred P[Element of REAL d] means (for i holds l.i <= $1.i & $1.i <= r.i) or
(ex i st r.i < l.i & ($1.i <= r.i or l.i <= $1.i));
A1: cell(l,r) = { x9 : P[x9] };
thus x in cell(l,r) iff P[x] from LMOD_7:sch 7(A1);
end;
theorem Th21:
(for i holds l.i <= r.i) implies
(x in cell(l,r) iff for i holds l.i <= x.i & x.i <= r.i)
proof
assume
A1: for i holds l.i <= r.i;
hereby
assume x in cell(l,r);
then (for i holds l.i <= x.i & x.i <= r.i) or
ex i st r.i < l.i & (x.i <= r.i or l.i <= x.i) by Th20;
hence for i holds l.i <= x.i & x.i <= r.i by A1;
end;
thus thesis;
end;
theorem Th22:
(ex i st r.i < l.i) implies
(x in cell(l,r) iff ex i st r.i < l.i & (x.i <= r.i or l.i <= x.i))
proof
given i0 such that
A1: r.i0 < l.i0;
x.i0 < l.i0 or r.i0 < x.i0 by A1,XXREAL_0:2;
hence
x in cell(l,r) implies ex i st r.i < l.i & (x.i <= r.i or l.i <= x.i)
by Th20;
thus thesis;
end;
theorem Th23:
l in cell(l,r) & r in cell(l,r)
proof
A1: (for i holds l.i <= l.i & l.i <= r.i) or ex i st r.i < l.i & (l.i <= r
.i or l.i <= l.i);
(for i holds l.i <= r.i & r.i <= r.i) or ex i st r.i < l.i & (r.i <= r
.i or l.i <= r.i);
hence thesis by A1;
end;
theorem Th24:
cell(x,x) = {x}
proof
for x9 being object holds x9 in cell(x,x) iff x9 = x
proof
let x9 be object;
thus x9 in cell(x,x) implies x9 = x
proof
assume
A1: x9 in cell(x,x);
then reconsider x,x9 as Function of Seg d,REAL by Def3;
now
let i;
A2: for i holds x.i <= x.i;
then
A3: x.i <= x9.i by A1,Th21;
x9.i <= x.i by A1,A2,Th21;
hence x9.i = x.i by A3,XXREAL_0:1;
end;
hence thesis by FUNCT_2:63;
end;
thus thesis by Th23;
end;
hence thesis by TARSKI:def 1;
end;
theorem Th25:
(for i holds l9.i <= r9.i) implies (cell(l,r) c= cell(l9,r9) iff
for i holds l9.i <= l.i & l.i <= r.i & r.i <= r9.i)
proof
assume
A1: for i holds l9.i <= r9.i;
thus cell(l,r) c= cell(l9,r9) implies
for i holds l9.i <= l.i & l.i <= r.i & r.i <= r9.i
proof
assume
A2: cell(l,r) c= cell(l9,r9);
let i0;
per cases;
suppose
A3: r.i0 < l.i0;
defpred P[Element of Seg d,Element of REAL] means $2 > l.$1 & $2 > r9.$1;
A4: for i ex xi being Element of REAL st P[i,xi] by Th2;
consider x being Function of Seg d,REAL such that
A5: for i holds P[i,x.i] from FUNCT_2:sch 3(A4);
reconsider x as Element of REAL d by Def3;
ex i st r.i < l.i & (x.i <= r.i or l.i <= x.i)
proof
take i0;
thus thesis by A3,A5;
end;
then
A6: x in cell(l,r);
ex i st x.i < l9.i or r9.i < x.i
proof
take i0;
thus thesis by A5;
end;
hence thesis by A1,A2,A6,Th21;
end;
suppose
A7: l.i0 <= r.i0;
A8: l in cell(l,r) by Th23;
r in cell(l,r) by Th23;
hence thesis by A1,A2,A7,A8,Th21;
end;
end;
assume
A9: for i holds l9.i <= l.i & l.i <= r.i & r.i <= r9.i;
let x be object;
assume
A10: x in cell(l,r);
then reconsider x as Element of REAL d;
now
let i;
A11: l9.i <= l.i by A9;
A12: l.i <= x.i by A9,A10,Th21;
A13: x.i <= r.i by A9,A10,Th21;
r.i <= r9.i by A9;
hence l9.i <= x.i & x.i <= r9.i by A11,A12,A13,XXREAL_0:2;
hence l9.i <= r9.i by XXREAL_0:2;
end;
hence thesis;
end;
theorem Th26:
(for i holds r.i < l.i) implies (cell(l,r) c= cell(l9,r9) iff
for i holds r.i <= r9.i & r9.i < l9.i & l9.i <= l.i)
proof
assume
A1: for i holds r.i < l.i;
thus cell(l,r) c= cell(l9,r9) implies
for i holds r.i <= r9.i & r9.i < l9.i & l9.i <= l.i
proof
assume
A2: cell(l,r) c= cell(l9,r9);
A3: for i holds r9.i < l9.i
proof
let i0;
assume
A4: l9.i0 <= r9.i0;
defpred P[Element of Seg d,Element of REAL] means
($1 = i0 implies l.$1 < $2 & r9.$1 < $2) &
(r9.$1 < l9.$1 implies r9.$1 < $2 & $2 < l9.$1);
A5: for i ex xi being Element of REAL st P[i,xi]
proof
let i;
per cases;
suppose i = i0 & r9.i < l9.i;
hence thesis by A4;
end;
suppose
A6: i <> i0;
r9.i < l9.i implies
ex xi being Element of REAL st r9.i < xi & xi < l9.i by Th1;
hence thesis by A6;
end;
suppose
A7: l9.i <= r9.i;
ex xi being Element of REAL st l.i < xi & r9.i < xi by Th2;
hence thesis by A7;
end;
end;
consider x being Function of Seg d,REAL such that
A8: for i holds P[i,x.i] from FUNCT_2:sch 3(A5);
reconsider x as Element of REAL d by Def3;
A9: r.i0 < l.i0 by A1;
x.i0 <= r.i0 or l.i0 <= x.i0 by A8;
then
A10: x in cell(l,r) by A9;
per cases by A2,A10,Th20;
suppose for i holds l9.i <= x.i & x.i <= r9.i;
then x.i0 <= r9.i0;
hence contradiction by A8;
end;
suppose ex i st r9.i < l9.i & (x.i <= r9.i or l9.i <= x.i);
hence contradiction by A8;
end;
end;
let i0;
hereby
assume
A11: r9.i0 < r.i0;
defpred P[Element of Seg d,Element of REAL] means
r9.$1 < $2 & $2 < l9.$1 & ($1 = i0 implies $2 < r.$1);
A12: for i ex xi being Element of REAL st P[i,xi]
proof
let i;
per cases;
suppose
A13: i = i0 & l9.i <= r.i;
r9.i < l9.i by A3;
then consider xi being Element of REAL such that
A14: r9.i < xi and
A15: xi < l9.i by Th1;
xi < r.i by A13,A15,XXREAL_0:2;
hence thesis by A14,A15;
end;
suppose
A16: i = i0 & r.i <= l9.i;
then consider xi being Element of REAL such that
A17: r9.i < xi and
A18: xi < r.i by A11,Th1;
xi < l9.i by A16,A18,XXREAL_0:2;
hence thesis by A17,A18;
end;
suppose
A19: i <> i0;
r9.i < l9.i by A3;
then ex xi being Element of REAL st ( r9.i < xi)&( xi < l9.i) by Th1;
hence thesis by A19;
end;
end;
consider x being Function of Seg d,REAL such that
A20: for i holds P[i,x.i] from FUNCT_2:sch 3(A12);
reconsider x as Element of REAL d by Def3;
A21: r.i0 < l.i0 by A1;
x.i0 <= r.i0 or l.i0 <= x.i0 by A20;
then
A22: x in cell(l,r) by A21;
not (l9.i0 <= x.i0 & x.i0 <= r9.i0) by A3,XXREAL_0:2;
then ex i st r9.i < l9.i & (x.i <= r9.i or l9.i <= x.i) by A2,A22,Th20;
hence contradiction by A20;
end;
thus r9.i0 < l9.i0 by A3;
hereby
assume
A23: l9.i0 > l.i0;
defpred R[Element of Seg d,Element of REAL] means
l9.$1 > $2 & $2 > r9.$1 & ($1 = i0 implies $2 > l.$1);
A24: for i ex xi being Element of REAL st R[i,xi]
proof
let i;
per cases;
suppose
A25: i = i0 & r9.i >= l.i;
l9.i > r9.i by A3;
then consider xi being Element of REAL such that
A26: r9.i < xi and
A27: xi < l9.i by Th1;
xi > l.i by A25,A26,XXREAL_0:2;
hence thesis by A26,A27;
end;
suppose
A28: i = i0 & l.i >= r9.i;
then consider xi being Element of REAL such that
A29: l.i < xi and
A30: xi < l9.i by A23,Th1;
xi > r9.i by A28,A29,XXREAL_0:2;
hence thesis by A29,A30;
end;
suppose
A31: i <> i0;
l9.i > r9.i by A3;
then ex xi being Element of REAL st ( r9.i < xi)&( xi < l9.i) by Th1;
hence thesis by A31;
end;
end;
consider x being Function of Seg d,REAL such that
A32: for i holds R[i,x.i] from FUNCT_2:sch 3(A24);
reconsider x as Element of REAL d by Def3;
A33: l.i0 > r.i0 by A1;
x.i0 >= l.i0 or r.i0 >= x.i0 by A32;
then
A34: x in cell(l,r) by A33;
not (r9.i0 >= x.i0 & x.i0 >= l9.i0) by A3,XXREAL_0:2;
then ex i st l9.i > r9.i & (x.i <= r9.i or l9.i <= x.i) by A2,A34,Th20;
hence contradiction by A32;
end;
end;
assume
A35: for i holds r.i <= r9.i & r9.i < l9.i & l9.i <= l.i;
let x be object;
assume
A36: x in cell(l,r);
then reconsider x as Element of REAL d;
set i0 = the Element of Seg d;
A37: r.i0 <= r9.i0 by A35;
r9.i0 < l9.i0 by A35;
then
A38: r.i0 < l9.i0 by A37,XXREAL_0:2;
l9.i0 <= l.i0 by A35;
then r.i0 < l.i0 by A38,XXREAL_0:2;
then x.i0 < l.i0 or r.i0 < x.i0 by XXREAL_0:2;
then consider i such that
r.i < l.i and
A39: x.i <= r.i or l.i <= x.i by A36,Th20;
A40: r.i <= r9.i by A35;
A41: l9.i <= l.i by A35;
A42: r9.i < l9.i by A35;
x.i <= r9.i or l9.i <= x.i by A39,A40,A41,XXREAL_0:2;
hence thesis by A42;
end;
theorem Th27:
(for i holds l.i <= r.i) & (for i holds r9.i < l9.i) implies
(cell(l,r) c= cell(l9,r9) iff ex i st r.i <= r9.i or l9.i <= l.i)
proof
assume
A1: for i holds l.i <= r.i;
assume
A2: for i holds r9.i < l9.i;
thus
cell(l,r) c= cell(l9,r9) implies ex i st r.i <= r9.i or l9.i <= l.i
proof
assume
A3: cell(l,r) c= cell(l9,r9);
assume
A4: for i holds r9.i < r.i & l.i < l9.i;
defpred P[Element of Seg d,Element of REAL] means
l.$1 <= $2 & $2 <= r.$1 & r9.$1 < $2 & $2 < l9.$1;
A5: for i ex xi being Element of REAL st P[i,xi]
proof
let i;
per cases;
suppose
A6: l.i <= r9.i & l9.i <= r.i;
r9.i < l9.i by A2;
then consider xi being Element of REAL such that
A7: r9.i < xi and
A8: xi < l9.i by Th1;
take xi;
thus thesis by A6,A7,A8,XXREAL_0:2;
end;
suppose
A9: r9.i < l.i & l9.i <= r.i;
reconsider li = l.i as Element of REAL by XREAL_0:def 1;
take li;
thus thesis by A1,A4,A9;
end;
suppose
A10: r.i < l9.i;
reconsider ri = r.i as Element of REAL by XREAL_0:def 1;
take ri;
thus thesis by A1,A4,A10;
end;
end;
consider x being Function of Seg d,REAL such that
A11: for i holds P[i,x.i] from FUNCT_2:sch 3(A5);
reconsider x as Element of REAL d by Def3;
A12: x in cell(l,r) by A11;
set i0 = the Element of Seg d;
r9.i0 < l9.i0 by A2;
then ex i st r9.i < l9.i & (x.i <= r9.i or l9.i <= x.i) by A3,A12,Th22;
hence contradiction by A11;
end;
given i0 such that
A13: r.i0 <= r9.i0 or l9.i0 <= l.i0;
let x be object;
assume
A14: x in cell(l,r);
then reconsider x as Element of REAL d;
A15: l.i0 <= x.i0 by A1,A14,Th21;
A16: x.i0 <= r.i0 by A1,A14,Th21;
ex i st r9.i < l9.i & (x.i <= r9.i or l9.i <= x.i)
proof
take i0;
thus thesis by A2,A13,A15,A16,XXREAL_0:2;
end;
hence thesis;
end;
theorem Th28:
(for i holds l.i <= r.i) or (for i holds l.i > r.i) implies
(cell(l,r) = cell(l9,r9) iff l = l9 & r = r9)
proof
assume
A1: (for i holds l.i <= r.i) or for i holds l.i > r.i;
thus cell(l,r) = cell(l9,r9) implies l = l9 & r = r9
proof
assume
A2: cell(l,r) = cell(l9,r9);
per cases by A1;
suppose
A3: for i holds l.i <= r.i;
then
A4: for i holds l.i <= l9.i & l9.i <= r9.i & r9.i <= r.i by A2,Th25;
reconsider l,r,l9,r9 as Function of Seg d,REAL by Def3;
A5: now
let i;
A6: l.i <= l9.i by A2,A3,Th25;
l9.i <= l.i by A2,A4,Th25;
hence l.i = l9.i by A6,XXREAL_0:1;
end;
now
let i;
A7: r.i <= r9.i by A2,A4,Th25;
r9.i <= r.i by A2,A3,Th25;
hence r.i = r9.i by A7,XXREAL_0:1;
end;
hence thesis by A5,FUNCT_2:63;
end;
suppose
A8: for i holds l.i > r.i;
then
A9: for i holds r.i <= r9.i & r9.i < l9.i & l9.i <= l.i by A2,Th26;
reconsider l,r,l9,r9 as Function of Seg d,REAL by Def3;
A10: now
let i;
A11: l.i <= l9.i by A2,A9,Th26;
l9.i <= l.i by A2,A8,Th26;
hence l.i = l9.i by A11,XXREAL_0:1;
end;
now
let i;
A12: r.i <= r9.i by A2,A8,Th26;
r9.i <= r.i by A2,A9,Th26;
hence r.i = r9.i by A12,XXREAL_0:1;
end;
hence thesis by A10,FUNCT_2:63;
end;
end;
thus thesis;
end;
definition
let d,G,k;
assume
A1: k <= d;
func cells(k,G) -> finite non empty Subset-Family of REAL d equals
:Def7:
{ cell(l,r) : ((ex X being Subset of Seg d st card X = k &
for i holds (i in X & l.i < r.i & [l.i,r.i] is Gap of G.i) or
(not i in X & l.i = r.i & l.i in G.i)) or
(k = d & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i)) };
coherence
proof
defpred R[Element of REAL d,Element of REAL d] means
((ex X being Subset of Seg d st card X = k &
for i holds (i in X & $1.i < $2.i & [$1.i,$2.i] is Gap of G.i) or
(not i in X & $1.i = $2.i & $1.i in G.i)) or
(k = d & for i holds $2.i < $1.i & [$1.i,$2.i] is Gap of G.i));
deffunc f(Element of REAL d,Element of REAL d) = cell($1,$2);
set CELLS = { f(l,r) : R[l,r] };
reconsider X = Seg k as Subset of Seg d by A1,FINSEQ_1:5;
defpred P[Element of Seg d,Element of [:REAL,REAL:]] means
($1 in X & ex li,ri st $2 = [li,ri] & li < ri & $2 is Gap of G.$1) or
(not $1 in X & ex li st $2 = [li,li] & li in G.$1);
A2: now
let i;
thus ex lri being Element of [:REAL,REAL:] st P[i,lri]
proof
per cases;
suppose
A3: i in X;
consider li,ri such that
A4: li in G.i and
A5: ri in G.i and
A6: li < ri and
A7: for xi st xi in G.i holds not (li < xi & xi < ri) by Th11;
reconsider li,ri as Element of REAL by XREAL_0:def 1;
take [li,ri];
[li,ri] is Gap of G.i by A4,A5,A6,A7,Def5;
hence thesis by A3,A6;
end;
suppose
A8: not i in X;
set li = the Element of G.i;
reconsider li as Element of REAL;
reconsider lri = [li,li] as Element of [:REAL,REAL:];
take lri;
thus thesis by A8;
end;
end;
end;
consider lr being Function of Seg d,[:REAL,REAL:] such that
A9: for i holds P[i,lr.i] from FUNCT_2:sch 3(A2);
deffunc l(Element of Seg d) = (lr.$1)`1;
consider l being Function of Seg d,REAL such that
A10: for i holds l.i = l(i) from FUNCT_2:sch 4;
deffunc r(Element of Seg d) = (lr.$1)`2;
consider r being Function of Seg d,REAL such that
A11: for i holds r.i = r(i) from FUNCT_2:sch 4;
reconsider l,r as Element of REAL d by Def3;
A12: now
let i;
A13: l.i = (lr.i)`1 by A10;
r.i = (lr.i)`2 by A11;
hence lr.i = [l.i,r.i] by A13,MCART_1:21;
end;
now
take A = cell(l,r);
thus A = cell(l,r);
now
take X;
thus card X = k by FINSEQ_1:57;
take l,r;
thus A = cell(l,r);
let i;
per cases;
suppose
A14: i in X;
then consider li,ri such that
A15: lr.i = [li,ri] and
A16: li < ri and
A17: lr.i is Gap of G.i by A9;
A18: lr.i = [l.i,r.i] by A12;
then li = l.i by A15,XTUPLE_0:1;
hence i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or
not i in X & l.i = r.i & l.i in G.i by A14,A15,A16,A17,A18,XTUPLE_0:1
;
end;
suppose
A19: not i in X;
then consider li such that
A20: lr.i = [li,li] and
A21: li in G.i by A9;
A22: [li,li] = [l.i,r.i] by A12,A20;
then li = l.i by XTUPLE_0:1;
hence i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or
not i in X & l.i = r.i & l.i in G.i by A19,A21,A22,XTUPLE_0:1;
end;
end;
hence ex l,r st A = cell(l,r) &
((ex X being Subset of Seg d st card X = k &
for i holds (i in X & l.i < r.i & [l.i,r.i] is Gap of G.i) or
(not i in X & l.i = r.i & l.i in G.i)) or
(k = d & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i));
end;
then
A23: cell(l,r) in CELLS;
defpred Q[object,Element of REAL d,Element of REAL d,object] means
$2 in product G & $3 in product G &
(($4 = [0,[$2,$3]] & $1 = cell($2,$3)) or
($4 = [1,[$2,$3]] & $1 = cell($2,$3)));
defpred S[object,object] means ex l,r st Q[$1,l,r,$2];
A24: for A being object st A in CELLS ex lr being object st S[A,lr]
proof
let A be object;
assume A in CELLS;
then consider l,r such that
A25: A = cell(l,r) and
A26: (ex X being Subset of Seg d st card X = k & for i holds (i in X &
l.i < r.i & [l.i,r.i] is Gap of G.i) or (not i in X & l.i = r.i & l.i in G.i))
or (k = d & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i);
per cases by A26;
suppose
A27: ex X being Subset of Seg d st card X = k &
for i holds i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or
not i in X & l.i = r.i & l.i in G.i;
take [0,[l,r]],l,r;
now
let i;
l.i < r.i & [l.i,r.i] is Gap of G.i or l.i = r.i & l.i in G.i by A27;
hence l.i in G.i & r.i in G.i by Th13;
end;
hence l in product G & r in product G by Th8;
thus thesis by A25;
end;
suppose
A28: k = d & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i;
take [1,[l,r]],l,r;
now
let i;
[l.i,r.i] is Gap of G.i by A28;
hence l.i in G.i & r.i in G.i by Th13;
end;
hence l in product G & r in product G by Th8;
thus thesis by A25;
end;
end;
consider f being Function such that
A29: dom f = CELLS &
for A being object st A in CELLS holds S[A,f.A] from CLASSES1:sch 1(A24);
A30: f is one-to-one
proof
let A,A9 be object;
assume that
A31: A in dom f and
A32: A9 in dom f and
A33: f.A = f.A9;
consider l,r such that
A34: Q[A,l,r,f.A] by A29,A31;
consider l9,r9 such that
A35: Q[A9,l9,r9,f.A9] by A29,A32;
per cases by A34;
suppose
A36: f.A = [0,[l,r]] & A = cell(l,r);
then
A37: [l,r] = [l9,r9] by A33,A35,XTUPLE_0:1;
then l = l9 by XTUPLE_0:1;
hence thesis by A35,A36,A37,XTUPLE_0:1;
end;
suppose
A38: f.A = [1,[l,r]] & A = cell(l,r);
then
A39: [l,r] = [l9,r9] by A33,A35,XTUPLE_0:1;
then l = l9 by XTUPLE_0:1;
hence thesis by A35,A38,A39,XTUPLE_0:1;
end;
end;
reconsider X = product G as finite set;
A40: rng f c= [:{0,1},[:X,X:]:]
proof
let lr be object;
assume lr in rng f;
then consider A being object such that
A41: A in dom f and
A42: lr = f.A by FUNCT_1:def 3;
consider l,r such that
A43: Q[A,l,r,f.A] by A29,A41;
A44: 0 in {0,1} by TARSKI:def 2;
A45: 1 in {0,1} by TARSKI:def 2;
[l,r] in [:X,X:] by A43,ZFMISC_1:87;
hence thesis by A42,A43,A44,A45,ZFMISC_1:87;
end;
CELLS c= bool(REAL d) from FrSet12;
hence thesis by A23,A29,A30,A40,CARD_1:59;
end;
end;
theorem Th29:
k <= d implies for A being Subset of REAL d holds A in cells(k,G) iff
ex l,r st A = cell(l,r) & ((ex X being Subset of Seg d st card X = k &
for i holds (i in X & l.i < r.i & [l.i,r.i] is Gap of G.i) or
(not i in X & l.i = r.i & l.i in G.i)) or
(k = d & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i))
proof
assume k <= d;
then cells(k,G) = { cell(l,r) : ((ex X being Subset of Seg d st card X = k &
for i holds (i in X & l.i < r.i & [l.i,r.i] is Gap of G.i) or
(not i in X & l.i = r.i & l.i in G.i)) or
(k = d & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i)) } by Def7;
hence thesis;
end;
theorem Th30:
k <= d implies (cell(l,r) in cells(k,G) iff
((ex X being Subset of Seg d st card X = k &
for i holds (i in X & l.i < r.i & [l.i,r.i] is Gap of G.i) or
(not i in X & l.i = r.i & l.i in G.i)) or
(k = d & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i)))
proof
assume
A1: k <= d;
hereby
assume cell(l,r) in cells(k,G);
then consider l9,r9 such that
A2: cell(l,r) = cell(l9,r9) and
A3: (ex X being Subset of Seg d st card X = k & for i holds (i in X &
l9.i < r9.i & [l9.i,r9.i] is Gap of G.i) or (not i in X & l9.i = r9.i & l9.i in
G.i)) or (k = d & for i holds r9.i < l9.i & [l9.i,r9.i] is Gap of G.i)
by A1,Th29;
l = l9 & r = r9
proof
per cases by A3;
suppose ex X being Subset of Seg d st card X = k &
for i holds i in X & l9.i < r9.i & [l9.i,r9.i] is Gap of G.i or
not i in X & l9.i = r9.i & l9.i in G.i;
then for i holds l9.i <= r9.i;
hence thesis by A2,Th28;
end;
suppose for i holds r9.i < l9.i & [l9.i,r9.i] is Gap of G.i;
hence thesis by A2,Th28;
end;
end;
hence (ex X being Subset of Seg d st card X = k &
for i holds (i in X & l.i < r.i & [l.i,r.i] is Gap of G.i) or
(not i in X & l.i = r.i & l.i in G.i)) or
(k = d & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i) by A3;
end;
thus thesis by A1,Th29;
end;
theorem Th31:
k <= d & cell(l,r) in cells(k,G) implies
(for i holds (l.i < r.i & [l.i,r.i] is Gap of G.i) or
(l.i = r.i & l.i in G.i)) or
for i holds r.i < l.i & [l.i,r.i] is Gap of G.i
proof
assume that
A1: k <= d and
A2: cell(l,r) in cells(k,G);
per cases by A1,A2,Th30;
suppose ex X being Subset of Seg d st card X = k &
for i holds i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or
not i in X & l.i = r.i & l.i in G.i;
hence thesis;
end;
suppose k = d & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i;
hence thesis;
end;
end;
theorem Th32:
k <= d & cell(l,r) in cells(k,G) implies for i holds l.i in G.i & r.i in G.i
proof
assume that
A1: k <= d and
A2: cell(l,r) in cells(k,G);
let i;
l.i < r.i & [l.i,r.i] is Gap of G.i or l.i = r.i & l.i in G.i or
r.i < l.i & [l.i,r.i] is Gap of G.i by A1,A2,Th31;
hence thesis by Th13;
end;
theorem
k <= d & cell(l,r) in cells(k,G) implies
(for i holds l.i <= r.i) or for i holds r.i < l.i by Th31;
theorem Th34:
for A being Subset of REAL d holds
A in cells(0,G) iff ex x st A = cell(x,x) & for i holds x.i in G.i
proof
let A be Subset of REAL d;
hereby
assume A in cells(0,G);
then consider l,r such that
A1: A = cell(l,r) and
A2: (ex X being Subset of Seg d st card X = 0 & for i holds (i in X & l
.i < r.i & [l.i,r.i] is Gap of G.i) or (not i in X & l.i = r.i & l.i in G.i))
or (0 = d & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i)
by Th29;
consider X being Subset of Seg d such that
A3: card X = 0 and
A4: for i holds i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or not i
in X & l.i = r.i & l.i in G.i
by A2;
reconsider l9 = l, r9 = r as Function of Seg d,REAL by Def3;
X = {} by A3;
then
A5: for i holds l9.i = r9.i & l.i in G.i by A4;
then l9 = r9 by FUNCT_2:63;
hence ex x st A = cell(x,x) & for i holds x.i in G.i by A1,A5;
end;
given x such that
A6: A = cell(x,x) and
A7: for i holds x.i in G.i;
ex X being Subset of Seg d st card X = 0 &
for i holds i in X & x.i < x.i & [x.i,x.i] is Gap of G.i or
not i in X & x.i = x.i & x.i in G.i
proof
reconsider X = {} as Subset of Seg d by XBOOLE_1:2;
take X;
thus thesis by A7;
end;
hence thesis by A6,Th29;
end;
theorem Th35:
cell(l,r) in cells(0,G) iff l = r & for i holds l.i in G.i
proof
hereby
assume cell(l,r) in cells(0,G);
then consider x such that
A1: cell(l,r) = cell(x,x) and
A2: for i holds x.i in G.i by Th34;
A3: for i holds x.i <= x.i;
then l = x by A1,Th28;
hence l = r & for i holds l.i in G.i by A1,A2,A3,Th28;
end;
thus thesis by Th34;
end;
theorem Th36:
for A being Subset of REAL d holds A in cells(d,G) iff
ex l,r st A = cell(l,r) & (for i holds [l.i,r.i] is Gap of G.i) &
((for i holds l.i < r.i) or for i holds r.i < l.i )
proof
let A be Subset of REAL d;
hereby
assume A in cells(d,G);
then consider l,r such that
A1: A = cell(l,r) and
A2: (ex X being Subset of Seg d st card X = d & for i holds (i in X & l
.i < r.i & [l.i,r.i] is Gap of G.i) or (not i in X & l.i = r.i & l.i in G.i))
or (d = d & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i)
by Th29;
thus
ex l,r st A = cell(l,r) & (for i holds [l.i,r.i] is Gap of G.i) &
((for i holds l.i < r.i) or for i holds r.i < l.i )
proof
take l,r;
per cases by A2;
suppose ex X being Subset of Seg d st card X = d &
for i holds i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or
not i in X & l.i = r.i & l.i in G.i;
then consider X being Subset of Seg d such that
A3: card X = d and
A4: for i holds i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or not i
in X & l.i = r.i & l.i in G.i;
card X = card Seg d by A3,FINSEQ_1:57;
then not X c< Seg d by CARD_2:48;
then X = Seg d by XBOOLE_0:def 8;
hence thesis by A1,A4;
end;
suppose for i holds r.i < l.i & [l.i,r.i] is Gap of G.i;
hence thesis by A1;
end;
end;
end;
given l,r such that
A5: A = cell(l,r) and
A6: for i holds [l.i,r.i] is Gap of G.i and
A7: (for i holds l.i < r.i) or for i holds r.i < l.i;
per cases by A7;
suppose
A8: for i holds l.i < r.i;
ex X being Subset of Seg d st card X = d &
for i holds i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or
not i in X & l.i = r.i & l.i in G.i
proof
Seg d c= Seg d;
then reconsider X = Seg d as Subset of Seg d;
take X;
thus card X = d by FINSEQ_1:57;
thus thesis by A6,A8;
end;
hence thesis by A5,Th29;
end;
suppose for i holds r.i < l.i;
hence thesis by A5,A6,Th29;
end;
end;
theorem Th37:
cell(l,r) in cells(d,G) iff (for i holds [l.i,r.i] is Gap of G.i) &
((for i holds l.i < r.i) or for i holds r.i < l.i )
proof
hereby
assume cell(l,r) in cells(d,G);
then consider l9,r9 such that
A1: cell(l,r) = cell(l9,r9) and
A2: for i holds [l9.i,r9.i] is Gap of G.i and
A3: (for i holds l9.i < r9.i) or for i holds r9.i < l9.i by Th36;
A4: (for i holds l9.i <= r9.i) or for i holds r9.i < l9.i by A3;
then
A5: l = l9 by A1,Th28;
r = r9 by A1,A4,Th28;
hence (for i holds [l.i,r.i] is Gap of G.i) &
((for i holds l.i < r.i) or for i holds r.i < l.i ) by A2,A3,A5;
end;
thus thesis by Th36;
end;
theorem Th38:
d = d9 + 1 implies for A being Subset of REAL d holds A in cells(d9,G) iff
ex l,r,i0 st A = cell(l,r) & l.i0 = r.i0 & l.i0 in G.i0 &
for i st i <> i0 holds l.i < r.i & [l.i,r.i] is Gap of G.i
proof
assume
A1: d = d9 + 1;
then
A2: d9 < d by NAT_1:13;
let A be Subset of REAL d;
hereby
assume A in cells(d9,G);
then consider l,r such that
A3: A = cell(l,r) and
A4: (ex X being Subset of Seg d st card X = d9 & for i holds (i in X &
l.i < r.i & [l.i,r.i] is Gap of G.i) or (not i in X & l.i = r.i & l.i in G.i))
or (d9 = d & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i)
by A2,Th29;
take l,r;
consider X being Subset of Seg d such that
A5: card X = d9 and
A6: for i holds i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or not i
in X & l.i = r.i & l.i in G.i
by A1,A4;
card(Seg d \ X) = card Seg d - card X by CARD_2:44
.= d - d9 by A5,FINSEQ_1:57
.= 1 by A1;
then consider i0 being object such that
A7: Seg d \ X = {i0} by CARD_2:42;
i0 in Seg d \ X by A7,TARSKI:def 1;
then reconsider i0 as Element of Seg d by XBOOLE_0:def 5;
take i0;
A8: now
let i;
i in Seg d \ X iff i = i0 by A7,TARSKI:def 1;
hence i in X iff i <> i0 by XBOOLE_0:def 5;
end;
thus A = cell(l,r) by A3;
not i0 in X by A8;
hence l.i0 = r.i0 & l.i0 in G.i0 by A6;
let i;
assume i <> i0;
then i in X by A8;
hence l.i < r.i & [l.i,r.i] is Gap of G.i by A6;
end;
given l,r,i0 such that
A9: A = cell(l,r) and
A10: l.i0 = r.i0 and
A11: l.i0 in G.i0 and
A12: for i st i <> i0 holds l.i < r.i & [l.i,r.i] is Gap of G.i;
reconsider X = Seg d \ {i0} as Subset of Seg d by XBOOLE_1:36;
card X = d9 & for i holds i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or
not i in X & l.i = r.i & l.i in G.i
proof
thus card X = card Seg d - card {i0} by CARD_2:44
.= d - card {i0} by FINSEQ_1:57
.= d - 1 by CARD_1:30
.= d9 by A1;
let i;
i in {i0} iff i = i0 by TARSKI:def 1;
hence thesis by A10,A11,A12,XBOOLE_0:def 5;
end;
hence thesis by A2,A9,Th29;
end;
theorem
d = d9 + 1 implies (cell(l,r) in cells(d9,G) iff
ex i0 st l.i0 = r.i0 & l.i0 in G.i0 &
for i st i <> i0 holds l.i < r.i & [l.i,r.i] is Gap of G.i)
proof
assume
A1: d = d9 + 1;
hereby
assume cell(l,r) in cells(d9,G);
then consider l9,r9,i0 such that
A2: cell(l,r) = cell(l9,r9) and
A3: l9.i0 = r9.i0 and
A4: l9.i0 in G.i0 and
A5: for i st i <> i0 holds l9.i < r9.i & [l9.i,r9.i] is Gap of G.i by A1,Th38;
take i0;
A6: now
let i;
i = i0 or i <> i0;
hence l9.i <= r9.i by A3,A5;
end;
then
A7: l = l9 by A2,Th28;
r = r9 by A2,A6,Th28;
hence l.i0 = r.i0 & l.i0 in G.i0 &
for i st i <> i0 holds l.i < r.i & [l.i,r.i] is Gap of G.i by A3,A4,A5,A7;
end;
thus thesis by A1,Th38;
end;
theorem Th40:
for A being Subset of REAL d holds A in cells(1,G) iff
ex l,r,i0 st A = cell(l,r) &
(l.i0 < r.i0 or d = 1 & r.i0 < l.i0) & [l.i0,r.i0] is Gap of G.i0 &
for i st i <> i0 holds l.i = r.i & l.i in G.i
proof
A1: d >= 1 by Def2;
let A be Subset of REAL d;
hereby
assume A in cells(1,G);
then consider l,r such that
A2: A = cell(l,r) and
A3: (ex X being Subset of Seg d st card X = 1 & for i holds (i in X & l
.i < r.i & [l.i,r.i] is Gap of G.i) or (not i in X & l.i = r.i & l.i in G.i))
or (1 = d & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i)
by A1,Th29;
take l,r;
thus ex i0 st A = cell(l,r) &
(l.i0 < r.i0 or d = 1 & r.i0 < l.i0) & [l.i0,r.i0] is Gap of G.i0 &
for i st i <> i0 holds l.i = r.i & l.i in G.i
proof
per cases by A3;
suppose ex X being Subset of Seg d st card X = 1 &
for i holds i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or
not i in X & l.i = r.i & l.i in G.i;
then consider X being Subset of Seg d such that
A4: card X = 1 and
A5: for i holds i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or not i
in X & l.i = r.i & l.i in G.i;
consider i0 being object such that
A6: X = {i0} by A4,CARD_2:42;
A7: i0 in X by A6,TARSKI:def 1;
then reconsider i0 as Element of Seg d;
take i0;
thus A = cell(l,r) &
(l.i0 < r.i0 or d = 1 & r.i0 < l.i0) & [l.i0,r.i0] is Gap of G.i0
by A2,A5,A7;
let i;
not i in X iff i <> i0 by A6,TARSKI:def 1;
hence thesis by A5;
end;
suppose
A8: d = 1 & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i;
reconsider i0 = 1 as Element of Seg d by A1,FINSEQ_1:1;
take i0;
thus A = cell(l,r) &
(l.i0 < r.i0 or d = 1 & r.i0 < l.i0) & [l.i0,r.i0] is Gap of G.i0
by A2,A8;
let i;
A9: 1 <= i by FINSEQ_1:1;
i <= d by FINSEQ_1:1;
hence thesis by A8,A9,XXREAL_0:1;
end;
end;
end;
given l,r,i0 such that
A10: A = cell(l,r) and
A11: l.i0 < r.i0 or d = 1 & r.i0 < l.i0 and
A12: [l.i0,r.i0] is Gap of G.i0 and
A13: for i st i <> i0 holds l.i = r.i & l.i in G.i;
set X = {i0};
per cases by A11;
suppose
A14: l.i0 < r.i0;
A15: card X = 1 by CARD_1:30;
now
let i;
i in X iff i = i0 by TARSKI:def 1;
hence i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or
not i in X & l.i = r.i & l.i in G.i by A12,A13,A14;
end;
hence thesis by A1,A10,A15,Th29;
end;
suppose
A16: d = 1 & r.i0 < l.i0;
now
let i;
A17: 1 <= i by FINSEQ_1:1;
A18: i <= d by FINSEQ_1:1;
A19: 1 <= i0 by FINSEQ_1:1;
A20: i0 <= d by FINSEQ_1:1;
A21: i = 1 by A16,A17,A18,XXREAL_0:1;
i0 = 1 by A16,A19,A20,XXREAL_0:1;
hence r.i < l.i & [l.i,r.i] is Gap of G.i by A12,A16,A21;
end;
hence thesis by A10,A11,Th29;
end;
end;
theorem
cell(l,r) in cells(1,G) iff
ex i0 st (l.i0 < r.i0 or d = 1 & r.i0 < l.i0) & [l.i0,r.i0] is Gap of G.i0 &
for i st i <> i0 holds l.i = r.i & l.i in G.i
proof
hereby
assume cell(l,r) in cells(1,G);
then consider l9,r9,i0 such that
A1: cell(l,r) = cell(l9,r9) and
A2: l9.i0 < r9.i0 or d = 1 & r9.i0 < l9.i0 and
A3: [l9.i0,r9.i0] is Gap of G.i0 and
A4: for i st i <> i0 holds l9.i = r9.i & l9.i in G.i by Th40;
A5: (for i holds l9.i <= r9.i) or for i holds r9.i < l9.i
proof
per cases by A2;
suppose
A6: l9.i0 < r9.i0;
now
let i;
i = i0 or i <> i0;
hence l9.i <= r9.i by A4,A6;
end;
hence thesis;
end;
suppose
A7: d = 1 & r9.i0 < l9.i0;
now
let i;
A8: 1 <= i by FINSEQ_1:1;
A9: i <= d by FINSEQ_1:1;
A10: 1 <= i0 by FINSEQ_1:1;
A11: i0 <= d by FINSEQ_1:1;
A12: i = 1 by A7,A8,A9,XXREAL_0:1;
i0 = 1 by A7,A10,A11,XXREAL_0:1;
hence r9.i < l9.i by A7,A12;
end;
hence thesis;
end;
end;
then
A13: l = l9 by A1,Th28;
r = r9 by A1,A5,Th28;
hence ex i0 st (l.i0 < r.i0 or d = 1 & r.i0 < l.i0) &
[l.i0,r.i0] is Gap of G.i0 &
for i st i <> i0 holds l.i = r.i & l.i in G.i by A2,A3,A4,A13;
end;
thus thesis by Th40;
end;
theorem Th42:
k <= d & k9 <= d & cell(l,r) in cells(k,G) & cell(l9,r9) in cells(k9,G) &
cell(l,r) c= cell(l9,r9) implies for i holds l.i = l9.i & r.i = r9.i or
l.i = l9.i & r.i = l9.i or l.i = r9.i & r.i = r9.i or
l.i <= r.i & r9.i < l9.i & r9.i <= l.i & r.i <= l9.i
proof
assume that
A1: k <= d and
A2: k9 <= d and
A3: cell(l,r) in cells(k,G) and
A4: cell(l9,r9) in cells(k9,G);
assume
A5: cell(l,r) c= cell(l9,r9);
let i;
per cases by A2,A4,Th31;
suppose
A6: for i holds l9.i < r9.i & [l9.i,r9.i] is Gap of G.i or
l9.i = r9.i & l9.i in G.i;
then
A7: for i holds l9.i <= r9.i;
then
A8: l9.i <= l.i by A5,Th25;
A9: l.i <= r.i by A5,A7,Th25;
A10: r.i <= r9.i by A5,A7,Th25;
A11: l9.i <= r.i by A8,A9,XXREAL_0:2;
A12: l.i <= r9.i by A9,A10,XXREAL_0:2;
thus thesis
proof
per cases by A6;
suppose
A13: [l9.i,r9.i] is Gap of G.i;
A14: now
assume that
A15: l9.i <> l.i and
A16: l.i <> r9.i;
A17: l9.i < l.i by A8,A15,XXREAL_0:1;
A18: l.i < r9.i by A12,A16,XXREAL_0:1;
l.i in G.i by A1,A3,Th32;
hence contradiction by A13,A17,A18,Th13;
end;
now
assume that
A19: l9.i <> r.i and
A20: r.i <> r9.i;
A21: l9.i < r.i by A11,A19,XXREAL_0:1;
A22: r.i < r9.i by A10,A20,XXREAL_0:1;
r.i in G.i by A1,A3,Th32;
hence contradiction by A13,A21,A22,Th13;
end;
hence thesis by A9,A14,XXREAL_0:1;
end;
suppose l9.i = r9.i;
hence thesis by A8,A10,A11,A12,XXREAL_0:1;
end;
end;
end;
suppose
A23: for i holds r9.i < l9.i & [l9.i,r9.i] is Gap of G.i;
then
A24: r9.i < l9.i;
A25: [l9.i,r9.i] is Gap of G.i by A23;
thus thesis
proof
per cases by A1,A3,Th31;
suppose
A26: for i holds r.i < l.i & [l.i,r.i] is Gap of G.i;
then
A27: r.i <= r9.i by A5,Th26;
A28: l9.i <= l.i by A5,A26,Th26;
A29: now
assume l9.i <> l.i;
then
A30: l9.i < l.i by A28,XXREAL_0:1;
l.i in G.i by A1,A3,Th32;
hence contradiction by A24,A25,A30,Th13;
end;
now
assume r.i <> r9.i;
then
A31: r.i < r9.i by A27,XXREAL_0:1;
r.i in G.i by A1,A3,Th32;
hence contradiction by A24,A25,A31,Th13;
end;
hence thesis by A29;
end;
suppose
A32: for i holds l.i < r.i & [l.i,r.i] is Gap of G.i or
l.i = r.i & l.i in G.i;
A33: l.i in G.i by A1,A3,Th32;
r.i in G.i by A1,A3,Th32;
hence thesis by A24,A25,A32,A33,Th13;
end;
end;
end;
end;
theorem Th43:
k < k9 & k9 <= d & cell(l,r) in cells(k,G) & cell(l9,r9) in cells(k9,G) &
cell(l,r) c= cell(l9,r9) implies
ex i st l.i = l9.i & r.i = l9.i or l.i = r9.i & r.i = r9.i
proof
assume that
A1: k < k9 and
A2: k9 <= d and
A3: cell(l,r) in cells(k,G) and
A4: cell(l9,r9) in cells(k9,G);
A5: k + 0 < d by A1,A2,XXREAL_0:2;
assume
A6: cell(l,r) c= cell(l9,r9);
consider X being Subset of Seg d such that
A7: card X = k and
A8: for i holds i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or not i
in X & l.i = r.i & l.i in G.i
by A3,A5,Th30;
A9: d - k > 0 by A5,XREAL_1:20;
card(Seg d \ X) = card Seg d - card X by CARD_2:44
.= d - k by A7,FINSEQ_1:57;
then consider i0 being object such that
A10: i0 in Seg d \ X by A9,CARD_1:27,XBOOLE_0:def 1;
reconsider i0 as Element of Seg d by A10,XBOOLE_0:def 5;
not i0 in X by A10,XBOOLE_0:def 5;
then
A11: l.i0 = r.i0 by A8;
per cases by A2,A3,A4,A5,A6,Th42;
suppose l.i0 = l9.i0 & r.i0 = r9.i0;
hence thesis by A11;
end;
suppose l.i0 = l9.i0 & r.i0 = l9.i0;
hence thesis;
end;
suppose l.i0 = r9.i0 & r.i0 = r9.i0;
hence thesis;
end;
suppose
A12: r9.i0 < l9.i0;
assume
A13: for i holds (l.i <> l9.i or r.i <> l9.i) & (l.i <> r9.i or r.i <> r9.i);
defpred P[Element of Seg d,Element of REAL] means
l.$1 <= $2 & $2 <= r.$1 & r9.$1 < $2 & $2 < l9.$1;
A14: for i ex xi being Element of REAL st P[i,xi]
proof
let i;
A15: l.i in G.i by A3,A5,Th32;
A16: r.i in G.i by A3,A5,Th32;
A17: r9.i < l9.i by A2,A4,A12,Th31;
A18: [l9.i,r9.i] is Gap of G.i by A2,A4,A12,Th31;
per cases;
suppose
A19: r9.i < l.i & l.i < l9.i;
reconsider li = l.i as Element of REAL by XREAL_0:def 1;
take li;
thus thesis by A8,A19;
end;
suppose
A20: l.i <= r9.i;
A21: l.i >= r9.i by A15,A17,A18,Th13;
then
A22: l.i = r9.i by A20,XXREAL_0:1;
then r.i <> r9.i by A13;
then l.i < r.i by A8,A22;
then consider xi being Element of REAL such that
A23: l.i < xi and
A24: xi < r.i by Th1;
take xi;
r.i <= l9.i by A16,A17,A18,Th13;
hence thesis by A21,A23,A24,XXREAL_0:2;
end;
suppose
A25: l9.i <= l.i;
l9.i >= l.i by A15,A17,A18,Th13;
then
A26: l9.i = l.i by A25,XXREAL_0:1;
l9.i >= r.i by A16,A17,A18,Th13;
then l9.i = r.i by A8,A26;
hence thesis by A13,A26;
end;
end;
consider x being Function of Seg d,REAL such that
A27: for i holds P[i,x.i] from FUNCT_2:sch 3(A14);
reconsider x as Element of REAL d by Def3;
A28: x in cell(l,r) by A27;
for i st r9.i < l9.i holds r9.i < x.i & x.i < l9.i by A27;
hence contradiction by A6,A12,A28,Th22;
end;
end;
theorem Th44:
for X,X9 being Subset of Seg d st cell(l,r) c= cell(l9,r9) &
(for i holds (i in X & l.i < r.i & [l.i,r.i] is Gap of G.i) or
(not i in X & l.i = r.i & l.i in G.i)) &
(for i holds (i in X9 & l9.i < r9.i & [l9.i,r9.i] is Gap of G.i) or
(not i in X9 & l9.i = r9.i & l9.i in G.i)) holds X c= X9 &
(for i st i in X or not i in X9 holds l.i = l9.i & r.i = r9.i) &
for i st not i in X & i in X9 holds
l.i = l9.i & r.i = l9.i or l.i = r9.i & r.i = r9.i
proof
let X,X9 be Subset of Seg d;
assume
A1: cell(l,r) c= cell(l9,r9);
assume
A2: for i holds i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or
not i in X & l.i = r.i & l.i in G.i;
assume
A3: for i holds i in X9 & l9.i < r9.i & [l9.i,r9.i] is Gap of G.i or
not i in X9 & l9.i = r9.i & l9.i in G.i;
A4: l in cell(l,r) by Th23;
A5: r in cell(l,r) by Th23;
A6: for i holds l9.i <= r9.i by A3;
thus X c= X9
proof
let i be object;
assume that
A7: i in X and
A8: not i in X9;
reconsider i as Element of Seg d by A7;
A9: l.i < r.i by A2,A7;
A10: l9.i = r9.i by A3,A8;
A11: l9.i <= l.i by A1,A4,A6,Th21;
r.i <= r9.i by A1,A5,A6,Th21;
hence thesis by A9,A10,A11,XXREAL_0:2;
end;
set k = card X;
set k9 = card X9;
A12: card Seg d = d by FINSEQ_1:57;
then
A13: k <= d by NAT_1:43;
A14: k9 <= d by A12,NAT_1:43;
A15: cell(l,r) in cells(k,G) by A2,A13,Th30;
A16: cell(l9,r9) in cells(k9,G) by A3,A14,Th30;
thus for i st i in X or not i in X9 holds l.i = l9.i & r.i = r9.i
proof
let i;
assume
A17: i in X or not i in X9;
l9.i <= r9.i by A3;
then l.i = l9.i & r.i = r9.i or
l.i = l9.i & r.i = l9.i or l.i = r9.i & r.i = r9.i by A1,A13,A14,A15,A16
,Th42;
hence thesis by A2,A3,A17;
end;
thus for i st not i in X & i in X9 holds
l.i = l9.i & r.i = l9.i or l.i = r9.i & r.i = r9.i
proof
let i;
assume that
A18: not i in X and
A19: i in X9;
A20: l.i = r.i by A2,A18;
l9.i < r9.i by A3,A19;
hence thesis by A1,A13,A14,A15,A16,A20,Th42;
end;
end;
definition
let d,G,k;
mode Cell of k,G is Element of cells(k,G);
end;
definition
let d,G,k;
mode Chain of k,G is Subset of cells(k,G);
end;
definition
let d,G,k;
func 0_(k,G) -> Chain of k,G equals
{};
coherence by SUBSET_1:1;
end;
definition
let d,G;
func Omega(G) -> Chain of d,G equals
cells(d,G);
coherence
proof
cells(d,G) c= cells(d,G);
hence thesis;
end;
end;
notation
let d,G,k;
let C1,C2 be Chain of k,G;
synonym C1 + C2 for C1 \+\ C2;
end;
definition
let d,G,k;
let C1,C2 be Chain of k,G;
redefine func C1 + C2 -> Chain of k,G; :: redefines + (CHAIN_1, synonym) → \+\ (XBOOLE_0, definition)
coherence
proof
C1 \+\ C2 c= cells(k,G);
hence thesis;
end;
end;
definition
let d,G;
func infinite-cell(G) -> Cell of d,G means
:Def10:
ex l,r st it = cell(l,r) & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i;
existence
proof
defpred P[Element of Seg d,Element of REAL] means
$2 in G.$1 & for xi st xi in G.$1 holds xi <= $2;
A1: for i ex li being Element of REAL st P[i,li] by Th9;
consider l being Function of Seg d,REAL such that
A2: for i holds P[i,l.i] from FUNCT_2:sch 3(A1);
reconsider l as Element of REAL d by Def3;
defpred R[Element of Seg d,Element of REAL] means
$2 in G.$1 & for xi st xi in G.$1 holds xi >= $2;
A3: for i ex ri being Element of REAL st R[i,ri] by Th10;
consider r being Function of Seg d,REAL such that
A4: for i holds R[i,r.i] from FUNCT_2:sch 3(A3);
reconsider r as Element of REAL d by Def3;
A5: now
let i;
r.i in G.i by A4;
then
A6: r.i <= l.i by A2;
now
assume
A7: l.i = r.i;
consider x1,x2 be object such that
A8: x1 in G.i and
A9: x2 in G.i and
A10: x1 <> x2 by ZFMISC_1:def 10;
reconsider x1,x2 as Element of REAL by A8,A9;
A11: r.i <= x1 by A4,A8;
A12: x1 <= l.i by A2,A8;
A13: r.i <= x2 by A4,A9;
A14: x2 <= l.i by A2,A9;
x1 = l.i by A7,A11,A12,XXREAL_0:1;
hence contradiction by A7,A10,A13,A14,XXREAL_0:1;
end;
hence r.i < l.i by A6,XXREAL_0:1;
end;
A15: now
let i;
A16: l.i in G.i by A2;
A17: r.i in G.i by A4;
A18: r.i < l.i by A5;
for xi st xi in G.i holds not (l.i < xi or xi < r.i) by A2,A4;
hence r.i < l.i & [l.i,r.i] is Gap of G.i by A16,A17,A18,Th13;
end;
then reconsider A = cell(l,r) as Cell of d,G by Th30;
take A,l,r;
thus thesis by A15;
end;
uniqueness
proof
let A,A9 be Cell of d,G;
given l,r such that
A19: A = cell(l,r) and
A20: for i holds r.i < l.i & [l.i,r.i] is Gap of G.i;
given l9,r9 such that
A21: A9 = cell(l9,r9) and
A22: for i holds r9.i < l9.i & [l9.i,r9.i] is Gap of G.i;
reconsider l,r,l9,r9 as Function of Seg d,REAL by Def3;
A23: now
let i;
A24: r.i < l.i by A20;
A25: [l.i,r.i] is Gap of G.i by A20;
A26: r9.i < l9.i by A22;
[l9.i,r9.i] is Gap of G.i by A22;
hence l.i = l9.i & r.i = r9.i by A24,A25,A26,Th19;
end;
then l = l9 by FUNCT_2:63;
hence thesis by A19,A21,A23,FUNCT_2:63;
end;
end;
theorem Th45:
cell(l,r) is Cell of d,G implies
(cell(l,r) = infinite-cell(G) iff for i holds r.i < l.i)
proof
assume
A1: cell(l,r) is Cell of d,G;
then reconsider A = cell(l,r) as Cell of d,G;
hereby
assume cell(l,r) = infinite-cell(G);
then consider l9,r9 such that
A2: cell(l,r) = cell(l9,r9) and
A3: for i holds r9.i < l9.i & [l9.i,r9.i] is Gap of G.i by Def10;
A4: l = l9 by A2,A3,Th28;
r = r9 by A2,A3,Th28;
hence for i holds r.i < l.i by A3,A4;
end;
set i0 = the Element of Seg d;
assume for i holds r.i < l.i;
then
A5: r.i0 < l.i0;
A6: A = cell(l,r);
for i holds r.i < l.i & [l.i,r.i] is Gap of G.i by A1,A5,Th31;
hence thesis by A6,Def10;
end;
theorem Th46:
cell(l,r) = infinite-cell(G) iff
for i holds r.i < l.i & [l.i,r.i] is Gap of G.i
proof
hereby
assume cell(l,r) = infinite-cell(G);
then consider l9,r9 such that
A1: cell(l,r) = cell(l9,r9) and
A2: for i holds r9.i < l9.i & [l9.i,r9.i] is Gap of G.i by Def10;
A3: l = l9 by A1,A2,Th28;
r = r9 by A1,A2,Th28;
hence for i holds r.i < l.i & [l.i,r.i] is Gap of G.i by A2,A3;
end;
assume
A4: for i holds r.i < l.i & [l.i,r.i] is Gap of G.i;
then cell(l,r) is Cell of d,G by Th30;
hence thesis by A4,Def10;
end;
scheme ChainInd { d()->non zero Nat, G()->Grating of d(),
k()->Nat, C()->Chain of k(),G(), P[set] } : P[C()]
provided
A1: P[0_(k(),G())] and
A2: for A being Cell of k(),G() st A in C() holds P[{A}] and
A3: for C1,C2 being Chain of k(),G() st C1 c= C() & C2 c= C() &
P[C1] & P[C2] holds P[C1 + C2]
proof
A4: C() is finite;
A5: P[{}] by A1;
A6: for x,B being set st x in C() & B c= C() & P[B] holds P[B \/ {x}]
proof
let A,C1 be set;
assume that
A7: A in C() and
A8: C1 c= C() and
A9: P[C1];
reconsider A9 = A as Cell of k(),G() by A7;
reconsider C19 = C1 as Chain of k(),G() by A8,XBOOLE_1:1;
per cases;
suppose A in C1;
then {A} c= C1 by ZFMISC_1:31;
hence thesis by A9,XBOOLE_1:12;
end;
suppose
A10: not A in C1;
now
let A9 be object;
assume
A11: A9 in C1 /\ {A};
then
A12: A9 in C1 by XBOOLE_0:def 4;
A9 in {A} by A11,XBOOLE_0:def 4;
hence contradiction by A10,A12,TARSKI:def 1;
end;
then C1 /\ {A} = {} by XBOOLE_0:def 1;
then
A13: C19 + {A9} = C1 \/ {A} \ {} by XBOOLE_1:101
.= C1 \/ {A};
A14: P[{A9}] by A2,A7;
{A} c= C() by A7,ZFMISC_1:31;
hence thesis by A3,A8,A9,A13,A14;
end;
end;
thus P[C()] from FINSET_1:sch 2(A4,A5,A6);
end;
:: the boundary operator
definition
let d,G,k;
let A be Cell of k,G;
func star A -> Chain of (k + 1),G equals
{ B where B is Cell of (k + 1),G : A c= B };
coherence
proof
defpred P[set] means A c= $1;
{ B where B is Cell of (k + 1),G : P[B] } c= cells(k + 1,G) from
FRAENKEL:sch 10;
hence thesis;
end;
end;
theorem Th47:
for A being Cell of k,G, B being Cell of (k + 1),G holds
B in star A iff A c= B
proof
let A be Cell of k,G, B be Cell of (k + 1),G;
defpred P[set] means A c= $1;
A1: star A = { B9 where B9 is Cell of (k + 1),G : P[B9] };
thus B in star A iff P[B] from LMOD_7:sch 7(A1);
end;
definition
let d,G,k;
let C be Chain of (k + 1),G;
func del C -> Chain of k,G equals
{ A where A is Cell of k,G : k + 1 <= d & card(star A /\ C) is odd };
coherence
proof
defpred P[Cell of k,G] means k + 1 <= d & card(star $1 /\ C) is odd;
{ A where A is Cell of k,G : P[A] } c= cells(k,G) from FRAENKEL:sch 10;
hence thesis;
end;
end;
notation
let d,G,k;
let C be Chain of (k + 1),G;
synonym .C for del C;
end;
definition
let d,G,k;
let C be Chain of (k + 1),G, C9 be Chain of k,G;
pred C9 bounds C means
C9 = del C;
end;
theorem Th48:
for A being Cell of k,G, C being Chain of (k + 1),G holds
A in del C iff k + 1 <= d & card(star A /\ C) is odd
proof
let A be Cell of k,G, C be Chain of (k + 1),G;
defpred P[Cell of k,G] means k + 1 <= d & card(star $1 /\ C) is odd;
A1: del C = { A9 where A9 is Cell of k,G : P[A9] };
thus A in del C iff P[A] from LMOD_7:sch 7(A1);
end;
theorem Th49:
k + 1 > d implies for C being Chain of (k + 1),G holds del C = 0_(k,G)
proof
assume
A1: k + 1 > d;
let C be Chain of (k + 1),G;
for A being object holds not A in del C by A1,Th48;
hence thesis by XBOOLE_0:def 1;
end;
theorem Th50:
k + 1 <= d implies for A being Cell of k,G, B being Cell of (k + 1),G holds
A in del {B} iff A c= B
proof
assume
A1: k + 1 <= d;
let A be Cell of k,G, B be Cell of (k + 1),G;
set X = star A /\ {B};
card X is odd iff B in star A
proof
per cases;
suppose
A2: B in star A;
now
let B9 be object;
B9 in {B} iff B9 = B by TARSKI:def 1;
hence B9 in X iff B9 = B by A2,XBOOLE_0:def 4;
end;
then X = {B} by TARSKI:def 1;
then card X = 2* 0 + 1 by CARD_1:30;
hence thesis by A2;
end;
suppose
A3: not B in star A;
now
let B9 be object;
B9 = B or not B9 in {B} by TARSKI:def 1;
hence not B9 in X by A3,XBOOLE_0:def 4;
end;
then card X = 2* 0 by CARD_1:27,XBOOLE_0:def 1;
hence thesis by A3;
end;
end;
hence thesis by A1,Th47,Th48;
end;
:: lemmas
theorem Th51:
d = d9 + 1 implies for A being Cell of d9,G holds card(star A) = 2
proof
assume
A1: d = d9 + 1;
then
A2: d9 < d by NAT_1:13;
let A be Cell of d9,G;
consider l,r,i0 such that
A3: A = cell(l,r) and
A4: l.i0 = r.i0 and
A5: l.i0 in G.i0 and
A6: for i st i <> i0 holds l.i < r.i & [l.i,r.i] is Gap of G.i by A1,Th38;
A7: now
let i;
i = i0 or i <> i0;
hence l.i <= r.i by A4,A6;
end;
ex B1,B2 being set st B1 in star A & B2 in star A & B1 <> B2 &
for B being set st B in star A holds B = B1 or B = B2
proof
ex l1,r1 st [l1.i0,r1.i0] is Gap of G.i0 & r1.i0 = l.i0 &
((l1.i0 < r1.i0 & for i st i <> i0 holds l1.i = l.i & r1.i = r.i) or
for i holds r1.i < l1.i & [l1.i,r1.i] is Gap of G.i)
proof
consider l1i0 being Element of REAL such that
A8: [l1i0,l.i0] is Gap of G.i0 by A5,Th16;
per cases by A8,Th13;
suppose
A9: l1i0 < l.i0;
defpred P[Element of Seg d,Element of REAL] means
($1 = i0 implies $2 = l1i0) &
($1 <> i0 implies $2 = l.$1);
A10: for i ex li being Element of REAL st P[i,li]
proof
let i;
A11: l.i in REAL by XREAL_0:def 1;
i = i0 or i <> i0;
hence thesis by A11;
end;
consider l1 being Function of Seg d,REAL such that
A12: for i holds P[i,l1.i] from FUNCT_2:sch 3(A10);
reconsider l1 as Element of REAL d by Def3;
take l1,r;
thus thesis by A4,A8,A9,A12;
end;
suppose
A13: l.i0 < l1i0;
consider l1,r1 such that
cell(l1,r1) = infinite-cell(G) and
A14: for i holds r1.i < l1.i & [l1.i,r1.i] is Gap of G.i by Def10;
take l1,r1;
A15: r1.i0 < l1.i0 by A14;
[l1.i0,r1.i0] is Gap of G.i0 by A14;
hence thesis by A8,A13,A14,A15,Th19;
end;
end;
then consider l1,r1 such that
A16: [l1.i0,r1.i0] is Gap of G.i0 and
A17: r1.i0 = l.i0 and
A18: (l1.i0 < r1.i0 & for i st i <> i0 holds l1.i = l.i & r1.i = r.i)
or for i holds r1.i < l1.i & [l1.i,r1.i] is Gap of G.i;
A19: now
let i;
A20: i
<> i0 & l1.i = l.i & r1.i = r.i implies [l1.i,r1.i] is Gap of G.i by A6;
i = i0 or i <> i0;
hence [l1.i,r1.i] is Gap of G.i by A16,A18,A20;
end;
A21: (for i holds l1.i < r1.i) or for i holds r1.i < l1.i
proof
per cases by A18;
suppose
A22: l1.i0 < r1.i0 & for i st i <> i0 holds l1.i = l.i & r1.i = r.i;
now
let i;
A23: i <> i0 & l1.i = l.i & r1.i = r.i implies l1.i < r1.i by A6;
i = i0 or i <> i0;
hence l1.i < r1.i by A22,A23;
end;
hence thesis;
end;
suppose for i holds r1.i < l1.i & [l1.i,r1.i] is Gap of G.i;
hence thesis;
end;
end;
then reconsider B1 = cell(l1,r1) as Cell of d,G by A19,Th37;
ex l2,r2 st [l2.i0,r2.i0] is Gap of G.i0 & l2.i0 = l.i0 &
((l2.i0 < r2.i0 & for i st i <> i0 holds l2.i = l.i & r2.i = r.i) or
for i holds r2.i < l2.i & [l2.i,r2.i] is Gap of G.i)
proof
consider r2i0 being Element of REAL such that
A24: [l.i0,r2i0] is Gap of G.i0 by A5,Th15;
per cases by A24,Th13;
suppose
A25: l.i0 < r2i0;
defpred P[Element of Seg d,Element of REAL] means
($1 = i0 implies $2 = r2i0) &
($1 <> i0 implies $2 = r.$1);
A26: for i ex ri being Element of REAL st P[i,ri]
proof
let i;
A27: r.i in REAL by XREAL_0:def 1;
i = i0 or i <> i0;
hence thesis by A27;
end;
consider r2 being Function of Seg d,REAL such that
A28: for i holds P[i,r2.i] from FUNCT_2:sch 3(A26);
reconsider r2 as Element of REAL d by Def3;
take l,r2;
thus thesis by A24,A25,A28;
end;
suppose
A29: r2i0 < l.i0;
consider l2,r2 such that
cell(l2,r2) = infinite-cell(G) and
A30: for i holds r2.i < l2.i & [l2.i,r2.i] is Gap of G.i by Def10;
take l2,r2;
A31: r2.i0 < l2.i0 by A30;
[l2.i0,r2.i0] is Gap of G.i0 by A30;
hence thesis by A24,A29,A30,A31,Th19;
end;
end;
then consider l2,r2 such that
A32: [l2.i0,r2.i0] is Gap of G.i0 and
A33: l2.i0 = l.i0 and
A34: (l2.i0 < r2.i0 & for i st i <> i0 holds l2.i = l.i & r2.i = r.i)
or for i holds r2.i < l2.i & [l2.i,r2.i] is Gap of G.i;
A35: now
let i;
A36: i
<> i0 & l2.i = l.i & r2.i = r.i implies [l2.i,r2.i] is Gap of G.i by A6;
i = i0 or i <> i0;
hence [l2.i,r2.i] is Gap of G.i by A32,A34,A36;
end;
(for i holds l2.i < r2.i) or for i holds r2.i < l2.i
proof
per cases by A34;
suppose
A37: l2.i0 < r2.i0 & for i st i <> i0 holds l2.i = l.i & r2.i = r.i;
now
let i;
A38: i <> i0 & l2.i = l.i & r2.i = r.i implies l2.i < r2.i by A6;
i = i0 or i <> i0;
hence l2.i < r2.i by A37,A38;
end;
hence thesis;
end;
suppose for i holds r2.i < l2.i & [l2.i,r2.i] is Gap of G.i;
hence thesis;
end;
end;
then reconsider B2 = cell(l2,r2) as Cell of d,G by A35,Th37;
take B1,B2;
A c= B1
proof
per cases by A18;
suppose
A39: l1.i0 < r1.i0 & for i st i <> i0 holds l1.i = l.i & r1.i = r.i;
A40: now
let i;
i = i0 or i <> i0 & l1.i = l.i & r1.i = r.i by A39;
hence l1.i <= r1.i by A6,A39;
end;
now
let i;
i = i0 or i <> i0 & l1.i = l.i & r1.i = r.i by A39;
hence l1.i <= l.i & l.i <= r.i & r.i <= r1.i by A4,A17,A40;
end;
hence thesis by A3,A40,Th25;
end;
suppose for i holds r1.i < l1.i & [l1.i,r1.i] is Gap of G.i;
hence thesis by A3,A4,A7,A17,Th27;
end;
end;
hence B1 in star A by A1;
A c= B2
proof
per cases by A34;
suppose
A41: l2.i0 < r2.i0 & for i st i <> i0 holds l2.i = l.i & r2.i = r.i;
A42: now
let i;
i = i0 or i <> i0 & l2.i = l.i & r2.i = r.i by A41;
hence l2.i <= r2.i by A6,A41;
end;
now
let i;
i = i0 or i <> i0 & l2.i = l.i & r2.i = r.i by A41;
hence l2.i <= l.i & l.i <= r.i & r.i <= r2.i by A4,A33,A42;
end;
hence thesis by A3,A42,Th25;
end;
suppose for i holds r2.i < l2.i & [l2.i,r2.i] is Gap of G.i;
hence thesis by A3,A7,A33,Th27;
end;
end;
hence B2 in star A by A1;
A43: l1 <> l2 by A17,A18,A33;
(for i holds l1.i <= r1.i) or for i holds r1.i < l1.i by A21;
hence B1 <> B2 by A43,Th28;
let B be set;
assume
A44: B in star A;
then reconsider B as Cell of d,G by A1;
consider l9,r9 such that
A45: B = cell(l9,r9) and
A46: for i holds [l9.i,r9.i] is Gap of G.i and
A47: (for i holds l9.i < r9.i) or for i holds r9.i < l9.i by Th36;
A48: [l9.i0,r9.i0] is Gap of G.i0 by A46;
A49: A c= B by A44,Th47;
per cases by A47;
suppose
A50: for i holds l9.i < r9.i;
A51: now
let i;
assume
A52: i <> i0;
l9.i < r9.i by A50;
then l.i = l9.i & r.i = r9.i or
l.i = l9.i & r.i = l9.i or l.i = r9.i & r.i = r9.i
by A2,A3,A45,A49,Th42;
hence l9.i = l.i & r9.i = r.i by A6,A52;
end;
thus thesis
proof
A53: l9.i0 < r9.i0 by A50;
per cases by A2,A3,A4,A45,A49,A53,Th42;
suppose
A54: l.i0 = r9.i0 & r.i0 = r9.i0;
then
A55: l9.i0 = l1.i0 by A16,A17,A48,Th18;
reconsider l9,r9,l1,r1 as Function of Seg d,REAL by Def3;
A56: now
let i;
A57: l1.i0 < l.i0 by A50,A54,A55;
then i = i0 or i <> i0 & l9.i = l.i & l1.i = l.i by A17,A18,A51;
hence l9.i = l1.i by A16,A17,A48,A54,Th18;
i = i0 or i <> i0 & r9.i = r.i & r1.i = r.i by A17,A18,A51,A57;
hence r9.i = r1.i by A17,A54;
end;
then l9 = l1 by FUNCT_2:63;
hence thesis by A45,A56,FUNCT_2:63;
end;
suppose
A58: l.i0 = l9.i0 & r.i0 = l9.i0;
then
A59: r9.i0 = r2.i0 by A32,A33,A48,Th17;
reconsider l9,r9,l2,r2 as Function of Seg d,REAL by Def3;
A60: now
let i;
A61: l.i0 < r2.i0 by A50,A58,A59;
then i = i0 or i <> i0 & r9.i = r.i & r2.i = r.i by A33,A34,A51;
hence r9.i = r2.i by A32,A33,A48,A58,Th17;
i = i0 or i <> i0 & l9.i = l.i & l2.i = l.i by A33,A34,A51,A61;
hence l9.i = l2.i by A33,A58;
end;
then l9 = l2 by FUNCT_2:63;
hence thesis by A45,A60,FUNCT_2:63;
end;
end;
end;
suppose
A62: for i holds r9.i < l9.i;
consider i1 such that
A63: l.i1 = l9.i1 & r.i1 = l9.i1 or l.i1 = r9.i1 & r.i1 = r9.i1
by A2,A3,A45,A49,Th43;
A64: i0 = i1 by A6,A63;
thus thesis
proof
per cases by A63,A64;
suppose
A65: l.i0 = r9.i0 & r.i0 = r9.i0;
then l9.i0 = l1.i0 by A16,A17,A48,Th18;
then B1 = infinite-cell(G) by A17,A18,A62,A65,Th45;
hence thesis by A45,A62,Th45;
end;
suppose
A66: l.i0 = l9.i0 & r.i0 = l9.i0;
then r9.i0 = r2.i0 by A32,A33,A48,Th17;
then B2 = infinite-cell(G) by A33,A34,A62,A66,Th45;
hence thesis by A45,A62,Th45;
end;
end;
end;
end;
hence thesis by Th5;
end;
theorem Th52:
for G being Grating of d, B being Cell of (0 + 1),G holds card(del {B}) = 2
proof
A1: 0 + 1 <= d by Def2;
let G be Grating of d, B be Cell of (0 + 1),G;
consider l,r,i0 such that
A2: B = cell(l,r) and
A3: l.i0 < r.i0 or d = 1 & r.i0 < l.i0 and
A4: [l.i0,r.i0] is Gap of G.i0 and
A5: for i st i <> i0 holds l.i = r.i & l.i in G.i by Th40;
ex A1,A2 being set st A1 in del {B} & A2 in del {B} & A1 <> A2 &
for A being set st A in del {B} holds A = A1 or A = A2
proof
for i holds l.i in G.i & r.i in G.i by A1,A2,Th32;
then reconsider A1 = cell(l,l), A2 = cell(r,r) as Cell of 0,G by Th35;
take A1,A2;
A6: A1 = {l} by Th24;
A7: A2 = {r} by Th24;
A8: l in B by A2,Th23;
A9: r in B by A2,Th23;
A10: {l} c= B by A8,ZFMISC_1:31;
{r} c= B by A9,ZFMISC_1:31;
hence A1 in del {B} & A2 in del {B} by A1,A6,A7,A10,Th50;
thus A1 <> A2 by A3,A6,A7,ZFMISC_1:3;
let A be set;
assume
A11: A in del {B};
then reconsider A as Cell of 0,G;
A12: A c= B by A1,A11,Th50;
consider x such that
A13: A = cell(x,x) and
A14: for i holds x.i in G.i by Th34;
A15: x in A by A13,Th23;
per cases by A3;
suppose
A16: l.i0 < r.i0;
A17: now
let i;
i = i0 or i <> i0;
hence l.i <= r.i by A5,A16;
end;
A18: x.i0 in G.i0 by A14;
A19: l.i0 <= x.i0 by A2,A12,A15,A17,Th21;
A20: x.i0 <= r.i0 by A2,A12,A15,A17,Th21;
A21: not (l.i0 < x.i0 & x.i0 < r.i0) by A4,A18,Th13;
A22: now
let i;
assume i <> i0;
then
A23: l.i = r.i by A5;
A24: l.i <= x.i by A2,A12,A15,A17,Th21;
x.i <= r.i by A2,A12,A15,A17,Th21;
hence x.i = l.i & x.i = r.i by A23,A24,XXREAL_0:1;
end;
thus thesis
proof
per cases by A19,A20,A21,XXREAL_0:1;
suppose
A25: x.i0 = l.i0;
reconsider x,l as Function of Seg d,REAL by Def3;
now
let i;
i = i0 or i <> i0;
hence x.i = l.i by A22,A25;
end;
then x = l by FUNCT_2:63;
hence thesis by A13;
end;
suppose
A26: x.i0 = r.i0;
reconsider x,r as Function of Seg d,REAL by Def3;
now
let i;
i = i0 or i <> i0;
hence x.i = r.i by A22,A26;
end;
then x = r by FUNCT_2:63;
hence thesis by A13;
end;
end;
end;
suppose
A27: d = 1 & r.i0 < l.i0;
A28: for i holds i = i0
proof
let i;
A29: 1 <= i by FINSEQ_1:1;
A30: i <= d by FINSEQ_1:1;
A31: 1 <= i0 by FINSEQ_1:1;
A32: i0 <= d by FINSEQ_1:1;
i = 1 by A27,A29,A30,XXREAL_0:1;
hence thesis by A27,A31,A32,XXREAL_0:1;
end;
consider i1 such that
r.i1 < l.i1 and
A33: x.i1 <= r.i1 or l.i1 <= x.i1 by A2,A12,A15,A27,Th22;
A34: i1 = i0 by A28;
A35: x.i0 in G.i0 by A14;
then
A36: not x.i0 < r.i0 by A4,A27,Th13;
A37: not l.i0 < x.i0 by A4,A27,A35,Th13;
thus thesis
proof
per cases by A33,A34,A36,A37,XXREAL_0:1;
suppose
A38: x.i0 = r.i0;
reconsider x,r as Function of Seg d,REAL by Def3;
now
let i;
i = i0 by A28;
hence x.i = r.i by A38;
end;
then x = r by FUNCT_2:63;
hence thesis by A13;
end;
suppose
A39: x.i0 = l.i0;
reconsider x,l as Function of Seg d,REAL by Def3;
now
let i;
i = i0 by A28;
hence x.i = l.i by A39;
end;
then x = l by FUNCT_2:63;
hence thesis by A13;
end;
end;
end;
end;
hence thesis by Th5;
end;
:: theorems
theorem
Omega(G) = 0_(d,G)` & 0_(d,G) = (Omega(G))`
proof
Omega(G) = 0_(d,G)`;
hence thesis;
end;
theorem
for C being Chain of k,G holds C + 0_(k,G) = C;
theorem Th55:
for C being Chain of d,G holds C` = C + Omega(G)
proof
let C be Chain of d,G;
C /\ cells(d,G) = C by XBOOLE_1:28;
hence thesis by XBOOLE_1:100;
end;
theorem Th56:
del 0_(k + 1,G) = 0_(k,G)
proof
now
let A be Cell of k,G;
card(star A /\ 0_(k + 1,G)) = 2* 0;
hence A in del 0_(k + 1,G) iff A in 0_(k,G) by Th48;
end;
hence thesis by SUBSET_1:3;
end;
theorem Th57:
for G being Grating of d9 + 1 holds del Omega(G) = 0_(d9,G)
proof
let G be Grating of d9 + 1;
now
let A be Cell of d9,G;
star A /\ Omega(G) = star A by XBOOLE_1:28;
then card(star A /\ Omega(G)) = 2* 1 by Th51;
hence A in del Omega(G) iff A in 0_(d9,G) by Th48;
end;
hence thesis by SUBSET_1:3;
end;
theorem Th58:
for C1,C2 being Chain of (k + 1),G holds del(C1 + C2) = del C1 + del C2
proof
let C1,C2 be Chain of (k + 1),G;
now
let A be Cell of k,G;
A1: star
A /\ (C1 \+\ C2) = (star A /\ C1) \+\ (star A /\ C2) by XBOOLE_1:112;
A2: A in del(C1 + C2) iff k + 1 <= d & card(star A /\ (C1 \+\ C2)) is odd
by Th48;
A3: A in del(C1) iff k + 1 <= d & card(star A /\ C1) is odd by Th48;
A in del(C2) iff k + 1 <= d & card(star A /\ C2) is odd by Th48;
hence A in del(C1 + C2) iff A in del C1 + del C2 by A1,A2,A3,Th7,XBOOLE_0:1
;
end;
hence thesis by SUBSET_1:3;
end;
theorem Th59:
for G being Grating of d9 + 1, C being Chain of (d9 + 1),G holds
del C` = del C
proof
let G be Grating of d9 + 1, C be Chain of (d9 + 1),G;
thus del C` = del(C + Omega(G)) by Th55
.= del C + del Omega(G) by Th58
.= del C + 0_(d9,G) by Th57
.= del C;
end;
theorem Th60:
for C being Chain of (k + 1 + 1),G holds del (del C) = 0_(k,G)
proof
let C be Chain of (k + 1 + 1),G;
per cases;
suppose
A1: k + 1 + 1 <= d;
then
A2: k + 1 < d by NAT_1:13;
then
A3: k < d by NAT_1:13;
A4: for C being Cell of (k + 1 + 1),G, l,r
st C = cell(l,r) & for i holds l.i <= r.i holds del (del {C}) = 0_(k,G)
proof
let C be Cell of (k + 1 + 1),G, l,r;
assume that
A5: C = cell(l,r) and
A6: for i holds l.i <= r.i;
now
let A be object;
assume
A7: A in del (del {C});
then reconsider A as Cell of k,G;
set BB = star A /\ del {C};
A8: now
let B be Cell of (k + 1),G;
B in BB iff B in star A & B in del {C} by XBOOLE_0:def 4;
hence B in BB iff A c= B & B c= C by A1,Th47,Th50;
end;
A9: card BB is odd by A7,Th48;
consider B being object such that
A10: B in BB by A9,CARD_1:27,XBOOLE_0:def 1;
reconsider B as Cell of (k + 1),G by A10;
A11: A c= B by A8,A10;
B c= C by A8,A10;
then
A12: A c= C by A11;
set i0 = the Element of Seg d;
l.i0 <= r.i0 by A6;
then consider Z being Subset of Seg d such that
A13: card Z = k + 1 + 1 and
A14: for i holds i in Z & l.i < r.i & [l.i,r.i] is Gap of G.i or not
i in Z & l.i = r.i & l.i in G.i
by A1,A5,Th30;
consider l9,r9 such that
A15: A = cell(l9,r9) and
A16: (ex X being Subset of Seg d st card X = k & for i holds (i in X &
l9.i < r9.i & [l9.i,r9.i] is Gap of G.i) or (not i in X & l9.i = r9.i & l9.i in
G.i)) or (k = d & for i holds r9.i < l9.i & [l9.i,r9.i] is Gap of G.i)
by A3,Th29;
l9.i0 <= r9.i0 by A5,A6,A12,A15,Th25;
then consider X being Subset of Seg d such that
A17: card X = k and
A18: for i holds i in X & l9.i < r9.i & [l9.i,r9.i] is Gap of G.i or
not i in X & l9.i = r9.i & l9.i in G.i
by A16;
ex B1,B2 being set st B1 in BB & B2 in BB & B1 <> B2 &
for B being set st B in BB holds B = B1 or B = B2
proof
A19: X c= Z by A5,A12,A14,A15,A18,Th44;
then card(Z \ X) = (k + (1 + 1)) - k by A13,A17,CARD_2:44
.= 2;
then consider i1,i2 being set such that
A20: i1 in Z \ X and
A21: i2 in Z \ X and
A22: i1 <> i2 and
A23: for i being set st i in Z \ X holds i = i1 or i = i2 by Th5;
A24: i1 in Z by A20,XBOOLE_0:def 5;
A25: i2 in Z by A21,XBOOLE_0:def 5;
A26: not i1 in X by A20,XBOOLE_0:def 5;
A27: not i2 in X by A21,XBOOLE_0:def 5;
reconsider i1,i2 as Element of Seg d by A20,A21;
set Y1 = X \/ {i1};
A28: X c= Y1 by XBOOLE_1:7;
{i1} c= Z by A24,ZFMISC_1:31;
then
A29: Y1 c= Z by A19,XBOOLE_1:8;
defpred S[Element of Seg d,Element of REAL] means
($1 in Y1 implies $2 = l.$1) & (not $1 in Y1 implies $2 = l9.$1);
A30: for i ex xi being Element of REAL st S[i,xi]
proof
let i;
A31: l.i in REAL & l9.i in REAL by XREAL_0:def 1;
i in Y1 or not i in Y1;
hence thesis by A31;
end;
consider l1 being Function of Seg d,REAL such that
A32: for i holds S[i,l1.i] from FUNCT_2:sch 3(A30);
defpred R[Element of Seg d,Element of REAL] means
($1 in Y1 implies $2 = r.$1) & (not $1 in Y1 implies $2 = r9.$1);
A33: for i ex xi being Element of REAL st R[i,xi]
proof
let i;
A34: r.i in REAL & r9.i in REAL by XREAL_0:def 1;
i in Y1 or not i in Y1;
hence thesis by A34;
end;
consider r1 being Function of Seg d,REAL such that
A35: for i holds R[i,r1.i] from FUNCT_2:sch 3(A33);
reconsider l1,r1 as Element of REAL d by Def3;
A36: for i holds l1.i <= r1.i
proof
let i;
l1.i = l.i & r1.i = r.i or l1.i = l9.i & r1.i = r9.i by A32,A35;
hence thesis by A14,A18;
end;
A37: card Y1 = card X + card {i1} by A26,CARD_2:40,ZFMISC_1:50
.= k + 1 by A17,CARD_1:30;
for i holds i in Y1 & l1.i < r1.i & [l1.i,r1.i] is Gap of G.i or
not i in Y1 & l1.i = r1.i & l1.i in G.i
proof
let i;
per cases;
suppose
A38: i in Y1;
then
A39: l1.i = l.i by A32;
r1.i = r.i by A35,A38;
hence thesis by A14,A29,A38,A39;
end;
suppose
A40: not i in Y1;
then
A41: l1.i = l9.i by A32;
A42: r1.i = r9.i by A35,A40;
not i in X by A28,A40;
hence thesis by A18,A40,A41,A42;
end;
end;
then reconsider B1 = cell(l1,r1) as Cell of (k + 1),G by A2,A37,Th30;
set Y2 = X \/ {i2};
A43: X c= Y2 by XBOOLE_1:7;
{i2} c= Z by A25,ZFMISC_1:31;
then
A44: Y2 c= Z by A19,XBOOLE_1:8;
defpred P[Element of Seg d,Element of REAL] means
($1 in Y2 implies $2 = l.$1) & (not $1 in Y2 implies $2 = l9.$1);
A45: for i ex xi being Element of REAL st P[i,xi]
proof
let i;
A46: l.i in REAL & l9.i in REAL by XREAL_0:def 1;
i in Y2 or not i in Y2;
hence thesis by A46;
end;
consider l2 being Function of Seg d,REAL such that
A47: for i holds P[i,l2.i] from FUNCT_2:sch 3(A45);
defpred R[Element of Seg d,Element of REAL] means
($1 in Y2 implies $2 = r.$1) & (not $1 in Y2 implies $2 = r9.$1);
A48: for i ex xi being Element of REAL st R[i,xi]
proof
let i;
A49: r.i in REAL & r9.i in REAL by XREAL_0:def 1;
i in Y2 or not i in Y2;
hence thesis by A49;
end;
consider r2 being Function of Seg d,REAL such that
A50: for i holds R[i,r2.i] from FUNCT_2:sch 3(A48);
reconsider l2,r2 as Element of REAL d by Def3;
A51: card Y2 = card X + card {i2} by A27,CARD_2:40,ZFMISC_1:50
.= k + 1 by A17,CARD_1:30;
for i holds i in Y2 & l2.i < r2.i & [l2.i,r2.i] is Gap of G.i or
not i in Y2 & l2.i = r2.i & l2.i in G.i
proof
let i;
per cases;
suppose
A52: i in Y2;
then
A53: l2.i = l.i by A47;
r2.i = r.i by A50,A52;
hence thesis by A14,A44,A52,A53;
end;
suppose
A54: not i in Y2;
then
A55: l2.i = l9.i by A47;
A56: r2.i = r9.i by A50,A54;
not i in X by A43,A54;
hence thesis by A18,A54,A55,A56;
end;
end;
then reconsider B2 = cell(l2,r2) as Cell of (k + 1),G by A2,A51,Th30;
take B1,B2;
A57: for i holds l1.i <= l9.i & l9.i <= r9.i & r9.i <= r1.i &
l.i <= l1.i & l1.i <= r1.i & r1.i <= r.i
proof
let i;
per cases;
suppose
A58: i in Y1;
then
A59: l1.i = l.i by A32;
r1.i = r.i by A35,A58;
hence thesis by A5,A6,A12,A15,A59,Th25;
end;
suppose
A60: not i in Y1;
then
A61: l1.i = l9.i by A32;
r1.i = r9.i by A35,A60;
hence thesis by A5,A6,A12,A15,A61,Th25;
end;
end;
then
A62: A c= B1 by A15,Th25;
B1 c= C by A5,A6,A57,Th25;
hence B1 in BB by A8,A62;
A63: for i holds l2.i <= l9.i & l9.i <= r9.i & r9.i <= r2.i &
l.i <= l2.i & l2.i <= r2.i & r2.i <= r.i
proof
let i;
per cases;
suppose
A64: i in Y2;
then
A65: l2.i = l.i by A47;
r2.i = r.i by A50,A64;
hence thesis by A5,A6,A12,A15,A65,Th25;
end;
suppose
A66: not i in Y2;
then
A67: l2.i = l9.i by A47;
r2.i = r9.i by A50,A66;
hence thesis by A5,A6,A12,A15,A67,Th25;
end;
end;
then
A68: A c= B2 by A15,Th25;
B2 c= C by A5,A6,A63,Th25;
hence B2 in BB by A8,A68;
i1 in {i1} by TARSKI:def 1;
then
A69: i1 in Y1 by XBOOLE_0:def 3;
A70: not i1 in X by A20,XBOOLE_0:def 5;
not i1 in {i2} by A22,TARSKI:def 1;
then
A71: not i1 in Y2 by A70,XBOOLE_0:def 3;
A72: l1.i1 = l.i1 by A32,A69;
A73: r1.i1 = r.i1 by A35,A69;
A74: l2.i1 = l9.i1 by A47,A71;
A75: r2.i1 = r9.i1 by A50,A71;
l.i1 < r.i1 by A14,A24;
then l1 <> l2 or r1 <> r2 by A18,A26,A72,A73,A74,A75;
hence B1 <> B2 by A36,Th28;
let B be set;
assume
A76: B in BB;
then reconsider B as Cell of (k + 1),G;
A77: A c= B by A8,A76;
A78: B c= C by A8,A76;
consider l99,r99 such that
A79: B = cell(l99,r99) and
A80: (ex Y being Subset of Seg d st card Y = k + 1 & for i holds (i in
Y & l99.i < r99.i & [l99.i,r99.i] is Gap of G.i) or (not i in Y & l99.i = r99.i
& l99.i in G.i)) or (k + 1 = d & for i holds r99.i < l99.i & [l99.i,r99.i] is
Gap of G.i)
by A2,Th29;
l99.i0 <= r99.i0 by A5,A6,A78,A79,Th25;
then consider Y being Subset of Seg d such that
A81: card Y = k + 1 and
A82: for i holds i in Y & l99.i < r99.i & [l99.i,r99.i] is Gap of G.i
or not i in Y & l99.i = r99.i & l99.i in G.i
by A80;
A83: X c= Y by A15,A18,A77,A79,A82,Th44;
A84: Y c= Z by A5,A14,A78,A79,A82,Th44;
card(Y \ X) = (k + 1) - k by A17,A81,A83,CARD_2:44
.= 1;
then consider i9 being object such that
A85: Y \ X = {i9} by CARD_2:42;
A86: i9 in Y \ X by A85,TARSKI:def 1;
then reconsider i9 as Element of Seg d;
A87: i9 in Y by A86,XBOOLE_0:def 5;
not i9 in X by A86,XBOOLE_0:def 5;
then
A88: i9 in Z \ X by A84,A87,XBOOLE_0:def 5;
A89: Y = X \/ Y by A83,XBOOLE_1:12
.= X \/ {i9} by A85,XBOOLE_1:39;
per cases by A23,A88,A89;
suppose
A90: Y = Y1;
reconsider l99,r99,l1,r1 as Function of Seg d,REAL by Def3;
A91: now
let i;
i in Y or not i in Y;
then l99.i = l.i & l1.i = l.i & r99.i = r.i & r1.i = r.i or
l99.i = l9.i & l1.i = l9.i & r99.i = r9.i & r1.i = r9.i
by A5,A14,A15,A18,A32,A35,A77,A78,A79,A82,A90,Th44;
hence l99.i = l1.i & r99.i = r1.i;
end;
then l99 = l1 by FUNCT_2:63;
hence thesis by A79,A91,FUNCT_2:63;
end;
suppose
A92: Y = Y2;
reconsider l99,r99,l2,r2 as Function of Seg d,REAL by Def3;
A93: now
let i;
i in Y or not i in Y;
then l99.i = l.i & l2.i = l.i & r99.i = r.i & r2.i = r.i or
l99.i = l9.i & l2.i = l9.i & r99.i = r9.i & r2.i = r9.i
by A5,A14,A15,A18,A47,A50,A77,A78,A79,A82,A92,Th44;
hence l99.i = l2.i & r99.i = r2.i;
end;
then l99 = l2 by FUNCT_2:63;
hence thesis by A79,A93,FUNCT_2:63;
end;
end;
then card BB = 2* 1 by Th5;
hence contradiction by A7,Th48;
end;
hence thesis by XBOOLE_0:def 1;
end;
A94: for C1,C2 being Chain of (k + 1 + 1),G
st del (del C1) = 0_(k,G) & del (del C2) = 0_(k,G) holds
del (del(C1 + C2)) = 0_(k,G)
proof
let C1,C2 be Chain of (k + 1 + 1),G;
assume that
A95: del (del C1) = 0_(k,G) and
A96: del (del C2) = 0_(k,G);
thus del (del(C1 + C2)) = del (del C1 + del C2) by Th58
.= 0_(k,G) + 0_(k,G) by A95,A96,Th58
.= 0_(k,G);
end;
defpred P[Chain of k+1+1,G] means del (del $1) = 0_(k,G);
del (del 0_(k + 1 + 1,G)) = del 0_(k + 1,G) by Th56
.= 0_(k,G) by Th56;
then
A97: P[0_(k+1+1,G)];
for A being Cell of (k + 1 + 1),G holds del (del {A}) = 0_(k,G)
proof
let A be Cell of (k + 1 + 1),G;
consider l,r such that
A98: A = cell(l,r) and
A99: (ex X being Subset of Seg d st card X = k + 1 + 1 & for i holds (
i in X & l.i < r.i & [l.i,r.i] is Gap of G.i) or (not i in X & l.i = r.i & l.i
in G.i)) or (k + 1 + 1 = d & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i)
by A1,Th29;
per cases by A99;
suppose ex X being Subset of Seg d st card X = k + 1 + 1 &
for i holds i in X & l.i < r.i & [l.i,r.i] is Gap of G.i or
not i in X & l.i = r.i & l.i in G.i;
then for i holds l.i <= r.i;
hence thesis by A4,A98;
end;
suppose
A100: k + 1 + 1 = d & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i;
then
A101: A = infinite-cell(G) by A98,Th46;
set C = {A}`;
A102: for A being Cell of k+1+1,G st A in C holds P[{A}]
proof
let A9 be Cell of (k + 1 + 1),G;
assume A9 in C;
then not A9 in {A} by XBOOLE_0:def 5;
then
A103: A9 <> infinite-cell(G) by A101,TARSKI:def 1;
consider l9,r9 such that
A104: A9 = cell(l9,r9) and
A105: (ex X being Subset of Seg d st card X = k + 1 + 1 & for i holds (
i in X & l9.i < r9.i & [l9.i,r9.i] is Gap of G.i) or (not i in X & l9.i = r9.i
& l9.i in G.i)) or (k + 1 + 1 = d & for i holds r9.i < l9.i & [l9.i,r9.i] is
Gap of G.i)
by A1,Th29;
per cases by A105;
suppose ex X being Subset of Seg d st card X = k + 1 + 1 &
for i holds i in X & l9.i < r9.i & [l9.i,r9.i] is Gap of G.i or
not i in X & l9.i = r9.i & l9.i in G.i;
then for i holds l9.i <= r9.i;
hence thesis by A4,A104;
end;
suppose for i holds r9.i < l9.i & [l9.i,r9.i] is Gap of G.i;
hence thesis by A103,A104,Th46;
end;
end;
A106: for C1,C2 being Chain of k+1+1,G st C1 c= C & C2 c= C &
P[C1] & P[C2] holds P[C1 + C2] by A94;
P[C] from ChainInd(A97,A102,A106);
hence thesis by A100,Th59;
end;
end;
then
A107: for A being Cell of k+1+1,G st A in C holds P[{A}];
A108: for C1,C2 being Chain of k+1+1,G st C1 c= C & C2 c= C &
P[C1] & P[C2] holds P[C1 + C2] by A94;
thus P[C] from ChainInd(A97,A107,A108);
end;
suppose k + 1 + 1 > d;
then del C = 0_(k + 1,G) by Th49;
hence thesis by Th56;
end;
end;
:: cycles
definition
let d,G,k;
mode Cycle of k,G -> Chain of k,G means
:Def14:
k = 0 & card it is even or
ex k9 st k = k9 + 1 & ex C being Chain of (k9 + 1),G st C = it &
del C = 0_(k9,G);
existence
proof
per cases by NAT_1:6;
suppose
A1: k = 0;
take 0_(k,G);
thus thesis by A1;
end;
suppose ex k9 being Nat st k = k9 + 1;
then consider k9 being Nat such that
A2: k = k9 + 1;
reconsider k9 as Element of NAT by ORDINAL1:def 12;
take C9 = 0_(k,G);
now
take k9;
thus k = k9 + 1 by A2;
reconsider C = C9 as Chain of (k9 + 1),G by A2;
take C;
thus C = C9 & del C = 0_(k9,G) by A2,Th56;
end;
hence thesis;
end;
end;
end;
theorem Th61:
for C being Chain of (k + 1),G holds
C is Cycle of (k + 1),G iff del C = 0_(k,G)
proof
let C be Chain of (k + 1),G;
hereby
assume C is Cycle of (k + 1),G;
then ex k9 st ( k + 1 = k9 + 1)&( ex C9 being Chain of (k9 + 1),
G st C9 = C & del C9 = 0_(k9,G)) by Def14;
hence del C = 0_(k,G);
end;
thus thesis by Def14;
end;
theorem
k > d implies for C being Chain of k,G holds C is Cycle of k,G
proof
assume
A1: k > d;
let C be Chain of k,G;
consider k9 being Nat such that
A2: k = k9 + 1 by A1,NAT_1:6;
reconsider k9 as Element of NAT by ORDINAL1:def 12;
reconsider C9 = C as Chain of (k9 + 1),G by A2;
del C9 = 0_(k9,G) by A1,A2,Th49;
hence thesis by A2,Def14;
end;
theorem Th63:
for C being Chain of 0,G holds C is Cycle of 0,G iff card C is even
proof
let C be Chain of 0,G;
hereby
assume C is Cycle of 0,G;
then 0 = 0 & card C is even or
ex k9 st 0 = k9 + 1 & ex C9 being Chain of (k9 + 1),G st C9 = C &
del C9 = 0_(k9,G) by Def14;
hence card C is even;
end;
thus thesis by Def14;
end;
definition
let d,G,k;
let C be Cycle of (k + 1),G;
redefine func del C equals :: redefines del (CHAIN_1, definition)
0_(k,G);
compatibility by Th61;
end;
definition
let d,G,k;
redefine func 0_(k,G) -> Cycle of k,G; :: redefines 0_ (CHAIN_1, definition)
coherence
proof
per cases by NAT_1:6;
suppose
A1: k = 0;
card {} = 2* 0;
hence thesis by A1,Def14;
end;
suppose ex k9 being Nat st k = k9 + 1;
then consider k9 being Nat such that
A2: k = k9 + 1;
reconsider k9 as Element of NAT by ORDINAL1:def 12;
del 0_(k9 + 1,G) = 0_(k9,G) by Th56;
hence thesis by A2,Def14;
end;
end;
end;
definition
let d,G;
redefine func Omega(G) -> Cycle of d,G; :: redefines Omega (CHAIN_1, definition)
coherence
proof
consider d9 being Nat such that
A1: d = d9 + 1 by NAT_1:6;
reconsider d9 as Element of NAT by ORDINAL1:def 12;
reconsider G as Grating of d9 + 1 by A1;
del Omega(G) = 0_(d9,G) by Th57;
hence thesis by A1,Def14;
end;
end;
definition
let d,G,k;
let C1,C2 be Cycle of k,G;
redefine func C1 + C2 -> Cycle of k,G; :: redefines + (CHAIN_1, synonym) → \+\ (XBOOLE_0, definition)
coherence
proof
per cases by NAT_1:6;
suppose
A1: k = 0;
then
A2: card C1 is even by Th63;
card C2 is even by A1,Th63;
then card(C1 + C2) is even by A2,Th7;
hence C1 + C2 is Cycle of k,G by A1,Th63;
end;
suppose ex k9 being Nat st k = k9 + 1;
then consider k9 being Nat such that
A3: k = k9 + 1;
reconsider k9 as Element of NAT by ORDINAL1:def 12;
reconsider C1,C2 as Cycle of (k9 + 1),G by A3;
A4: del C1 = 0_(k9,G);
del C2 = 0_(k9,G);
then del(C1 + C2) = 0_(k9,G) + 0_(k9,G) by A4,Th58
.= 0_(k9,G);
hence thesis by A3,Th61;
end;
end;
end;
theorem
for C being Cycle of d,G holds C` is Cycle of d,G
proof
let C be Cycle of d,G;
consider d9 being Nat such that
A1: d = d9 + 1 by NAT_1:6;
reconsider d9 as Element of NAT by ORDINAL1:def 12;
reconsider G as Grating of d9 + 1 by A1;
reconsider C as Cycle of (d9 + 1),G by A1;
del C = 0_(d9,G);
then del C` = 0_(d9,G) by Th59;
hence thesis by A1,Th61;
end;
definition
let d,G,k;
let C be Chain of (k + 1),G;
redefine func del C -> Cycle of k,G; :: redefines del (CHAIN_1, definition)
coherence
proof
per cases by NAT_1:6;
suppose
A1: k = 0;
defpred P[Chain of (k + 1),G] means del $1 is Cycle of k,G;
del 0_(k + 1,G) = 0_(k,G);
then
A2: P[0_(k + 1,G)];
now
let B be Cell of (0 + 1),G;
assume B in C;
card(del {B}) = 2* 1 by Th52;
hence del {B} is Cycle of 0,G by Def14;
end;
then
A3: for A being Cell of (k + 1),G st A in C holds P[{A}] by A1;
A4: for C1,C2 being Chain of (k + 1),G st C1 c= C & C2 c= C &
P[C1] & P[C2] holds P[C1 + C2]
proof
let C1,C2 be Chain of (k + 1),G;
assume that C1 c= C and C2 c= C and
A5: P[C1] and
A6: P[C2];
reconsider C19 = del C1, C29 = del C2 as Cycle of k,G by A5,A6;
del(C1 + C2) = C19 + C29 by Th58;
hence thesis;
end;
thus P[C] from ChainInd(A2,A3,A4);
end;
suppose ex k9 being Nat st k = k9 + 1;
then consider k9 being Nat such that
A7: k = k9 + 1;
reconsider k9 as Element of NAT by ORDINAL1:def 12;
reconsider C as Chain of (k9 + 1 + 1),G by A7;
del (del C) = 0_(k9,G) by Th60;
hence thesis by A7,Th61;
end;
end;
end;
begin :: groups and homomorphisms
definition
let d,G,k;
func Chains(k,G) -> strict AbGroup means
:Def16:
the carrier of it = bool(cells(k,G)) & 0.it = 0_(k,G) &
for A,B being Element of it, A9,B9 being Chain of k,G
st A = A9 & B = B9 holds A + B = A9 + B9;
existence
proof
deffunc f(Chain of k,G, Chain of k,G) = $1 + $2;
consider op being BinOp of bool(cells(k,G)) such that
A1: for A,B being Chain of k,G holds op.(A,B) = f(A,B) from BINOP_1:sch 4;
set ch = addLoopStr(#bool(cells(k,G)),op,0_(k,G)#);
A2: ch is add-associative
proof
let A,B,C be Element of ch;
reconsider A9 = A, B9 = B, C9 = C as Chain of k,G;
thus (A + B) + C = op.(A9 + B9,C) by A1
.= (A9 + B9) + C9 by A1
.= A9 + (B9 + C9) by XBOOLE_1:91
.= op.(A,B9 + C9) by A1
.= A + (B + C) by A1;
end;
A3: ch is right_zeroed
proof
let A be Element of ch;
reconsider A9 = A as Chain of k,G;
thus A + 0.ch = A9 + 0_(k,G) by A1
.= A;
end;
A4: ch is right_complementable
proof
let A be Element of ch;
reconsider A9 = A as Chain of k,G;
take A;
thus A + A = A9 + A9 by A1
.= 0.ch by XBOOLE_1:92;
end;
ch is Abelian
proof
let A,B be Element of ch;
reconsider A9 = A, B9 = B as Chain of k,G;
thus A + B = A9 + B9 by A1
.= B + A by A1;
end;
then reconsider ch as strict AbGroup by A2,A3,A4;
take ch;
thus the carrier of ch = bool(cells(k,G));
thus 0.ch = 0_(k,G);
let A,B be Element of ch, A9,B9 be Chain of k,G;
assume that
A5: A = A9 and
A6: B = B9;
thus thesis by A1,A5,A6;
end;
uniqueness
proof
let C1,C2 be strict AbGroup;
assume that
A7: the carrier of C1 = bool(cells(k,G)) and
A8: 0.C1 = 0_(k,G) and
A9: for A,B being Element of C1, A9,B9 being Chain of k,G st A = A9 &
B = B9 holds A + B = A9 + B9 and
A10: the carrier of C2 = bool(cells(k,G)) and
A11: 0.C2 = 0_(k,G) and
A12: for A,B being Element of C2, A9,B9 being Chain of k,G st A = A9 &
B = B9 holds A + B = A9 + B9;
set X = [:bool(cells(k,G)),bool(cells(k,G)):];
reconsider op1 = the addF of C1, op2 = the addF of C2 as
Function of X,bool(cells(k,G)) by A7,A10;
now
let AB be Element of X;
consider A9,B9 being Chain of k,G such that
A13: AB = [A9,B9] by DOMAIN_1:1;
reconsider A1 = A9, B1 = B9 as Element of C1 by A7;
reconsider A2 = A9, B2 = B9 as Element of C2 by A10;
thus op1.AB = A1 + B1 by A13
.= A9 + B9 by A9
.= A2 + B2 by A12
.= op2.AB by A13;
end;
hence thesis by A7,A8,A10,A11,FUNCT_2:63;
end;
end;
definition
let d,G,k;
mode GrChain of k,G is Element of Chains(k,G);
end;
theorem
for x being set holds x is Chain of k,G iff x is GrChain of k,G by Def16;
definition
let d,G,k;
func del(k,G) -> Homomorphism of Chains(k + 1,G),Chains(k,G) means
for A being Element of Chains(k + 1,G), A9 being Chain of (k + 1),G
st A = A9 holds it.A = del A9;
existence
proof
deffunc f(Subset of cells(k + 1,G)) = del $1;
consider f being
Function of bool(cells(k + 1,G)),bool(cells(k,G)) such that
A1: for
A being Subset of cells(k + 1,G) holds f.A = f(A) from FUNCT_2:sch 4;
A2: the carrier of Chains(k + 1,G) = bool(cells(k + 1,G)) by Def16;
the carrier of Chains(k,G) = bool(cells(k,G)) by Def16;
then reconsider f9 = f as Function of Chains(k + 1,G),Chains(k,G) by A2;
now
let A,B being Element of Chains(k + 1,G);
reconsider A9 = A, B9 = B as Chain of (k + 1),G by Def16;
thus f.(A + B) = f.(A9 + B9) by Def16
.= del(A9 + B9) by A1
.= del A9 + del B9 by Th58
.= del A9 + f.B9 by A1
.= f.A9 + f.B9 by A1
.= f9.A + f9.B by Def16;
end; then
f9 is additive by VECTSP_1:def 20;
then reconsider f9 as Homomorphism of Chains(k + 1,G),Chains(k,G);
take f9;
thus thesis by A1;
end;
uniqueness
proof
let f,g be Homomorphism of Chains(k + 1,G),Chains(k,G);
assume
A3: for A being Element of Chains(k + 1,G), A9 being Chain of (k + 1),G
st A = A9 holds f.A = del A9;
assume
A4: for A being Element of Chains(k + 1,G), A9 being Chain of (k + 1),G
st A = A9 holds g.A = del A9;
now
let A be Element of Chains(k + 1,G);
reconsider A9 = A as Element of Chains(k + 1,G);
reconsider A99 = A as Chain of (k + 1),G by Def16;
f.A9 = del A99 by A3
.= g.A9 by A4;
hence f.A = g.A;
end;
hence f = g by FUNCT_2:63;
end;
end;