let d be non zero Nat; :: thesis: for G being Grating of d
for A being Subset of (REAL d) holds
( A in cells (1,G) iff ex l, r being Element of REAL d ex i0 being Element of Seg d 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 being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i ) ) ) )
let G be Grating of d; :: thesis: for A being Subset of (REAL d) holds
( A in cells (1,G) iff ex l, r being Element of REAL d ex i0 being Element of Seg d 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 being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i ) ) ) )
A1: d >= 1 by Def2;
let A be Subset of (REAL d); :: thesis: ( A in cells (1,G) iff ex l, r being Element of REAL d ex i0 being Element of Seg d 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 being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i ) ) ) )
hereby :: thesis: ( ex l, r being Element of REAL d ex i0 being Element of Seg d 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 being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i ) ) ) implies A in cells (1,G) )
assume A in cells (1,G) ; :: thesis: ex l, r being Element of REAL d ex i0 being Element of Seg d 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 being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i ) ) )
then consider l, r being Element of REAL d such that
A2: A = cell (l,r) and
A3: ( ex X being Subset of (Seg d) st
( card X = 1 & ( 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 ( 1 = d & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) by A1, Th29;
take l = l; :: thesis: ex r being Element of REAL d ex i0 being Element of Seg d 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 being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i ) ) )
take r = r; :: thesis: ex i0 being Element of Seg d 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 being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i ) ) )
thus ex i0 being Element of Seg d 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 being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i ) ) ) :: thesis: verum
proof
per cases ( ex X being Subset of (Seg d) st
( card X = 1 & ( 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 ( d = 1 & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) by A3;
suppose ex X being Subset of (Seg d) st
( card X = 1 & ( 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 ) ) ) ) ; :: thesis: ex i0 being Element of Seg d 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 being Element of Seg d st i <> i0 holds
( 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 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 ) ) ;
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 = i0 as Element of Seg d ;
take i0 ; :: thesis: ( 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 being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i ) ) )
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; :: thesis: for i being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i )
let i be Element of Seg d; :: thesis: ( i <> i0 implies ( l . i = r . i & l . i in G . i ) )
( not i in X iff i <> i0 ) by A6, TARSKI:def 1;
hence ( i <> i0 implies ( l . i = r . i & l . i in G . i ) ) by A5; :: thesis: verum
end;
suppose A8: ( d = 1 & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ; :: thesis: ex i0 being Element of Seg d 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 being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i ) ) )
reconsider i0 = 1 as Element of Seg d by A1, FINSEQ_1:1;
take i0 ; :: thesis: ( 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 being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i ) ) )
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; :: thesis: for i being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i )
let i be Element of Seg d; :: thesis: ( i <> i0 implies ( l . i = r . i & l . i in G . i ) )
A9: 1 <= i by FINSEQ_1:1;
i <= d by FINSEQ_1:1;
hence ( i <> i0 implies ( l . i = r . i & l . i in G . i ) ) by A8, A9, XXREAL_0:1; :: thesis: verum
end;
end;
end;
end;
given l, r being Element of REAL d, i0 being Element of Seg d 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 being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i ) ; :: thesis: A in cells (1,G)
set X = {i0};
per cases ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) by A11;
suppose A14: l . i0 < r . i0 ; :: thesis: A in cells (1,G)
A15: card {i0} = 1 by CARD_1:30;
now :: thesis: for i being Element of Seg d holds
( ( i in {i0} & l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( not i in {i0} & l . i = r . i & l . i in G . i ) )
let i be Element of Seg d; :: thesis: ( ( i in {i0} & l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( not i in {i0} & l . i = r . i & l . i in G . i ) )
( i in {i0} iff i = i0 ) by TARSKI:def 1;
hence ( ( i in {i0} & l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( not i in {i0} & l . i = r . i & l . i in G . i ) ) by A12, A13, A14; :: thesis: verum
end;
hence A in cells (1,G) by A1, A10, A15, Th29; :: thesis: verum
end;
suppose A16: ( d = 1 & r . i0 < l . i0 ) ; :: thesis: A in cells (1,G)
now :: thesis: for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i )
let i be Element of Seg d; :: thesis: ( r . i < l . i & [(l . i),(r . i)] is Gap of G . 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; :: thesis: verum
end;
hence A in cells (1,G) by A10, A11, Th29; :: thesis: verum
end;
end;