let d be non zero Element of NAT ; :: thesis: for G being Grating of d
for A being Subset of (REAL d) holds
( A in cells 0 ,G iff ex x being Element of REAL d st
( A = cell x,x & ( for i being Element of Seg d holds x . i in G . i ) ) )
let G be Grating of d; :: thesis: for A being Subset of (REAL d) holds
( A in cells 0 ,G iff ex x being Element of REAL d st
( A = cell x,x & ( for i being Element of Seg d holds x . i in G . i ) ) )
let A be Subset of (REAL d); :: thesis: ( A in cells 0 ,G iff ex x being Element of REAL d st
( A = cell x,x & ( for i being Element of Seg d holds x . i in G . i ) ) )
hereby :: thesis: ( ex x being Element of REAL d st
( A = cell x,x & ( for i being Element of Seg d holds x . i in G . i ) ) implies A in cells 0 ,G )
assume
A in cells 0 ,
G
;
:: thesis: ex x being Element of REAL d st
( A = cell x,x & ( for i being Element of Seg d holds x . i in G . i ) )then consider l,
r being
Element of
REAL d such that A1:
(
A = cell l,
r & ( ex
X being
Subset of
(Seg d) st
(
card X = 0 & ( 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 (
0 = d & ( for
i being
Element of
Seg d holds
(
r . i < l . i &
[(l . i),(r . i)] is
Gap of
G . i ) ) ) ) )
by Th33;
consider X being
Subset of
(Seg d) such that A2:
(
card X = 0 & ( 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 A1;
reconsider l' =
l,
r' =
r as
Function of
(Seg d),
REAL by Def4;
X = {}
by A2;
then A3:
for
i being
Element of
Seg d holds
(
l' . i = r' . i &
l . i in G . i )
by A2;
then
l' = r'
by FUNCT_2:113;
hence
ex
x being
Element of
REAL d st
(
A = cell x,
x & ( for
i being
Element of
Seg d holds
x . i in G . i ) )
by A1, A3;
:: thesis: verum
end;
given x being Element of REAL d such that A4:
( A = cell x,x & ( for i being Element of Seg d holds x . i in G . i ) )
; :: thesis: A in cells 0 ,G
ex X being Subset of (Seg d) st
( card X = 0 & ( for i being Element of Seg d 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 ) ) ) )
hence
A in cells 0 ,G
by A4, Th33; :: thesis: verum