let MS be PseudoMetricSpace; :: thesis: Family_open_set (FMT_induced_by (uniformity_induced_by MS)) = Family_open_set MS
set X = Family_open_set (FMT_induced_by (uniformity_induced_by MS));
set Y = Family_open_set MS;
thus Family_open_set (FMT_induced_by (uniformity_induced_by MS)) c= Family_open_set MS :: according to XBOOLE_0:def 10 :: thesis: Family_open_set MS c= Family_open_set (FMT_induced_by (uniformity_induced_by MS))
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in Family_open_set (FMT_induced_by (uniformity_induced_by MS)) or t in Family_open_set MS )
assume A2: t in Family_open_set (FMT_induced_by (uniformity_induced_by MS)) ; :: thesis: t in Family_open_set MS
then reconsider t1 = t as Subset of (FMT_induced_by (uniformity_induced_by MS)) ;
for x being Point of MS st x in t1 holds
ex r being Real st
( r > 0 & Ball (x,r) c= t1 )
proof
let x be Point of MS; :: thesis: ( x in t1 implies ex r being Real st
( r > 0 & Ball (x,r) c= t1 ) )
assume A3: x in t1 ; :: thesis: ex r being Real st
( r > 0 & Ball (x,r) c= t1 )
reconsider x1 = x as Element of (uniformity_induced_by MS) ;
t1 in Neighborhood x1 by A3, A2, Th8, Th9;
then consider V0 being Element of the entourages of (uniformity_induced_by MS) such that
A4: t1 = Neighborhood (V0,x1) ;
consider b being Element of fundamental_system_of_entourages MS such that
A5: b c= V0 by CARDFIL2:def 8;
b in { (fundamental_element_of_entourages (MS,r)) where r is positive Real : verum } ;
then consider r0 being positive Real such that
A6: b = fundamental_element_of_entourages (MS,r0) ;
now :: thesis: ex r0 being positive Real st
( r0 > 0 & Ball (x,r0) c= t1 )
take r0 = r0; :: thesis: ( r0 > 0 & Ball (x,r0) c= t1 )
thus r0 > 0 ; :: thesis: Ball (x,r0) c= t1
thus Ball (x,r0) c= t1 :: thesis: verum
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in Ball (x,r0) or u in t1 )
assume A7: u in Ball (x,r0) ; :: thesis: u in t1
then reconsider u1 = u as Element of MS ;
dist (x,u1) < r0 by A7, METRIC_1:11;
then [x,u1] in b by A6;
hence u in t1 by A4, A5; :: thesis: verum
end;
end;
hence ex r being Real st
( r > 0 & Ball (x,r) c= t1 ) ; :: thesis: verum
end;
hence t in Family_open_set MS by PCOMPS_1:def 4; :: thesis: verum
end;
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in Family_open_set MS or t in Family_open_set (FMT_induced_by (uniformity_induced_by MS)) )
assume A8: t in Family_open_set MS ; :: thesis: t in Family_open_set (FMT_induced_by (uniformity_induced_by MS))
then reconsider t1 = t as Subset of MS ;
for x being Element of (uniformity_induced_by MS) st x in t1 holds
t1 in Neighborhood x
proof
let x be Element of (uniformity_induced_by MS); :: thesis: ( x in t1 implies t1 in Neighborhood x )
assume A9: x in t1 ; :: thesis: t1 in Neighborhood x
reconsider x1 = x as Element of MS ;
consider r0 being Real such that
A10: r0 > 0 and
A11: Ball (x1,r0) c= t1 by A8, PCOMPS_1:def 4, A9;
reconsider r1 = r0 / 2 as positive Real by A10;
set V0 = fundamental_element_of_entourages (MS,r1);
fundamental_element_of_entourages (MS,r1) in fundamental_system_of_entourages MS ;
then reconsider V0 = fundamental_element_of_entourages (MS,r1) as Element of fundamental_system_of_entourages MS ;
reconsider V1 = V0 \/ [:t1,t1:] as Subset of [: the carrier of MS, the carrier of MS:] ;
V0 c= V1 by XBOOLE_1:7;
then reconsider V1 = V1 as Element of the entourages of (uniformity_induced_by MS) by CARDFIL2:def 8;
set Z = { y where y is Element of (uniformity_induced_by MS) : [x,y] in V1 } ;
{ y where y is Element of (uniformity_induced_by MS) : [x,y] in V1 } = t1
proof
thus { y where y is Element of (uniformity_induced_by MS) : [x,y] in V1 } c= t1 :: according to XBOOLE_0:def 10 :: thesis: t1 c= { y where y is Element of (uniformity_induced_by MS) : [x,y] in V1 }
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { y where y is Element of (uniformity_induced_by MS) : [x,y] in V1 } or u in t1 )
assume u in { y where y is Element of (uniformity_induced_by MS) : [x,y] in V1 } ; :: thesis: u in t1
then consider y0 being Element of (uniformity_induced_by MS) such that
A13: u = y0 and
A14: [x,y0] in V1 ;
per cases ( [x,y0] in V0 or [x,y0] in [:t1,t1:] ) by A14, XBOOLE_0:def 3;
suppose [x,y0] in V0 ; :: thesis: u in t1
then consider x2, y2 being Element of MS such that
A15: [x,y0] = [x2,y2] and
A16: dist (x2,y2) <= r1 ;
r0 / 2 < r0 / 1 by A10, XREAL_1:76;
then A17: dist (x2,y2) < r0 by A16, XXREAL_0:2;
Ball (x2,r0) = Ball (x1,r0) by A15, XTUPLE_0:1;
then y2 in t1 by A17, METRIC_1:11, A11;
hence u in t1 by A13, A15, XTUPLE_0:1; :: thesis: verum
end;
suppose [x,y0] in [:t1,t1:] ; :: thesis: u in t1
then ex a, b being object st
( a in t1 & b in t1 & [x,y0] = [a,b] ) by ZFMISC_1:def 2;
hence u in t1 by A13, XTUPLE_0:1; :: thesis: verum
end;
end;
end;
let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in t1 or v in { y where y is Element of (uniformity_induced_by MS) : [x,y] in V1 } )
assume A18: v in t1 ; :: thesis: v in { y where y is Element of (uniformity_induced_by MS) : [x,y] in V1 }
then reconsider v1 = v as Element of (uniformity_induced_by MS) ;
[x,v1] in [:t1,t1:] by A18, A9, ZFMISC_1:def 2;
then [x,v1] in V1 by XBOOLE_0:def 3;
hence v in { y where y is Element of (uniformity_induced_by MS) : [x,y] in V1 } ; :: thesis: verum
end;
then t1 = Neighborhood (V1,x) ;
hence t1 in Neighborhood x ; :: thesis: verum
end;
hence t in Family_open_set (FMT_induced_by (uniformity_induced_by MS)) by Th8, Th9; :: thesis: verum