let n be Nat; ( n <> 0 implies for PP being Subset-Family of (TopSpaceMetr (Euclid n)) st PP = product_prebasis ((Seg n) --> R^1) holds
PP is quasi_prebasis )
assume A1:
n <> 0
; for PP being Subset-Family of (TopSpaceMetr (Euclid n)) st PP = product_prebasis ((Seg n) --> R^1) holds
PP is quasi_prebasis
set E = Euclid n;
set T = TopSpaceMetr (Euclid n);
let PP be Subset-Family of (TopSpaceMetr (Euclid n)); ( PP = product_prebasis ((Seg n) --> R^1) implies PP is quasi_prebasis )
set J = (Seg n) --> R^1;
set C = Carrier ((Seg n) --> R^1);
set S = Seg n;
reconsider S = Seg n as non empty finite set by A1;
assume A2:
PP = product_prebasis ((Seg n) --> R^1)
; PP is quasi_prebasis
A3:
REAL n = Funcs ((Seg n),REAL)
by FINSEQ_2:93;
A4:
dom (Carrier ((Seg n) --> R^1)) = Seg n
by PARTFUN1:def 2;
A5:
Funcs ((Seg n),REAL) = product (Carrier ((Seg n) --> R^1))
by Th25;
defpred S1[ set , object ] means ex e being Point of (Euclid n) st
( e = $1 & $2 = OpenHypercubes e );
A6:
for i being Element of (TopSpaceMetr (Euclid n)) ex j being object st S1[i,j]
consider NS being ManySortedSet of (TopSpaceMetr (Euclid n)) such that
A7:
for x being Point of (TopSpaceMetr (Euclid n)) holds S1[x,NS . x]
from PBOOLE:sch 6(A6);
then reconsider NS = NS as Neighborhood_System of TopSpaceMetr (Euclid n) by TOPGEN_2:def 3;
take B = Union NS; CANTOR_1:def 4 B c= FinMeetCl PP
let b be object ; TARSKI:def 3 ( not b in B or b in FinMeetCl PP )
reconsider bb = b as set by TARSKI:1;
assume
b in B
; b in FinMeetCl PP
then consider Z being set such that
A8:
b in Z
and
A9:
Z in rng NS
by TARSKI:def 4;
consider x being object such that
A10:
x in dom NS
and
A11:
NS . x = Z
by A9, FUNCT_1:def 3;
reconsider x = x as Point of (Euclid n) by A10;
A12:
dom x = Seg n
by FINSEQ_1:89;
S1[x,NS . x]
by A7;
then consider m being non zero Element of NAT such that
A13:
b = OpenHypercube (x,(1 / m))
by A8, A11;
deffunc H2( object ) -> set = product ((Carrier ((Seg n) --> R^1)) +* ($1,(R^1 ].((x . $1) - (1 / m)),((x . $1) + (1 / m)).[)));
defpred S2[ set ] means verum;
set Y = { H2(q) where q is Element of S : S2[q] } ;
A14:
{ H2(q) where q is Element of S : S2[q] } is finite
from PRE_CIRC:sch 1();
{ H2(q) where q is Element of S : S2[q] } c= bool the carrier of (TopSpaceMetr (Euclid n))
proof
let s be
object ;
TARSKI:def 3 ( not s in { H2(q) where q is Element of S : S2[q] } or s in bool the carrier of (TopSpaceMetr (Euclid n)) )
assume
s in { H2(q) where q is Element of S : S2[q] }
;
s in bool the carrier of (TopSpaceMetr (Euclid n))
then consider q being
Element of
S such that A15:
s = H2(
q)
;
H2(
q)
c= the
carrier of
(TopSpaceMetr (Euclid n))
proof
let z be
object ;
TARSKI:def 3 ( not z in H2(q) or z in the carrier of (TopSpaceMetr (Euclid n)) )
set f =
(Carrier ((Seg n) --> R^1)) +* (
q,
(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[));
assume
z in H2(
q)
;
z in the carrier of (TopSpaceMetr (Euclid n))
then consider g being
Function such that A16:
z = g
and A17:
dom g = dom ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[)))
and A18:
for
d being
object st
d in dom ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) holds
g . d in ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) . d
by CARD_3:def 5;
A19:
dom ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) = dom (Carrier ((Seg n) --> R^1))
by FUNCT_7:30;
then reconsider g =
g as
FinSequence by A4, A17, FINSEQ_1:def 2;
rng g c= REAL
proof
let b be
object ;
TARSKI:def 3 ( not b in rng g or b in REAL )
assume
b in rng g
;
b in REAL
then consider a being
object such that A20:
a in dom g
and A21:
g . a = b
by FUNCT_1:def 3;
A22:
g . a in ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) . a
by A17, A18, A20;
per cases
( a = q or a <> q )
;
suppose
a <> q
;
b in REAL then A23:
((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) . a = (Carrier ((Seg n) --> R^1)) . a
by FUNCT_7:32;
ex
R being
1-sorted st
(
R = ((Seg n) --> R^1) . a &
(Carrier ((Seg n) --> R^1)) . a = the
carrier of
R )
by A20, A17, A19, PRALG_1:def 15;
hence
b in REAL
by A21, A22, A23, A20, A17, A19, FUNCOP_1:7;
verum end; end;
end;
then
g is
FinSequence of
REAL
by FINSEQ_1:def 4;
then A24:
g is
Element of
REAL *
by FINSEQ_1:def 11;
n in NAT
by ORDINAL1:def 12;
then
len g = n
by A4, A17, A19, FINSEQ_1:def 3;
hence
z in the
carrier of
(TopSpaceMetr (Euclid n))
by A16, A24;
verum
end;
hence
s in bool the
carrier of
(TopSpaceMetr (Euclid n))
by A15, ZFMISC_1:def 1;
verum
end;
then reconsider Y = { H2(q) where q is Element of S : S2[q] } as Subset-Family of (TopSpaceMetr (Euclid n)) ;
A25:
Y c= PP
consider N being object such that
A28:
N in S
by XBOOLE_0:def 1;
A29:
H2(N) in Y
by A28;
then A30:
Intersect Y = meet Y
by SETFAM_1:def 9;
A31:
dom (Intervals (x,(1 / m))) = dom x
by Def3;
A32:
now for i being Element of S holds product (Intervals (x,(1 / m))) c= product ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[)))let i be
Element of
S;
product (Intervals (x,(1 / m))) c= product ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[)))set f =
(Carrier ((Seg n) --> R^1)) +* (
i,
(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[));
thus
product (Intervals (x,(1 / m))) c= product ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[)))
verumproof
let d be
object ;
TARSKI:def 3 ( not d in product (Intervals (x,(1 / m))) or d in product ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) )
assume
d in product (Intervals (x,(1 / m)))
;
d in product ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[)))
then consider d1 being
Function such that A33:
d = d1
and A34:
dom d1 = dom (Intervals (x,(1 / m)))
and A35:
for
a being
object st
a in dom (Intervals (x,(1 / m))) holds
d1 . a in (Intervals (x,(1 / m))) . a
by CARD_3:def 5;
A36:
dom ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) = dom (Carrier ((Seg n) --> R^1))
by FUNCT_7:30;
now for k being object st k in dom ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) holds
d1 . k in ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . klet k be
object ;
( k in dom ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) implies d1 . b1 in ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . b1 )assume A37:
k in dom ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[)))
;
d1 . b1 in ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . b1then A38:
(Intervals (x,(1 / m))) . k = ].((x . k) - (1 / m)),((x . k) + (1 / m)).[
by A36, A12, Def3;
A39:
d1 . k in (Intervals (x,(1 / m))) . k
by A35, A31, A12, A36, A37;
per cases
( k = i or k <> i )
;
suppose
k <> i
;
d1 . b1 in ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . b1then A40:
((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . k = (Carrier ((Seg n) --> R^1)) . k
by FUNCT_7:32;
A41:
ex
R being
1-sorted st
(
R = ((Seg n) --> R^1) . k &
(Carrier ((Seg n) --> R^1)) . k = the
carrier of
R )
by A37, A36, PRALG_1:def 15;
d1 . k in REAL
by A38, A39;
hence
d1 . k in ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . k
by A40, A41, A37, A36, FUNCOP_1:7;
verum end; end; end;
hence
d in product ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[)))
by A33, A4, A34, A31, A12, A36, CARD_3:9;
verum
end; end;
bb = Intersect Y
proof
now for M being set st M in Y holds
bb c= Mlet M be
set ;
( M in Y implies bb c= M )assume
M in Y
;
bb c= Mthen
ex
i being
Element of
S st
M = H2(
i)
;
hence
bb c= M
by A13, A32;
verum end;
hence
bb c= Intersect Y
by A30, A29, SETFAM_1:5;
XBOOLE_0:def 10 Intersect Y c= bb
let q be
object ;
TARSKI:def 3 ( not q in Intersect Y or q in bb )
assume A42:
q in Intersect Y
;
q in bb
then reconsider q =
q as
Function ;
A43:
dom q = Seg n
by A42, FINSEQ_1:89;
now for a being object st a in dom (Intervals (x,(1 / m))) holds
q . a in (Intervals (x,(1 / m))) . alet a be
object ;
( a in dom (Intervals (x,(1 / m))) implies q . a in (Intervals (x,(1 / m))) . a )assume A44:
a in dom (Intervals (x,(1 / m)))
;
q . a in (Intervals (x,(1 / m))) . aA45:
(Intervals (x,(1 / m))) . a = ].((x . a) - (1 / m)),((x . a) + (1 / m)).[
by A44, A31, Def3;
set f =
(Carrier ((Seg n) --> R^1)) +* (
a,
(R^1 ].((x . a) - (1 / m)),((x . a) + (1 / m)).[));
H2(
a)
in Y
by A44, A31, A12;
then A46:
q in H2(
a)
by A42, SETFAM_1:43;
then A47:
dom q = dom ((Carrier ((Seg n) --> R^1)) +* (a,(R^1 ].((x . a) - (1 / m)),((x . a) + (1 / m)).[)))
by CARD_3:9;
then A48:
q . a in ((Carrier ((Seg n) --> R^1)) +* (a,(R^1 ].((x . a) - (1 / m)),((x . a) + (1 / m)).[))) . a
by A43, A44, A31, A12, A46, CARD_3:9;
dom ((Carrier ((Seg n) --> R^1)) +* (a,(R^1 ].((x . a) - (1 / m)),((x . a) + (1 / m)).[))) = dom (Carrier ((Seg n) --> R^1))
by FUNCT_7:30;
hence
q . a in (Intervals (x,(1 / m))) . a
by A45, A48, A43, A44, A31, A12, A47, FUNCT_7:31;
verum end;
hence
q in bb
by A13, A43, A31, A12, CARD_3:9;
verum
end;
hence
b in FinMeetCl PP
by A25, A14, CANTOR_1:def 3; verum