let k be Element of NAT ; :: thesis: for d being non zero Element of NAT
for G being Grating of d
for C being Chain of ((k + 1) + 1),G holds del (del C) = 0_ k,G
let d be non zero Element of NAT ; :: thesis: for G being Grating of d
for C being Chain of ((k + 1) + 1),G holds del (del C) = 0_ k,G
let G be Grating of d; :: thesis: for C being Chain of ((k + 1) + 1),G holds del (del C) = 0_ k,G
let C be Chain of ((k + 1) + 1),G; :: thesis: del (del C) = 0_ k,G
per cases
( (k + 1) + 1 <= d or (k + 1) + 1 > d )
;
suppose A1:
(k + 1) + 1
<= d
;
:: thesis: del (del C) = 0_ k,Gthen 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 for
l,
r being
Element of
REAL d st
C = cell l,
r & ( for
i being
Element of
Seg d holds
l . i <= r . i ) holds
del (del {C}) = 0_ k,
G
proof
let C be
Cell of
((k + 1) + 1),
G;
:: thesis: for l, r being Element of REAL d st C = cell l,r & ( for i being Element of Seg d holds l . i <= r . i ) holds
del (del {C}) = 0_ k,Glet l,
r be
Element of
REAL d;
:: thesis: ( C = cell l,r & ( for i being Element of Seg d holds l . i <= r . i ) implies del (del {C}) = 0_ k,G )
assume A5:
(
C = cell l,
r & ( for
i being
Element of
Seg d holds
l . i <= r . i ) )
;
:: thesis: del (del {C}) = 0_ k,G
now let A be
set ;
:: thesis: not A in del (del {C})assume A6:
A in del (del {C})
;
:: thesis: contradictionthen reconsider A =
A as
Cell of
k,
G ;
set BB =
(star A) /\ (del {C});
A8:
not
card ((star A) /\ (del {C})) is
even
by A6, Th52;
2
* 0 is
even
;
then consider B being
set such that A9:
B in (star A) /\ (del {C})
by A8, CARD_1:47, XBOOLE_0:def 1;
reconsider B =
B as
Cell of
(k + 1),
G by A9;
(
A c= B &
B c= C )
by A7, A9;
then A10:
A c= C
by XBOOLE_1:1;
consider i0 being
Element of
Seg d;
l . i0 <= r . i0
by A5;
then consider Z being
Subset of
(Seg d) such that A11:
(
card Z = (k + 1) + 1 & ( for
i being
Element of
Seg d 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, Th34;
consider l',
r' being
Element of
REAL d such that A12:
(
A = cell l',
r' & ( ex
X being
Subset of
(Seg d) st
(
card X = k & ( for
i being
Element of
Seg d 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 being
Element of
Seg d holds
(
r' . i < l' . i &
[(l' . i),(r' . i)] is
Gap of
G . i ) ) ) ) )
by A3, Th33;
l' . i0 <= r' . i0
by A5, A10, A12, Th29;
then consider X being
Subset of
(Seg d) such that A13:
(
card X = k & ( for
i being
Element of
Seg d 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 A12;
ex
B1,
B2 being
set st
(
B1 in (star A) /\ (del {C}) &
B2 in (star A) /\ (del {C}) &
B1 <> B2 & ( for
B being
set holds
( not
B in (star A) /\ (del {C}) or
B = B1 or
B = B2 ) ) )
proof
A14:
(
X c= Z & ( for
i being
Element of
Seg d st (
i in X or not
i in Z ) holds
(
l' . i = l . i &
r' . i = r . i ) ) & ( for
i being
Element of
Seg d st not
i in X &
i in Z & not (
l' . i = l . i &
r' . i = l . i ) holds
(
l' . i = r . i &
r' . i = r . i ) ) )
by A5, A10, A11, A12, A13, Th48;
then card (Z \ X) =
(k + (1 + 1)) - k
by A11, A13, CARD_2:63
.=
2
;
then consider i1,
i2 being
set such that A15:
(
i1 in Z \ X &
i2 in Z \ X &
i1 <> i2 & ( for
i being
set holds
( not
i in Z \ X or
i = i1 or
i = i2 ) ) )
by Th6;
A16:
(
i1 in Z &
i2 in Z & not
i1 in X & not
i2 in X )
by A15, XBOOLE_0:def 5;
reconsider i1 =
i1,
i2 =
i2 as
Element of
Seg d by A15;
set Y1 =
X \/ {i1};
A17:
X c= X \/ {i1}
by XBOOLE_1:7;
{i1} c= Z
by A16, ZFMISC_1:37;
then A18:
X \/ {i1} c= Z
by A14, XBOOLE_1:8;
defpred S1[
Element of
Seg d,
Real]
means ( ( $1
in X \/ {i1} implies $2
= l . $1 ) & ( not $1
in X \/ {i1} implies $2
= l' . $1 ) );
A19:
for
i being
Element of
Seg d ex
xi being
Real st
S1[
i,
xi]
consider l1 being
Function of
(Seg d),
REAL such that A20:
for
i being
Element of
Seg d holds
S1[
i,
l1 . i]
from FUNCT_2:sch 3(A19);
defpred S2[
Element of
Seg d,
Real]
means ( ( $1
in X \/ {i1} implies $2
= r . $1 ) & ( not $1
in X \/ {i1} implies $2
= r' . $1 ) );
A21:
for
i being
Element of
Seg d ex
xi being
Real st
S2[
i,
xi]
consider r1 being
Function of
(Seg d),
REAL such that A22:
for
i being
Element of
Seg d holds
S2[
i,
r1 . i]
from FUNCT_2:sch 3(A21);
reconsider l1 =
l1,
r1 =
r1 as
Element of
REAL d by Def4;
A23:
for
i being
Element of
Seg d holds
l1 . i <= r1 . i
A24:
card (X \/ {i1}) =
(card X) + (card {i1})
by A16, CARD_2:53, ZFMISC_1:56
.=
k + 1
by A13, CARD_1:50
;
for
i being
Element of
Seg d holds
( (
i in X \/ {i1} &
l1 . i < r1 . i &
[(l1 . i),(r1 . i)] is
Gap of
G . i ) or ( not
i in X \/ {i1} &
l1 . i = r1 . i &
l1 . i in G . i ) )
then reconsider B1 =
cell l1,
r1 as
Cell of
(k + 1),
G by A2, A24, Th34;
set Y2 =
X \/ {i2};
A28:
X c= X \/ {i2}
by XBOOLE_1:7;
{i2} c= Z
by A16, ZFMISC_1:37;
then A29:
X \/ {i2} c= Z
by A14, XBOOLE_1:8;
defpred S3[
Element of
Seg d,
Real]
means ( ( $1
in X \/ {i2} implies $2
= l . $1 ) & ( not $1
in X \/ {i2} implies $2
= l' . $1 ) );
A30:
for
i being
Element of
Seg d ex
xi being
Real st
S3[
i,
xi]
consider l2 being
Function of
(Seg d),
REAL such that A31:
for
i being
Element of
Seg d holds
S3[
i,
l2 . i]
from FUNCT_2:sch 3(A30);
defpred S4[
Element of
Seg d,
Real]
means ( ( $1
in X \/ {i2} implies $2
= r . $1 ) & ( not $1
in X \/ {i2} implies $2
= r' . $1 ) );
A32:
for
i being
Element of
Seg d ex
xi being
Real st
S4[
i,
xi]
consider r2 being
Function of
(Seg d),
REAL such that A33:
for
i being
Element of
Seg d holds
S4[
i,
r2 . i]
from FUNCT_2:sch 3(A32);
reconsider l2 =
l2,
r2 =
r2 as
Element of
REAL d by Def4;
A34:
card (X \/ {i2}) =
(card X) + (card {i2})
by A16, CARD_2:53, ZFMISC_1:56
.=
k + 1
by A13, CARD_1:50
;
for
i being
Element of
Seg d holds
( (
i in X \/ {i2} &
l2 . i < r2 . i &
[(l2 . i),(r2 . i)] is
Gap of
G . i ) or ( not
i in X \/ {i2} &
l2 . i = r2 . i &
l2 . i in G . i ) )
then reconsider B2 =
cell l2,
r2 as
Cell of
(k + 1),
G by A2, A34, Th34;
take
B1
;
:: thesis: ex B2 being set st
( B1 in (star A) /\ (del {C}) & B2 in (star A) /\ (del {C}) & B1 <> B2 & ( for B being set holds
( not B in (star A) /\ (del {C}) or B = B1 or B = B2 ) ) )
take
B2
;
:: thesis: ( B1 in (star A) /\ (del {C}) & B2 in (star A) /\ (del {C}) & B1 <> B2 & ( for B being set holds
( not B in (star A) /\ (del {C}) or B = B1 or B = B2 ) ) )
for
i being
Element of
Seg d holds
(
l1 . i <= l' . i &
l' . i <= r' . i &
r' . i <= r1 . i &
l . i <= l1 . i &
l1 . i <= r1 . i &
r1 . i <= r . i )
then
(
A c= B1 &
B1 c= C )
by A5, A12, Th29;
hence
B1 in (star A) /\ (del {C})
by A7;
:: thesis: ( B2 in (star A) /\ (del {C}) & B1 <> B2 & ( for B being set holds
( not B in (star A) /\ (del {C}) or B = B1 or B = B2 ) ) )
for
i being
Element of
Seg d holds
(
l2 . i <= l' . i &
l' . i <= r' . i &
r' . i <= r2 . i &
l . i <= l2 . i &
l2 . i <= r2 . i &
r2 . i <= r . i )
then
(
A c= B2 &
B2 c= C )
by A5, A12, Th29;
hence
B2 in (star A) /\ (del {C})
by A7;
:: thesis: ( B1 <> B2 & ( for B being set holds
( not B in (star A) /\ (del {C}) or B = B1 or B = B2 ) ) )
then
(
l1 <> l2 or
r1 <> r2 )
;
hence
B1 <> B2
by A23, Th32;
:: thesis: for B being set holds
( not B in (star A) /\ (del {C}) or B = B1 or B = B2 )
let B be
set ;
:: thesis: ( not B in (star A) /\ (del {C}) or B = B1 or B = B2 )
assume A38:
B in (star A) /\ (del {C})
;
:: thesis: ( B = B1 or B = B2 )
then reconsider B =
B as
Cell of
(k + 1),
G ;
A39:
(
A c= B &
B c= C )
by A7, A38;
consider l'',
r'' being
Element of
REAL d such that A40:
(
B = cell l'',
r'' & ( ex
Y being
Subset of
(Seg d) st
(
card Y = k + 1 & ( for
i being
Element of
Seg d holds
( (
i in Y &
l'' . i < r'' . i &
[(l'' . i),(r'' . i)] is
Gap of
G . i ) or ( not
i in Y &
l'' . i = r'' . i &
l'' . i in G . i ) ) ) ) or (
k + 1
= d & ( for
i being
Element of
Seg d holds
(
r'' . i < l'' . i &
[(l'' . i),(r'' . i)] is
Gap of
G . i ) ) ) ) )
by A2, Th33;
l'' . i0 <= r'' . i0
by A5, A39, A40, Th29;
then consider Y being
Subset of
(Seg d) such that A41:
(
card Y = k + 1 & ( for
i being
Element of
Seg d holds
( (
i in Y &
l'' . i < r'' . i &
[(l'' . i),(r'' . i)] is
Gap of
G . i ) or ( not
i in Y &
l'' . i = r'' . i &
l'' . i in G . i ) ) ) )
by A40;
A42:
(
X c= Y & ( for
i being
Element of
Seg d st (
i in X or not
i in Y ) holds
(
l'' . i = l' . i &
r'' . i = r' . i ) ) )
by A12, A13, A39, A40, A41, Th48;
A43:
(
Y c= Z & ( for
i being
Element of
Seg d st (
i in Y or not
i in Z ) holds
(
l'' . i = l . i &
r'' . i = r . i ) ) )
by A5, A11, A39, A40, A41, Th48;
card (Y \ X) =
(k + 1) - k
by A13, A41, A42, CARD_2:63
.=
1
;
then consider i' being
set such that A44:
Y \ X = {i'}
by CARD_2:60;
A45:
i' in Y \ X
by A44, TARSKI:def 1;
then reconsider i' =
i' as
Element of
Seg d ;
(
i' in Y & not
i' in X )
by A45, XBOOLE_0:def 5;
then A46:
i' in Z \ X
by A43, XBOOLE_0:def 5;
A47:
Y =
X \/ Y
by A42, XBOOLE_1:12
.=
X \/ {i'}
by A44, XBOOLE_1:39
;
per cases
( Y = X \/ {i1} or Y = X \/ {i2} )
by A15, A46, A47;
suppose A48:
Y = X \/ {i1}
;
:: thesis: ( B = B1 or B = B2 )reconsider l'' =
l'',
r'' =
r'',
l1 =
l1,
r1 =
r1 as
Function of
(Seg d),
REAL by Def4;
now let i be
Element of
Seg d;
:: thesis: ( l'' . i = l1 . i & r'' . i = r1 . i )
(
i in Y or not
i in Y )
;
then
( (
l'' . i = l . i &
l1 . i = l . i &
r'' . i = r . i &
r1 . i = r . i ) or (
l'' . i = l' . i &
l1 . i = l' . i &
r'' . i = r' . i &
r1 . i = r' . i ) )
by A5, A11, A12, A13, A20, A22, A39, A40, A41, A48, Th48;
hence
(
l'' . i = l1 . i &
r'' . i = r1 . i )
;
:: thesis: verum end; then
(
l'' = l1 &
r'' = r1 )
by FUNCT_2:113;
hence
(
B = B1 or
B = B2 )
by A40;
:: thesis: verum end; suppose A49:
Y = X \/ {i2}
;
:: thesis: ( B = B1 or B = B2 )reconsider l'' =
l'',
r'' =
r'',
l2 =
l2,
r2 =
r2 as
Function of
(Seg d),
REAL by Def4;
now let i be
Element of
Seg d;
:: thesis: ( l'' . i = l2 . i & r'' . i = r2 . i )
(
i in Y or not
i in Y )
;
then
( (
l'' . i = l . i &
l2 . i = l . i &
r'' . i = r . i &
r2 . i = r . i ) or (
l'' . i = l' . i &
l2 . i = l' . i &
r'' . i = r' . i &
r2 . i = r' . i ) )
by A5, A11, A12, A13, A31, A33, A39, A40, A41, A49, Th48;
hence
(
l'' . i = l2 . i &
r'' . i = r2 . i )
;
:: thesis: verum end; then
(
l'' = l2 &
r'' = r2 )
by FUNCT_2:113;
hence
(
B = B1 or
B = B2 )
by A40;
:: thesis: verum end;
end; then
card ((star A) /\ (del {C})) = 2
* 1
by Th6;
hence
contradiction
by A6, Th52;
:: thesis: verum end;
hence
del (del {C}) = 0_ k,
G
by XBOOLE_0:def 1;
:: thesis: verum
end; A50:
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;
:: thesis: ( del (del C1) = 0_ k,G & del (del C2) = 0_ k,G implies del (del (C1 + C2)) = 0_ k,G )
assume A51:
(
del (del C1) = 0_ k,
G &
del (del C2) = 0_ k,
G )
;
:: thesis: del (del (C1 + C2)) = 0_ k,G
thus del (del (C1 + C2)) =
del ((del C1) + (del C2))
by Th63
.=
(0_ k,G) + (0_ k,G)
by A51, Th63
.=
0_ k,
G
;
:: thesis: verum
end; defpred S1[
Chain of
((k + 1) + 1),
G]
means del (del $1) = 0_ k,
G;
A52:
S1[
0_ ((k + 1) + 1),
G]
for
A being
Cell of
((k + 1) + 1),
G holds
del (del {A}) = 0_ k,
G
then A60:
for
A being
Cell of
((k + 1) + 1),
G st
A in C holds
S1[
{A}]
;
A61:
for
C1,
C2 being
Chain of
((k + 1) + 1),
G st
C1 c= C &
C2 c= C &
S1[
C1] &
S1[
C2] holds
S1[
C1 + C2]
by A50;
thus
S1[
C]
from CHAIN_1:sch 4(A52, A60, A61); :: thesis: verum end;