let n be Nat; :: thesis: ( 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 ; :: thesis: 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)); :: thesis: ( 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) ; :: thesis: 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]
proof
let i be Element of (TopSpaceMetr (Euclid n)); :: thesis: ex j being object st S1[i,j]
reconsider j = i as Point of (Euclid n) ;
take OpenHypercubes j ; :: thesis: S1[i, OpenHypercubes j]
take j ; :: thesis: ( j = i & OpenHypercubes j = OpenHypercubes j )
thus ( j = i & OpenHypercubes j = OpenHypercubes j ) ; :: thesis: verum
end;
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);
now :: thesis: for x being Point of (TopSpaceMetr (Euclid n)) holds NS . x is Basis of x
let x be Point of (TopSpaceMetr (Euclid n)); :: thesis: NS . x is Basis of x
reconsider y = x as Point of (Euclid n) ;
S1[y,NS . y] by A7;
hence NS . x is Basis of x ; :: thesis: verum
end;
then reconsider NS = NS as Neighborhood_System of TopSpaceMetr (Euclid n) by TOPGEN_2:def 3;
take B = Union NS; :: according to CANTOR_1:def 4 :: thesis: B c= FinMeetCl PP
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in B or b in FinMeetCl PP )
reconsider bb = b as set by TARSKI:1;
assume b in B ; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( 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] } ; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( 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) ; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( not b in rng g or b in REAL )
assume b in rng g ; :: thesis: 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 ; :: thesis: b in REAL
then ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) . a = R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[ by A17, A19, A20, FUNCT_7:31;
hence b in REAL by A21, A22; :: thesis: verum
end;
suppose a <> q ; :: thesis: 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; :: thesis: 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; :: thesis: verum
end;
hence s in bool the carrier of (TopSpaceMetr (Euclid n)) by A15, ZFMISC_1:def 1; :: thesis: 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
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Y or z in PP )
assume A26: z in Y ; :: thesis: z in PP
then consider i being Element of S such that
A27: z = H2(i) ;
((Seg n) --> R^1) . i = R^1 ;
hence z in PP by A2, A5, A26, A3, A27, WAYBEL18:def 2; :: thesis: verum
end;
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 :: thesis: 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; :: thesis: 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)).[))) :: thesis: verum
proof
let d be object ; :: according to TARSKI:def 3 :: thesis: ( 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))) ; :: thesis: 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 :: thesis: 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)).[))) . k
let k be object ; :: thesis: ( 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)).[))) ; :: thesis: d1 . b1 in ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . b1
then 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 ; :: thesis: d1 . b1 in ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . b1
hence d1 . k in ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . k by A38, A39, A37, A36, FUNCT_7:31; :: thesis: verum
end;
suppose k <> i ; :: thesis: d1 . b1 in ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . b1
then 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; :: thesis: 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; :: thesis: verum
end;
end;
bb = Intersect Y
proof
now :: thesis: for M being set st M in Y holds
bb c= M
let M be set ; :: thesis: ( M in Y implies bb c= M )
assume M in Y ; :: thesis: bb c= M
then ex i being Element of S st M = H2(i) ;
hence bb c= M by A13, A32; :: thesis: verum
end;
hence bb c= Intersect Y by A30, A29, SETFAM_1:5; :: according to XBOOLE_0:def 10 :: thesis: Intersect Y c= bb
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in Intersect Y or q in bb )
assume A42: q in Intersect Y ; :: thesis: q in bb
then reconsider q = q as Function ;
A43: dom q = Seg n by A42, FINSEQ_1:89;
now :: thesis: for a being object st a in dom (Intervals (x,(1 / m))) holds
q . a in (Intervals (x,(1 / m))) . a
let a be object ; :: thesis: ( 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))) ; :: thesis: q . a in (Intervals (x,(1 / m))) . a
A45: (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; :: thesis: verum
end;
hence q in bb by A13, A43, A31, A12, CARD_3:9; :: thesis: verum
end;
hence b in FinMeetCl PP by A25, A14, CANTOR_1:def 3; :: thesis: verum