:: PCOMPS_1 semantic presentation
begin
theorem Th1: :: PCOMPS_1:1
for PM being MetrStruct
for x being Element of PM
for r, p being real number st r <= p holds
Ball (x,r) c= Ball (x,p)
proof
let PM be MetrStruct ; ::_thesis: for x being Element of PM
for r, p being real number st r <= p holds
Ball (x,r) c= Ball (x,p)
let x be Element of PM; ::_thesis: for r, p being real number st r <= p holds
Ball (x,r) c= Ball (x,p)
let r, p be real number ; ::_thesis: ( r <= p implies Ball (x,r) c= Ball (x,p) )
assume A1: r <= p ; ::_thesis: Ball (x,r) c= Ball (x,p)
for y being Element of PM st y in Ball (x,r) holds
y in Ball (x,p)
proof
let y be Element of PM; ::_thesis: ( y in Ball (x,r) implies y in Ball (x,p) )
assume A2: y in Ball (x,r) ; ::_thesis: y in Ball (x,p)
then dist (x,y) < r by METRIC_1:11;
then A3: dist (x,y) < p by A1, XXREAL_0:2;
not PM is empty by A2;
hence y in Ball (x,p) by A3, METRIC_1:11; ::_thesis: verum
end;
hence Ball (x,r) c= Ball (x,p) by SUBSET_1:2; ::_thesis: verum
end;
theorem Th2: :: PCOMPS_1:2
for T being TopSpace
for A being Subset of T holds
( Cl A <> {} iff A <> {} )
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds
( Cl A <> {} iff A <> {} )
let A be Subset of T; ::_thesis: ( Cl A <> {} iff A <> {} )
( A <> {} implies Cl A <> {} )
proof
set x = the Element of A;
A1: A c= Cl A by PRE_TOPC:18;
assume A2: A <> {} ; ::_thesis: Cl A <> {}
ex x being set st x in Cl A
proof
take the Element of A ; ::_thesis: the Element of A in Cl A
thus the Element of A in Cl A by A2, A1, TARSKI:def_3; ::_thesis: verum
end;
hence Cl A <> {} ; ::_thesis: verum
end;
hence ( Cl A <> {} iff A <> {} ) by PRE_TOPC:22; ::_thesis: verum
end;
theorem Th3: :: PCOMPS_1:3
for T being non empty TopSpace
for FX being Subset-Family of T st FX is Cover of T holds
for x being Point of T ex W being Subset of T st
( x in W & W in FX )
proof
let T be non empty TopSpace; ::_thesis: for FX being Subset-Family of T st FX is Cover of T holds
for x being Point of T ex W being Subset of T st
( x in W & W in FX )
let FX be Subset-Family of T; ::_thesis: ( FX is Cover of T implies for x being Point of T ex W being Subset of T st
( x in W & W in FX ) )
assume FX is Cover of T ; ::_thesis: for x being Point of T ex W being Subset of T st
( x in W & W in FX )
then A1: union FX = [#] T by SETFAM_1:45;
thus for x being Point of T ex W being Subset of T st
( x in W & W in FX ) ::_thesis: verum
proof
let x be Point of T; ::_thesis: ex W being Subset of T st
( x in W & W in FX )
thus ex W being Subset of T st
( x in W & W in FX ) ::_thesis: verum
proof
consider W being set such that
A2: x in W and
A3: W in FX by A1, TARSKI:def_4;
reconsider W = W as Subset of T by A3;
take W ; ::_thesis: ( x in W & W in FX )
thus ( x in W & W in FX ) by A2, A3; ::_thesis: verum
end;
end;
end;
theorem :: PCOMPS_1:4
for a being set holds the topology of (1TopSp a) = bool a ;
theorem :: PCOMPS_1:5
for a being set holds the carrier of (1TopSp a) = a ;
theorem :: PCOMPS_1:6
for a being set holds 1TopSp {a} is compact ;
theorem :: PCOMPS_1:7
for T being non empty TopSpace
for x being Point of T st T is T_2 holds
{x} is closed ;
definition
let T be TopStruct ;
let IT be Subset-Family of T;
attrIT is locally_finite means :Def1: :: PCOMPS_1:def 1
for x being Point of T ex W being Subset of T st
( x in W & W is open & { V where V is Subset of T : ( V in IT & V meets W ) } is finite );
end;
:: deftheorem Def1 defines locally_finite PCOMPS_1:def_1_:_
for T being TopStruct
for IT being Subset-Family of T holds
( IT is locally_finite iff for x being Point of T ex W being Subset of T st
( x in W & W is open & { V where V is Subset of T : ( V in IT & V meets W ) } is finite ) );
theorem Th8: :: PCOMPS_1:8
for T being non empty TopSpace
for FX being Subset-Family of T
for W being Subset of T holds { V where V is Subset of T : ( V in FX & V meets W ) } c= FX
proof
let T be non empty TopSpace; ::_thesis: for FX being Subset-Family of T
for W being Subset of T holds { V where V is Subset of T : ( V in FX & V meets W ) } c= FX
let FX be Subset-Family of T; ::_thesis: for W being Subset of T holds { V where V is Subset of T : ( V in FX & V meets W ) } c= FX
let W be Subset of T; ::_thesis: { V where V is Subset of T : ( V in FX & V meets W ) } c= FX
now__::_thesis:_for_Y_being_set_st_Y_in__{__V_where_V_is_Subset_of_T_:_(_V_in_FX_&_V_meets_W_)__}__holds_
Y_in_FX
let Y be set ; ::_thesis: ( Y in { V where V is Subset of T : ( V in FX & V meets W ) } implies Y in FX )
assume Y in { V where V is Subset of T : ( V in FX & V meets W ) } ; ::_thesis: Y in FX
then ex V being Subset of T st
( Y = V & V in FX & V meets W ) ;
hence Y in FX ; ::_thesis: verum
end;
hence { V where V is Subset of T : ( V in FX & V meets W ) } c= FX by TARSKI:def_3; ::_thesis: verum
end;
theorem Th9: :: PCOMPS_1:9
for T being non empty TopSpace
for FX, GX being Subset-Family of T st FX c= GX & GX is locally_finite holds
FX is locally_finite
proof
let T be non empty TopSpace; ::_thesis: for FX, GX being Subset-Family of T st FX c= GX & GX is locally_finite holds
FX is locally_finite
let FX, GX be Subset-Family of T; ::_thesis: ( FX c= GX & GX is locally_finite implies FX is locally_finite )
assume that
A1: FX c= GX and
A2: GX is locally_finite ; ::_thesis: FX is locally_finite
now__::_thesis:_for_x_being_Point_of_T_ex_W_being_Subset_of_T_st_
(_x_in_W_&_W_is_open_&__{__V_where_V_is_Subset_of_T_:_(_V_in_FX_&_V_meets_W_)__}__is_finite_)
let x be Point of T; ::_thesis: ex W being Subset of T st
( x in W & W is open & { V where V is Subset of T : ( V in FX & V meets W ) } is finite )
thus ex W being Subset of T st
( x in W & W is open & { V where V is Subset of T : ( V in FX & V meets W ) } is finite ) ::_thesis: verum
proof
consider Y being Subset of T such that
A3: x in Y and
A4: Y is open and
A5: { X where X is Subset of T : ( X in GX & X meets Y ) } is finite by A2, Def1;
take W = Y; ::_thesis: ( x in W & W is open & { V where V is Subset of T : ( V in FX & V meets W ) } is finite )
thus x in W by A3; ::_thesis: ( W is open & { V where V is Subset of T : ( V in FX & V meets W ) } is finite )
thus W is open by A4; ::_thesis: { V where V is Subset of T : ( V in FX & V meets W ) } is finite
{ V where V is Subset of T : ( V in FX & V meets W ) } c= { X where X is Subset of T : ( X in GX & X meets Y ) }
proof
now__::_thesis:_for_Z_being_set_st_Z_in__{__V_where_V_is_Subset_of_T_:_(_V_in_FX_&_V_meets_W_)__}__holds_
Z_in__{__X_where_X_is_Subset_of_T_:_(_X_in_GX_&_X_meets_Y_)__}_
let Z be set ; ::_thesis: ( Z in { V where V is Subset of T : ( V in FX & V meets W ) } implies Z in { X where X is Subset of T : ( X in GX & X meets Y ) } )
assume A6: Z in { V where V is Subset of T : ( V in FX & V meets W ) } ; ::_thesis: Z in { X where X is Subset of T : ( X in GX & X meets Y ) }
ex X being Subset of T st
( Z = X & X in GX & X meets Y )
proof
consider V being Subset of T such that
A7: Z = V and
A8: V in FX and
A9: V meets W by A6;
take X = V; ::_thesis: ( Z = X & X in GX & X meets Y )
thus Z = X by A7; ::_thesis: ( X in GX & X meets Y )
thus X in GX by A1, A8; ::_thesis: X meets Y
thus X meets Y by A9; ::_thesis: verum
end;
hence Z in { X where X is Subset of T : ( X in GX & X meets Y ) } ; ::_thesis: verum
end;
hence { V where V is Subset of T : ( V in FX & V meets W ) } c= { X where X is Subset of T : ( X in GX & X meets Y ) } by TARSKI:def_3; ::_thesis: verum
end;
hence { V where V is Subset of T : ( V in FX & V meets W ) } is finite by A5; ::_thesis: verum
end;
end;
hence FX is locally_finite by Def1; ::_thesis: verum
end;
theorem Th10: :: PCOMPS_1:10
for T being non empty TopSpace
for FX being Subset-Family of T st FX is finite holds
FX is locally_finite
proof
let T be non empty TopSpace; ::_thesis: for FX being Subset-Family of T st FX is finite holds
FX is locally_finite
let FX be Subset-Family of T; ::_thesis: ( FX is finite implies FX is locally_finite )
assume A1: FX is finite ; ::_thesis: FX is locally_finite
for x being Point of T ex W being Subset of T st
( x in W & W is open & { V where V is Subset of T : ( V in FX & V meets W ) } is finite )
proof
let x be Point of T; ::_thesis: ex W being Subset of T st
( x in W & W is open & { V where V is Subset of T : ( V in FX & V meets W ) } is finite )
take [#] T ; ::_thesis: ( x in [#] T & [#] T is open & { V where V is Subset of T : ( V in FX & V meets [#] T ) } is finite )
thus x in [#] T ; ::_thesis: ( [#] T is open & { V where V is Subset of T : ( V in FX & V meets [#] T ) } is finite )
thus [#] T is open ; ::_thesis: { V where V is Subset of T : ( V in FX & V meets [#] T ) } is finite
thus { V where V is Subset of T : ( V in FX & V meets [#] T ) } is finite by A1, Th8, FINSET_1:1; ::_thesis: verum
end;
hence FX is locally_finite by Def1; ::_thesis: verum
end;
definition
let T be TopStruct ;
let FX be Subset-Family of T;
func clf FX -> Subset-Family of T means :Def2: :: PCOMPS_1:def 2
for Z being Subset of T holds
( Z in it iff ex W being Subset of T st
( Z = Cl W & W in FX ) );
existence
ex b1 being Subset-Family of T st
for Z being Subset of T holds
( Z in b1 iff ex W being Subset of T st
( Z = Cl W & W in FX ) )
proof
defpred S1[ set ] means ex W being Subset of T st
( $1 = Cl W & W in FX );
thus ex S being Subset-Family of T st
for Z being Subset of T holds
( Z in S iff S1[Z] ) from SUBSET_1:sch_3(); ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset-Family of T st ( for Z being Subset of T holds
( Z in b1 iff ex W being Subset of T st
( Z = Cl W & W in FX ) ) ) & ( for Z being Subset of T holds
( Z in b2 iff ex W being Subset of T st
( Z = Cl W & W in FX ) ) ) holds
b1 = b2
proof
let HX, GX be Subset-Family of T; ::_thesis: ( ( for Z being Subset of T holds
( Z in HX iff ex W being Subset of T st
( Z = Cl W & W in FX ) ) ) & ( for Z being Subset of T holds
( Z in GX iff ex W being Subset of T st
( Z = Cl W & W in FX ) ) ) implies HX = GX )
assume that
A1: for Z being Subset of T holds
( Z in HX iff ex W being Subset of T st
( Z = Cl W & W in FX ) ) and
A2: for X being Subset of T holds
( X in GX iff ex V being Subset of T st
( X = Cl V & V in FX ) ) ; ::_thesis: HX = GX
now__::_thesis:_for_X_being_set_st_X_in_GX_holds_
X_in_HX
let X be set ; ::_thesis: ( X in GX implies X in HX )
assume A3: X in GX ; ::_thesis: X in HX
then reconsider X9 = X as Subset of T ;
ex V being Subset of T st
( X9 = Cl V & V in FX ) by A2, A3;
hence X in HX by A1; ::_thesis: verum
end;
then A4: GX c= HX by TARSKI:def_3;
now__::_thesis:_for_Z_being_set_st_Z_in_HX_holds_
Z_in_GX
let Z be set ; ::_thesis: ( Z in HX implies Z in GX )
assume A5: Z in HX ; ::_thesis: Z in GX
then reconsider Z9 = Z as Subset of T ;
ex W being Subset of T st
( Z9 = Cl W & W in FX ) by A1, A5;
hence Z in GX by A2; ::_thesis: verum
end;
then HX c= GX by TARSKI:def_3;
hence HX = GX by A4, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines clf PCOMPS_1:def_2_:_
for T being TopStruct
for FX, b3 being Subset-Family of T holds
( b3 = clf FX iff for Z being Subset of T holds
( Z in b3 iff ex W being Subset of T st
( Z = Cl W & W in FX ) ) );
theorem :: PCOMPS_1:11
for T being TopSpace
for FX being Subset-Family of T holds clf FX is closed
proof
let T be TopSpace; ::_thesis: for FX being Subset-Family of T holds clf FX is closed
let FX be Subset-Family of T; ::_thesis: clf FX is closed
for V being Subset of T st V in clf FX holds
V is closed
proof
let V be Subset of T; ::_thesis: ( V in clf FX implies V is closed )
assume V in clf FX ; ::_thesis: V is closed
then ex W being Subset of T st
( V = Cl W & W in FX ) by Def2;
hence V is closed ; ::_thesis: verum
end;
hence clf FX is closed by TOPS_2:def_2; ::_thesis: verum
end;
theorem Th12: :: PCOMPS_1:12
for T being TopSpace
for FX being Subset-Family of T st FX = {} holds
clf FX = {}
proof
let T be TopSpace; ::_thesis: for FX being Subset-Family of T st FX = {} holds
clf FX = {}
let FX be Subset-Family of T; ::_thesis: ( FX = {} implies clf FX = {} )
reconsider CFX = clf FX as set ;
set X = the Element of CFX;
assume A1: FX = {} ; ::_thesis: clf FX = {}
A2: for X being set holds not X in CFX
proof
let X be set ; ::_thesis: not X in CFX
assume A3: X in CFX ; ::_thesis: contradiction
then reconsider X = X as Subset of T ;
ex V being Subset of T st
( X = Cl V & V in FX ) by A3, Def2;
hence contradiction by A1; ::_thesis: verum
end;
assume not clf FX = {} ; ::_thesis: contradiction
then the Element of CFX in CFX ;
hence contradiction by A2; ::_thesis: verum
end;
theorem Th13: :: PCOMPS_1:13
for T being non empty TopSpace
for V being Subset of T
for FX being Subset-Family of T st FX = {V} holds
clf FX = {(Cl V)}
proof
let T be non empty TopSpace; ::_thesis: for V being Subset of T
for FX being Subset-Family of T st FX = {V} holds
clf FX = {(Cl V)}
let V be Subset of T; ::_thesis: for FX being Subset-Family of T st FX = {V} holds
clf FX = {(Cl V)}
let FX be Subset-Family of T; ::_thesis: ( FX = {V} implies clf FX = {(Cl V)} )
reconsider CFX = clf FX as set ;
assume A1: FX = {V} ; ::_thesis: clf FX = {(Cl V)}
for W being set holds
( W in CFX iff W = Cl V )
proof
let W be set ; ::_thesis: ( W in CFX iff W = Cl V )
A2: ( W = Cl V implies W in CFX )
proof
assume A3: W = Cl V ; ::_thesis: W in CFX
ex X being Subset of T st
( W = Cl X & X in FX )
proof
take V ; ::_thesis: ( W = Cl V & V in FX )
thus ( W = Cl V & V in FX ) by A1, A3, TARSKI:def_1; ::_thesis: verum
end;
hence W in CFX by Def2; ::_thesis: verum
end;
( W in CFX implies W = Cl V )
proof
assume A4: W in CFX ; ::_thesis: W = Cl V
then reconsider W = W as Subset of T ;
ex X being Subset of T st
( W = Cl X & X in FX ) by A4, Def2;
hence W = Cl V by A1, TARSKI:def_1; ::_thesis: verum
end;
hence ( W in CFX iff W = Cl V ) by A2; ::_thesis: verum
end;
hence clf FX = {(Cl V)} by TARSKI:def_1; ::_thesis: verum
end;
theorem Th14: :: PCOMPS_1:14
for T being non empty TopSpace
for FX, GX being Subset-Family of T st FX c= GX holds
clf FX c= clf GX
proof
let T be non empty TopSpace; ::_thesis: for FX, GX being Subset-Family of T st FX c= GX holds
clf FX c= clf GX
let FX, GX be Subset-Family of T; ::_thesis: ( FX c= GX implies clf FX c= clf GX )
reconsider CFX = clf FX, CGX = clf GX as set ;
assume A1: FX c= GX ; ::_thesis: clf FX c= clf GX
for X being set st X in CFX holds
X in CGX
proof
let X be set ; ::_thesis: ( X in CFX implies X in CGX )
assume A2: X in CFX ; ::_thesis: X in CGX
then reconsider X = X as Subset of T ;
ex V being Subset of T st
( X = Cl V & V in FX ) by A2, Def2;
hence X in CGX by A1, Def2; ::_thesis: verum
end;
hence clf FX c= clf GX by TARSKI:def_3; ::_thesis: verum
end;
theorem Th15: :: PCOMPS_1:15
for T being non empty TopSpace
for FX, GX being Subset-Family of T holds clf (FX \/ GX) = (clf FX) \/ (clf GX)
proof
let T be non empty TopSpace; ::_thesis: for FX, GX being Subset-Family of T holds clf (FX \/ GX) = (clf FX) \/ (clf GX)
let FX, GX be Subset-Family of T; ::_thesis: clf (FX \/ GX) = (clf FX) \/ (clf GX)
for X being set holds
( X in clf (FX \/ GX) iff X in (clf FX) \/ (clf GX) )
proof
let X be set ; ::_thesis: ( X in clf (FX \/ GX) iff X in (clf FX) \/ (clf GX) )
A1: now__::_thesis:_(_X_in_(clf_FX)_\/_(clf_GX)_implies_X_in_clf_(FX_\/_GX)_)
assume A2: X in (clf FX) \/ (clf GX) ; ::_thesis: X in clf (FX \/ GX)
now__::_thesis:_X_in_clf_(FX_\/_GX)
percases ( X in clf FX or X in clf GX ) by A2, XBOOLE_0:def_3;
supposeA3: X in clf FX ; ::_thesis: X in clf (FX \/ GX)
then reconsider X9 = X as Subset of T ;
ex W being Subset of T st
( X9 = Cl W & W in FX \/ GX )
proof
consider Z being Subset of T such that
A4: ( X9 = Cl Z & Z in FX ) by A3, Def2;
take Z ; ::_thesis: ( X9 = Cl Z & Z in FX \/ GX )
thus ( X9 = Cl Z & Z in FX \/ GX ) by A4, XBOOLE_0:def_3; ::_thesis: verum
end;
hence X in clf (FX \/ GX) by Def2; ::_thesis: verum
end;
supposeA5: X in clf GX ; ::_thesis: X in clf (FX \/ GX)
then reconsider X9 = X as Subset of T ;
ex W being Subset of T st
( X9 = Cl W & W in FX \/ GX )
proof
consider Z being Subset of T such that
A6: ( X9 = Cl Z & Z in GX ) by A5, Def2;
take Z ; ::_thesis: ( X9 = Cl Z & Z in FX \/ GX )
thus ( X9 = Cl Z & Z in FX \/ GX ) by A6, XBOOLE_0:def_3; ::_thesis: verum
end;
hence X in clf (FX \/ GX) by Def2; ::_thesis: verum
end;
end;
end;
hence X in clf (FX \/ GX) ; ::_thesis: verum
end;
now__::_thesis:_(_X_in_clf_(FX_\/_GX)_implies_X_in_(clf_FX)_\/_(clf_GX)_)
assume A7: X in clf (FX \/ GX) ; ::_thesis: X in (clf FX) \/ (clf GX)
then reconsider X9 = X as Subset of T ;
consider W being Subset of T such that
A8: X9 = Cl W and
A9: W in FX \/ GX by A7, Def2;
now__::_thesis:_X9_in_(clf_FX)_\/_(clf_GX)
percases ( W in FX or W in GX ) by A9, XBOOLE_0:def_3;
suppose W in FX ; ::_thesis: X9 in (clf FX) \/ (clf GX)
then X9 in clf FX by A8, Def2;
hence X9 in (clf FX) \/ (clf GX) by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose W in GX ; ::_thesis: X9 in (clf FX) \/ (clf GX)
then X9 in clf GX by A8, Def2;
hence X9 in (clf FX) \/ (clf GX) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence X in (clf FX) \/ (clf GX) ; ::_thesis: verum
end;
hence ( X in clf (FX \/ GX) iff X in (clf FX) \/ (clf GX) ) by A1; ::_thesis: verum
end;
hence clf (FX \/ GX) = (clf FX) \/ (clf GX) by TARSKI:1; ::_thesis: verum
end;
theorem Th16: :: PCOMPS_1:16
for T being non empty TopSpace
for FX being Subset-Family of T st FX is finite holds
Cl (union FX) = union (clf FX)
proof
let T be non empty TopSpace; ::_thesis: for FX being Subset-Family of T st FX is finite holds
Cl (union FX) = union (clf FX)
let FX be Subset-Family of T; ::_thesis: ( FX is finite implies Cl (union FX) = union (clf FX) )
assume FX is finite ; ::_thesis: Cl (union FX) = union (clf FX)
then consider p being FinSequence such that
A1: rng p = FX by FINSEQ_1:52;
consider n being Nat such that
A2: dom p = Seg n by FINSEQ_1:def_2;
defpred S1[ Nat] means for GX being Subset-Family of T st GX = p .: (Seg $1) & $1 <= n & 1 <= n holds
Cl (union GX) = union (clf GX);
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: for GX being Subset-Family of T st GX = p .: (Seg k) & k <= n & 1 <= n holds
Cl (union GX) = union (clf GX) ; ::_thesis: S1[k + 1]
let GX be Subset-Family of T; ::_thesis: ( GX = p .: (Seg (k + 1)) & k + 1 <= n & 1 <= n implies Cl (union GX) = union (clf GX) )
assume A5: GX = p .: (Seg (k + 1)) ; ::_thesis: ( not k + 1 <= n or not 1 <= n or Cl (union GX) = union (clf GX) )
assume that
A6: k + 1 <= n and
A7: 1 <= n ; ::_thesis: Cl (union GX) = union (clf GX)
now__::_thesis:_Cl_(union_GX)_=_union_(clf_GX)
reconsider G2 = Im (p,(k + 1)) as Subset-Family of T by A1, RELAT_1:111, TOPS_2:2;
reconsider G1 = p .: (Seg k) as Subset-Family of T by A1, RELAT_1:111, TOPS_2:2;
k + 1 <= n + 1 by A6, NAT_1:12;
then A8: k <= n by XREAL_1:6;
0 + 1 = 1 ;
then 1 <= k + 1 by XREAL_1:7;
then k + 1 in dom p by A2, A6, FINSEQ_1:1;
then A9: G2 = {(p . (k + 1))} by FUNCT_1:59;
then union G2 = p . (k + 1) by ZFMISC_1:25;
then reconsider G3 = p . (k + 1) as Subset of T ;
A10: union (clf G2) = union {(Cl G3)} by A9, Th13
.= Cl G3 by ZFMISC_1:25
.= Cl (union G2) by A9, ZFMISC_1:25 ;
A11: p .: (Seg (k + 1)) = p .: ((Seg k) \/ {(k + 1)}) by FINSEQ_1:9
.= (p .: (Seg k)) \/ (p .: {(k + 1)}) by RELAT_1:120 ;
then Cl (union GX) = Cl ((union G1) \/ (union G2)) by A5, ZFMISC_1:78
.= (Cl (union G1)) \/ (Cl (union G2)) by PRE_TOPC:20 ;
then Cl (union GX) = (union (clf G1)) \/ (union (clf G2)) by A4, A7, A10, A8;
then Cl (union GX) = union ((clf G1) \/ (clf G2)) by ZFMISC_1:78;
hence Cl (union GX) = union (clf GX) by A5, A11, Th15; ::_thesis: verum
end;
hence Cl (union GX) = union (clf GX) ; ::_thesis: verum
end;
A12: S1[ 0 ]
proof
let GX be Subset-Family of T; ::_thesis: ( GX = p .: (Seg 0) & 0 <= n & 1 <= n implies Cl (union GX) = union (clf GX) )
assume that
A13: GX = p .: (Seg 0) and
0 <= n and
1 <= n ; ::_thesis: Cl (union GX) = union (clf GX)
union GX = {} T by A13, ZFMISC_1:2;
then Cl (union GX) = {} T by PRE_TOPC:22;
hence Cl (union GX) = union (clf GX) by A13, Th12, ZFMISC_1:2; ::_thesis: verum
end;
A14: for k being Nat holds S1[k] from NAT_1:sch_2(A12, A3);
A15: now__::_thesis:_(_1_<=_n_implies_Cl_(union_FX)_=_union_(clf_FX)_)
assume A16: 1 <= n ; ::_thesis: Cl (union FX) = union (clf FX)
FX = p .: (Seg n) by A1, A2, RELAT_1:113;
hence Cl (union FX) = union (clf FX) by A14, A16; ::_thesis: verum
end;
A17: now__::_thesis:_(_n_=_0_implies_Cl_(union_FX)_=_union_(clf_FX)_)
assume n = 0 ; ::_thesis: Cl (union FX) = union (clf FX)
then Seg n = {} ;
then A18: FX = p .: {} by A1, A2, RELAT_1:113;
then union FX = {} T by ZFMISC_1:2;
then Cl (union FX) = {} T by PRE_TOPC:22;
hence Cl (union FX) = union (clf FX) by A18, Th12, ZFMISC_1:2; ::_thesis: verum
end;
now__::_thesis:_(_n_<>_0_implies_1_<=_n_)
A19: 1 = 0 + 1 ;
assume n <> 0 ; ::_thesis: 1 <= n
hence 1 <= n by A19, NAT_1:13; ::_thesis: verum
end;
hence Cl (union FX) = union (clf FX) by A15, A17; ::_thesis: verum
end;
theorem Th17: :: PCOMPS_1:17
for T being non empty TopSpace
for FX being Subset-Family of T holds FX is_finer_than clf FX
proof
let T be non empty TopSpace; ::_thesis: for FX being Subset-Family of T holds FX is_finer_than clf FX
let FX be Subset-Family of T; ::_thesis: FX is_finer_than clf FX
set GX = clf FX;
for X being set st X in FX holds
ex Y being set st
( Y in clf FX & X c= Y )
proof
let X be set ; ::_thesis: ( X in FX implies ex Y being set st
( Y in clf FX & X c= Y ) )
assume A1: X in FX ; ::_thesis: ex Y being set st
( Y in clf FX & X c= Y )
then reconsider X = X as Subset of T ;
thus ex Y being set st
( Y in clf FX & X c= Y ) ::_thesis: verum
proof
reconsider Y = Cl X as set ;
take Y ; ::_thesis: ( Y in clf FX & X c= Y )
thus Y in clf FX by A1, Def2; ::_thesis: X c= Y
thus X c= Y by PRE_TOPC:18; ::_thesis: verum
end;
end;
hence FX is_finer_than clf FX by SETFAM_1:def_2; ::_thesis: verum
end;
scheme :: PCOMPS_1:sch 1
Lambda1top{ F1() -> TopSpace, F2() -> Subset-Family of F1(), F3() -> Subset-Family of F1(), F4( set ) -> Subset of F1() } :
ex f being Function of F2(),F3() st
for Z being Subset of F1() st Z in F2() holds
f . Z = F4(Z)
provided
A1: for Z being Subset of F1() st Z in F2() holds
F4(Z) in F3()
proof
A2: for x being set st x in F2() holds
F4(x) in F3() by A1;
consider f being Function of F2(),F3() such that
A3: for x being set st x in F2() holds
f . x = F4(x) from FUNCT_2:sch_2(A2);
take f ; ::_thesis: for Z being Subset of F1() st Z in F2() holds
f . Z = F4(Z)
thus for Z being Subset of F1() st Z in F2() holds
f . Z = F4(Z) by A3; ::_thesis: verum
end;
theorem :: PCOMPS_1:18
for T being non empty TopSpace
for FX being Subset-Family of T st FX is locally_finite holds
clf FX is locally_finite
proof
let T be non empty TopSpace; ::_thesis: for FX being Subset-Family of T st FX is locally_finite holds
clf FX is locally_finite
let FX be Subset-Family of T; ::_thesis: ( FX is locally_finite implies clf FX is locally_finite )
set GX = clf FX;
assume A1: FX is locally_finite ; ::_thesis: clf FX is locally_finite
for x being Point of T ex W being Subset of T st
( x in W & W is open & { V where V is Subset of T : ( V in clf FX & V meets W ) } is finite )
proof
let x be Point of T; ::_thesis: ex W being Subset of T st
( x in W & W is open & { V where V is Subset of T : ( V in clf FX & V meets W ) } is finite )
thus ex W being Subset of T st
( x in W & W is open & { V where V is Subset of T : ( V in clf FX & V meets W ) } is finite ) ::_thesis: verum
proof
deffunc H1( Subset of T) -> Element of bool the carrier of T = Cl $1;
consider W being Subset of T such that
A2: x in W and
A3: W is open and
A4: { V where V is Subset of T : ( V in FX & V meets W ) } is finite by A1, Def1;
take W ; ::_thesis: ( x in W & W is open & { V where V is Subset of T : ( V in clf FX & V meets W ) } is finite )
thus x in W by A2; ::_thesis: ( W is open & { V where V is Subset of T : ( V in clf FX & V meets W ) } is finite )
thus W is open by A3; ::_thesis: { V where V is Subset of T : ( V in clf FX & V meets W ) } is finite
set CGX = { V where V is Subset of T : ( V in clf FX & V meets W ) } ;
set CFX = { V where V is Subset of T : ( V in FX & V meets W ) } ;
A5: for Y being Subset of T st Y in FX holds
H1(Y) in clf FX by Def2;
consider f being Function of FX,(clf FX) such that
A6: for X being Subset of T st X in FX holds
f . X = H1(X) from PCOMPS_1:sch_1(A5);
A7: ( clf FX = {} implies FX = {} ) by Th17, SETFAM_1:16;
then A8: dom f = FX by FUNCT_2:def_1;
for Z being set holds
( Z in f .: { V where V is Subset of T : ( V in FX & V meets W ) } iff Z in { V where V is Subset of T : ( V in clf FX & V meets W ) } )
proof
let Z be set ; ::_thesis: ( Z in f .: { V where V is Subset of T : ( V in FX & V meets W ) } iff Z in { V where V is Subset of T : ( V in clf FX & V meets W ) } )
A9: ( Z in { V where V is Subset of T : ( V in clf FX & V meets W ) } implies Z in f .: { V where V is Subset of T : ( V in FX & V meets W ) } )
proof
assume A10: Z in { V where V is Subset of T : ( V in clf FX & V meets W ) } ; ::_thesis: Z in f .: { V where V is Subset of T : ( V in FX & V meets W ) }
ex Y being set st
( Y in dom f & Y in { V where V is Subset of T : ( V in FX & V meets W ) } & Z = f . Y )
proof
consider V being Subset of T such that
A11: Z = V and
A12: V in clf FX and
A13: V meets W by A10;
consider X being Subset of T such that
A14: V = Cl X and
A15: X in FX by A12, Def2;
take X ; ::_thesis: ( X in dom f & X in { V where V is Subset of T : ( V in FX & V meets W ) } & Z = f . X )
A16: V /\ W <> {} by A13, XBOOLE_0:def_7;
ex Q being Subset of T st
( X = Q & Q in FX & Q meets W )
proof
take Q = X; ::_thesis: ( X = Q & Q in FX & Q meets W )
thus X = Q ; ::_thesis: ( Q in FX & Q meets W )
thus Q in FX by A15; ::_thesis: Q meets W
Cl (W /\ (Cl Q)) <> {} by A16, A14, Th2;
then Cl (W /\ Q) <> {} by A3, TOPS_1:14;
then Q /\ W <> {} by Th2;
hence Q meets W by XBOOLE_0:def_7; ::_thesis: verum
end;
hence ( X in dom f & X in { V where V is Subset of T : ( V in FX & V meets W ) } & Z = f . X ) by A6, A7, A11, A14, FUNCT_2:def_1; ::_thesis: verum
end;
hence Z in f .: { V where V is Subset of T : ( V in FX & V meets W ) } by FUNCT_1:def_6; ::_thesis: verum
end;
( Z in f .: { V where V is Subset of T : ( V in FX & V meets W ) } implies Z in { V where V is Subset of T : ( V in clf FX & V meets W ) } )
proof
assume Z in f .: { V where V is Subset of T : ( V in FX & V meets W ) } ; ::_thesis: Z in { V where V is Subset of T : ( V in clf FX & V meets W ) }
then consider Y being set such that
A17: Y in dom f and
A18: Y in { V where V is Subset of T : ( V in FX & V meets W ) } and
A19: Z = f . Y by FUNCT_1:def_6;
reconsider Y = Y as Subset of T by A8, A17;
A20: f . Y = Cl Y by A6, A8, A17;
then reconsider Z = Z as Subset of T by A19;
ex V being Subset of T st
( Y = V & V in FX & V meets W ) by A18;
then A21: Z meets W by A19, A20, PRE_TOPC:18, XBOOLE_1:63;
Z in clf FX by A8, A17, A19, A20, Def2;
hence Z in { V where V is Subset of T : ( V in clf FX & V meets W ) } by A21; ::_thesis: verum
end;
hence ( Z in f .: { V where V is Subset of T : ( V in FX & V meets W ) } iff Z in { V where V is Subset of T : ( V in clf FX & V meets W ) } ) by A9; ::_thesis: verum
end;
hence { V where V is Subset of T : ( V in clf FX & V meets W ) } is finite by A4, TARSKI:1; ::_thesis: verum
end;
end;
hence clf FX is locally_finite by Def1; ::_thesis: verum
end;
theorem :: PCOMPS_1:19
for T being non empty TopSpace
for FX being Subset-Family of T holds union FX c= union (clf FX) by Th17, SETFAM_1:13;
theorem Th20: :: PCOMPS_1:20
for T being non empty TopSpace
for FX being Subset-Family of T st FX is locally_finite holds
Cl (union FX) = union (clf FX)
proof
let T be non empty TopSpace; ::_thesis: for FX being Subset-Family of T st FX is locally_finite holds
Cl (union FX) = union (clf FX)
let FX be Subset-Family of T; ::_thesis: ( FX is locally_finite implies Cl (union FX) = union (clf FX) )
set UFX = Cl (union FX);
set UCFX = union (clf FX);
assume A1: FX is locally_finite ; ::_thesis: Cl (union FX) = union (clf FX)
for x being Point of T st x in Cl (union FX) holds
x in union (clf FX)
proof
let x be Point of T; ::_thesis: ( x in Cl (union FX) implies x in union (clf FX) )
consider W being Subset of T such that
A2: ( x in W & W is open ) and
A3: { V where V is Subset of T : ( V in FX & V meets W ) } is finite by A1, Def1;
set HX = { V where V is Subset of T : ( V in FX & V meets W ) } ;
reconsider HX = { V where V is Subset of T : ( V in FX & V meets W ) } as Subset-Family of T by Th8, TOPS_2:2;
A4: Cl (union HX) = union (clf HX) by A3, Th16;
set FHX = FX \ HX;
A5: not x in Cl (union (FX \ HX))
proof
assume A6: x in Cl (union (FX \ HX)) ; ::_thesis: contradiction
reconsider FHX = FX \ HX as set ;
for Z being set st Z in FHX holds
Z misses W
proof
let Z be set ; ::_thesis: ( Z in FHX implies Z misses W )
assume A7: Z in FHX ; ::_thesis: Z misses W
then reconsider Z = Z as Subset of T ;
( Z in FX & not Z in HX ) by A7, XBOOLE_0:def_5;
hence Z misses W ; ::_thesis: verum
end;
then union FHX misses W by ZFMISC_1:80;
hence contradiction by A2, A6, TOPS_1:12; ::_thesis: verum
end;
HX \/ (FX \ HX) = HX \/ FX by XBOOLE_1:39
.= FX by Th8, XBOOLE_1:12 ;
then A8: Cl (union FX) = Cl ((union HX) \/ (union (FX \ HX))) by ZFMISC_1:78
.= (Cl (union HX)) \/ (Cl (union (FX \ HX))) by PRE_TOPC:20 ;
clf HX c= clf FX by Th8, Th14;
then A9: union (clf HX) c= union (clf FX) by ZFMISC_1:77;
assume x in Cl (union FX) ; ::_thesis: x in union (clf FX)
then x in Cl (union HX) by A5, A8, XBOOLE_0:def_3;
hence x in union (clf FX) by A4, A9; ::_thesis: verum
end;
then A10: Cl (union FX) c= union (clf FX) by SUBSET_1:2;
for x being Point of T st x in union (clf FX) holds
x in Cl (union FX)
proof
let x be Point of T; ::_thesis: ( x in union (clf FX) implies x in Cl (union FX) )
assume x in union (clf FX) ; ::_thesis: x in Cl (union FX)
then consider X being set such that
A11: x in X and
A12: X in clf FX by TARSKI:def_4;
reconsider X = X as Subset of T by A12;
consider Y being Subset of T such that
A13: X = Cl Y and
A14: Y in FX by A12, Def2;
for A being Subset of T st A is open & x in A holds
union FX meets A
proof
let A be Subset of T; ::_thesis: ( A is open & x in A implies union FX meets A )
assume A15: ( A is open & x in A ) ; ::_thesis: union FX meets A
ex y being Point of T st y in (union FX) /\ A
proof
Y meets A by A11, A13, A15, TOPS_1:12;
then consider z being set such that
A16: z in Y /\ A by XBOOLE_0:4;
z in Y by A16, XBOOLE_0:def_4;
then A17: z in union FX by A14, TARSKI:def_4;
take z ; ::_thesis: ( z is Point of T & z in (union FX) /\ A )
z in A by A16, XBOOLE_0:def_4;
hence ( z is Point of T & z in (union FX) /\ A ) by A17, XBOOLE_0:def_4; ::_thesis: verum
end;
hence union FX meets A by XBOOLE_0:4; ::_thesis: verum
end;
hence x in Cl (union FX) by TOPS_1:12; ::_thesis: verum
end;
then union (clf FX) c= Cl (union FX) by SUBSET_1:2;
hence Cl (union FX) = union (clf FX) by A10, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: PCOMPS_1:21
for T being non empty TopSpace
for FX being Subset-Family of T st FX is locally_finite & FX is closed holds
union FX is closed
proof
let T be non empty TopSpace; ::_thesis: for FX being Subset-Family of T st FX is locally_finite & FX is closed holds
union FX is closed
let FX be Subset-Family of T; ::_thesis: ( FX is locally_finite & FX is closed implies union FX is closed )
assume that
A1: FX is locally_finite and
A2: FX is closed ; ::_thesis: union FX is closed
union (clf FX) c= union FX
proof
set UFX = union FX;
set UCFX = union (clf FX);
for x being Point of T st x in union (clf FX) holds
x in union FX
proof
let x be Point of T; ::_thesis: ( x in union (clf FX) implies x in union FX )
assume x in union (clf FX) ; ::_thesis: x in union FX
then consider X being set such that
A3: x in X and
A4: X in clf FX by TARSKI:def_4;
reconsider X = X as Subset of T by A4;
consider W being Subset of T such that
A5: X = Cl W and
A6: W in FX by A4, Def2;
reconsider W = W as Subset of T ;
W is closed by A2, A6, TOPS_2:def_2;
then x in W by A3, A5, PRE_TOPC:22;
hence x in union FX by A6, TARSKI:def_4; ::_thesis: verum
end;
hence union (clf FX) c= union FX by SUBSET_1:2; ::_thesis: verum
end;
then A7: Cl (union FX) c= union FX by A1, Th20;
union FX c= union (clf FX) by Th17, SETFAM_1:13;
then union FX c= Cl (union FX) by A1, Th20;
hence union FX is closed by A7, XBOOLE_0:def_10; ::_thesis: verum
end;
definition
let IT be TopStruct ;
attrIT is paracompact means :Def3: :: PCOMPS_1:def 3
for FX being Subset-Family of IT st FX is Cover of IT & FX is open holds
ex GX being Subset-Family of IT st
( GX is open & GX is Cover of IT & GX is_finer_than FX & GX is locally_finite );
end;
:: deftheorem Def3 defines paracompact PCOMPS_1:def_3_:_
for IT being TopStruct holds
( IT is paracompact iff for FX being Subset-Family of IT st FX is Cover of IT & FX is open holds
ex GX being Subset-Family of IT st
( GX is open & GX is Cover of IT & GX is_finer_than FX & GX is locally_finite ) );
registration
cluster non empty TopSpace-like paracompact for TopStruct ;
existence
ex b1 being non empty TopSpace st b1 is paracompact
proof
take PT = 1TopSp {1}; ::_thesis: PT is paracompact
let FX be Subset-Family of PT; :: according to PCOMPS_1:def_3 ::_thesis: ( FX is Cover of PT & FX is open implies ex GX being Subset-Family of PT st
( GX is open & GX is Cover of PT & GX is_finer_than FX & GX is locally_finite ) )
assume that
A1: FX is Cover of PT and
FX is open ; ::_thesis: ex GX being Subset-Family of PT st
( GX is open & GX is Cover of PT & GX is_finer_than FX & GX is locally_finite )
consider GX being Subset-Family of PT such that
A2: ( GX c= FX & GX is Cover of PT ) and
GX is finite by A1;
take GX ; ::_thesis: ( GX is open & GX is Cover of PT & GX is_finer_than FX & GX is locally_finite )
thus ( GX is open & GX is Cover of PT & GX is_finer_than FX & GX is locally_finite ) by A2, Th10, SETFAM_1:12, TOPS_2:11; ::_thesis: verum
end;
end;
theorem :: PCOMPS_1:22
for T being non empty TopSpace st T is compact holds
T is paracompact
proof
let T be non empty TopSpace; ::_thesis: ( T is compact implies T is paracompact )
assume A1: T is compact ; ::_thesis: T is paracompact
for FX being Subset-Family of T st FX is Cover of T & FX is open holds
ex GX being Subset-Family of T st
( GX is open & GX is Cover of T & GX is_finer_than FX & GX is locally_finite )
proof
let FX be Subset-Family of T; ::_thesis: ( FX is Cover of T & FX is open implies ex GX being Subset-Family of T st
( GX is open & GX is Cover of T & GX is_finer_than FX & GX is locally_finite ) )
assume that
A2: FX is Cover of T and
A3: FX is open ; ::_thesis: ex GX being Subset-Family of T st
( GX is open & GX is Cover of T & GX is_finer_than FX & GX is locally_finite )
consider GX being Subset-Family of T such that
A4: GX c= FX and
A5: GX is Cover of T and
A6: GX is finite by A1, A2, A3, COMPTS_1:def_1;
take GX ; ::_thesis: ( GX is open & GX is Cover of T & GX is_finer_than FX & GX is locally_finite )
for W being Subset of T st W in GX holds
W is open by A3, A4, TOPS_2:def_1;
hence GX is open by TOPS_2:def_1; ::_thesis: ( GX is Cover of T & GX is_finer_than FX & GX is locally_finite )
thus GX is Cover of T by A5; ::_thesis: ( GX is_finer_than FX & GX is locally_finite )
thus GX is_finer_than FX by A4, SETFAM_1:12; ::_thesis: GX is locally_finite
thus GX is locally_finite by A6, Th10; ::_thesis: verum
end;
hence T is paracompact by Def3; ::_thesis: verum
end;
theorem Th23: :: PCOMPS_1:23
for T being non empty TopSpace
for B, A being Subset of T st T is paracompact & B is closed & ( for x being Point of T st x in B holds
ex V, W being Subset of T st
( V is open & W is open & A c= V & x in W & V misses W ) ) holds
ex Y, Z being Subset of T st
( Y is open & Z is open & A c= Y & B c= Z & Y misses Z )
proof
let T be non empty TopSpace; ::_thesis: for B, A being Subset of T st T is paracompact & B is closed & ( for x being Point of T st x in B holds
ex V, W being Subset of T st
( V is open & W is open & A c= V & x in W & V misses W ) ) holds
ex Y, Z being Subset of T st
( Y is open & Z is open & A c= Y & B c= Z & Y misses Z )
let B, A be Subset of T; ::_thesis: ( T is paracompact & B is closed & ( for x being Point of T st x in B holds
ex V, W being Subset of T st
( V is open & W is open & A c= V & x in W & V misses W ) ) implies ex Y, Z being Subset of T st
( Y is open & Z is open & A c= Y & B c= Z & Y misses Z ) )
assume that
A1: T is paracompact and
A2: B is closed and
A3: for x being Point of T st x in B holds
ex V, W being Subset of T st
( V is open & W is open & A c= V & x in W & V misses W ) ; ::_thesis: ex Y, Z being Subset of T st
( Y is open & Z is open & A c= Y & B c= Z & Y misses Z )
defpred S1[ set ] means ( $1 = B ` or ex V, W being Subset of T ex x being Point of T st
( x in B & $1 = W & V is open & W is open & A c= V & x in W & V misses W ) );
consider GX being Subset-Family of T such that
A4: for X being Subset of T holds
( X in GX iff S1[X] ) from SUBSET_1:sch_3();
now__::_thesis:_for_x_being_Point_of_T_st_x_in_[#]_T_holds_
x_in_union_GX
let x be Point of T; ::_thesis: ( x in [#] T implies x in union GX )
assume x in [#] T ; ::_thesis: x in union GX
then A5: x in B \/ (B `) by PRE_TOPC:2;
now__::_thesis:_x_in_union_GX
percases ( x in B or x in B ` ) by A5, XBOOLE_0:def_3;
supposeA6: x in B ; ::_thesis: x in union GX
ex X being Subset of T st
( x in X & X in GX )
proof
consider V, W being Subset of T such that
A7: ( V is open & W is open & A c= V ) and
A8: x in W and
A9: V misses W by A3, A6;
take X = W; ::_thesis: ( x in X & X in GX )
thus x in X by A8; ::_thesis: X in GX
thus X in GX by A4, A6, A7, A8, A9; ::_thesis: verum
end;
hence x in union GX by TARSKI:def_4; ::_thesis: verum
end;
supposeA10: x in B ` ; ::_thesis: x in union GX
ex X being Subset of T st
( x in X & X in GX )
proof
take X = B ` ; ::_thesis: ( x in X & X in GX )
thus x in X by A10; ::_thesis: X in GX
thus X in GX by A4; ::_thesis: verum
end;
hence x in union GX by TARSKI:def_4; ::_thesis: verum
end;
end;
end;
hence x in union GX ; ::_thesis: verum
end;
then [#] T c= union GX by SUBSET_1:2;
then [#] T = union GX by XBOOLE_0:def_10;
then A11: GX is Cover of T by SETFAM_1:45;
for X being Subset of T st X in GX holds
X is open
proof
let X be Subset of T; ::_thesis: ( X in GX implies X is open )
assume A12: X in GX ; ::_thesis: X is open
now__::_thesis:_X_is_open
percases ( X = B ` or ex V, W being Subset of T ex y being Point of T st
( y in B & X = W & V is open & W is open & A c= V & y in W & V misses W ) ) by A4, A12;
suppose X = B ` ; ::_thesis: X is open
hence X is open by A2; ::_thesis: verum
end;
suppose ex V, W being Subset of T ex y being Point of T st
( y in B & X = W & V is open & W is open & A c= V & y in W & V misses W ) ; ::_thesis: X is open
hence X is open ; ::_thesis: verum
end;
end;
end;
hence X is open ; ::_thesis: verum
end;
then GX is open by TOPS_2:def_1;
then consider FX being Subset-Family of T such that
A13: FX is open and
A14: FX is Cover of T and
A15: FX is_finer_than GX and
A16: FX is locally_finite by A1, A11, Def3;
set HX = { W where W is Subset of T : ( W in FX & W meets B ) } ;
A17: { W where W is Subset of T : ( W in FX & W meets B ) } c= FX by Th8;
reconsider HX = { W where W is Subset of T : ( W in FX & W meets B ) } as Subset-Family of T by Th8, TOPS_2:2;
take Y = (union (clf HX)) ` ; ::_thesis: ex Z being Subset of T st
( Y is open & Z is open & A c= Y & B c= Z & Y misses Z )
take Z = union HX; ::_thesis: ( Y is open & Z is open & A c= Y & B c= Z & Y misses Z )
union (clf HX) = Cl (union HX) by A16, A17, Th9, Th20;
hence Y is open ; ::_thesis: ( Z is open & A c= Y & B c= Z & Y misses Z )
thus Z is open by A13, A17, TOPS_2:11, TOPS_2:19; ::_thesis: ( A c= Y & B c= Z & Y misses Z )
A18: for X being Subset of T st X in HX holds
A /\ (Cl X) = {}
proof
let X be Subset of T; ::_thesis: ( X in HX implies A /\ (Cl X) = {} )
assume X in HX ; ::_thesis: A /\ (Cl X) = {}
then A19: ex W being Subset of T st
( W = X & W in FX & W meets B ) ;
then consider Y being set such that
A20: Y in GX and
A21: X c= Y by A15, SETFAM_1:def_2;
reconsider Y = Y as Subset of T by A20;
now__::_thesis:_A_/\_(Cl_X)_=_{}
percases ( Y = B ` or ex V, W being Subset of T ex y being Point of T st
( y in B & Y = W & V is open & W is open & A c= V & y in W & V misses W ) ) by A4, A20;
suppose Y = B ` ; ::_thesis: A /\ (Cl X) = {}
hence A /\ (Cl X) = {} by A19, A21, XBOOLE_1:63, XBOOLE_1:79; ::_thesis: verum
end;
suppose ex V, W being Subset of T ex y being Point of T st
( y in B & Y = W & V is open & W is open & A c= V & y in W & V misses W ) ; ::_thesis: A /\ (Cl X) = {}
then consider V, W being Subset of T, y being Point of T such that
y in B and
A22: Y = W and
A23: V is open and
W is open and
A24: A c= V and
y in W and
A25: V misses W ;
V misses X by A21, A22, A25, XBOOLE_1:63;
then Cl (V /\ X) = Cl ({} T) by XBOOLE_0:def_7;
then Cl (V /\ X) = {} by PRE_TOPC:22;
then Cl (V /\ (Cl X)) = {} by A23, TOPS_1:14;
then V /\ (Cl X) = {} by Th2;
then Cl X misses V by XBOOLE_0:def_7;
then A misses Cl X by A24, XBOOLE_1:63;
hence A /\ (Cl X) = {} by XBOOLE_0:def_7; ::_thesis: verum
end;
end;
end;
hence A /\ (Cl X) = {} ; ::_thesis: verum
end;
A misses union (clf HX)
proof
assume A meets union (clf HX) ; ::_thesis: contradiction
then consider x being set such that
A26: x in A and
A27: x in union (clf HX) by XBOOLE_0:3;
reconsider x = x as Point of T by A26;
now__::_thesis:_(_x_in_union_(clf_HX)_implies_not_x_in_A_)
assume x in union (clf HX) ; ::_thesis: not x in A
then consider X being set such that
A28: x in X and
A29: X in clf HX by TARSKI:def_4;
reconsider X = X as Subset of T by A29;
ex W being Subset of T st
( X = Cl W & W in HX ) by A29, Def2;
then A /\ X = {} by A18;
then A misses X by XBOOLE_0:def_7;
hence not x in A by A28, XBOOLE_0:3; ::_thesis: verum
end;
hence contradiction by A26, A27; ::_thesis: verum
end;
hence A c= Y by SUBSET_1:23; ::_thesis: ( B c= Z & Y misses Z )
now__::_thesis:_for_y_being_Point_of_T_st_y_in_B_holds_
y_in_Z
let y be Point of T; ::_thesis: ( y in B implies y in Z )
assume A30: y in B ; ::_thesis: y in Z
ex W being Subset of T st
( y in W & W in HX )
proof
consider W being Subset of T such that
A31: y in W and
A32: W in FX by A14, Th3;
take W ; ::_thesis: ( y in W & W in HX )
thus y in W by A31; ::_thesis: W in HX
W meets B by A30, A31, XBOOLE_0:3;
hence W in HX by A32; ::_thesis: verum
end;
hence y in Z by TARSKI:def_4; ::_thesis: verum
end;
hence B c= Z by SUBSET_1:2; ::_thesis: Y misses Z
Z c= Y ` by Th17, SETFAM_1:13;
hence Y misses Z by SUBSET_1:23; ::_thesis: verum
end;
theorem Th24: :: PCOMPS_1:24
for T being non empty TopSpace st T is T_2 & T is paracompact holds
T is regular
proof
let T be non empty TopSpace; ::_thesis: ( T is T_2 & T is paracompact implies T is regular )
assume A1: T is T_2 ; ::_thesis: ( not T is paracompact or T is regular )
assume A2: T is paracompact ; ::_thesis: T is regular
for x being Point of T
for A being Subset of T st A <> {} & A is closed & x in A ` holds
ex W, V being Subset of T st
( W is open & V is open & x in W & A c= V & W misses V )
proof
let x be Point of T; ::_thesis: for A being Subset of T st A <> {} & A is closed & x in A ` holds
ex W, V being Subset of T st
( W is open & V is open & x in W & A c= V & W misses V )
let A be Subset of T; ::_thesis: ( A <> {} & A is closed & x in A ` implies ex W, V being Subset of T st
( W is open & V is open & x in W & A c= V & W misses V ) )
assume that
A <> {} and
A3: A is closed and
A4: x in A ` ; ::_thesis: ex W, V being Subset of T st
( W is open & V is open & x in W & A c= V & W misses V )
set B = {x};
A5: not x in A by A4, XBOOLE_0:def_5;
for y being Point of T st y in A holds
ex V, W being Subset of T st
( V is open & W is open & {x} c= V & y in W & V misses W )
proof
let y be Point of T; ::_thesis: ( y in A implies ex V, W being Subset of T st
( V is open & W is open & {x} c= V & y in W & V misses W ) )
assume y in A ; ::_thesis: ex V, W being Subset of T st
( V is open & W is open & {x} c= V & y in W & V misses W )
then consider V, W being Subset of T such that
A6: ( V is open & W is open & x in V & y in W & V misses W ) by A1, A5, PRE_TOPC:def_10;
take V ; ::_thesis: ex W being Subset of T st
( V is open & W is open & {x} c= V & y in W & V misses W )
take W ; ::_thesis: ( V is open & W is open & {x} c= V & y in W & V misses W )
thus ( V is open & W is open & {x} c= V & y in W & V misses W ) by A6, ZFMISC_1:31; ::_thesis: verum
end;
then consider Y, Z being Subset of T such that
A7: ( Y is open & Z is open & {x} c= Y & A c= Z & Y misses Z ) by A2, A3, Th23;
take Y ; ::_thesis: ex V being Subset of T st
( Y is open & V is open & x in Y & A c= V & Y misses V )
take Z ; ::_thesis: ( Y is open & Z is open & x in Y & A c= Z & Y misses Z )
thus ( Y is open & Z is open & x in Y & A c= Z & Y misses Z ) by A7, ZFMISC_1:31; ::_thesis: verum
end;
hence T is regular by COMPTS_1:def_2; ::_thesis: verum
end;
theorem :: PCOMPS_1:25
for T being non empty TopSpace st T is T_2 & T is paracompact holds
T is normal
proof
let T be non empty TopSpace; ::_thesis: ( T is T_2 & T is paracompact implies T is normal )
assume that
A1: T is T_2 and
A2: T is paracompact ; ::_thesis: T is normal
for A, B being Subset of T st A <> {} & B <> {} & A is closed & B is closed & A misses B holds
ex W, V being Subset of T st
( W is open & V is open & A c= W & B c= V & W misses V )
proof
let A, B be Subset of T; ::_thesis: ( A <> {} & B <> {} & A is closed & B is closed & A misses B implies ex W, V being Subset of T st
( W is open & V is open & A c= W & B c= V & W misses V ) )
assume that
A3: A <> {} and
B <> {} and
A4: A is closed and
A5: B is closed and
A6: A misses B ; ::_thesis: ex W, V being Subset of T st
( W is open & V is open & A c= W & B c= V & W misses V )
for x being Point of T st x in B holds
ex W, V being Subset of T st
( W is open & V is open & A c= W & x in V & W misses V )
proof
let x be Point of T; ::_thesis: ( x in B implies ex W, V being Subset of T st
( W is open & V is open & A c= W & x in V & W misses V ) )
assume x in B ; ::_thesis: ex W, V being Subset of T st
( W is open & V is open & A c= W & x in V & W misses V )
then not x in A by A6, XBOOLE_0:3;
then A7: x in A ` by SUBSET_1:29;
T is regular by A1, A2, Th24;
then consider V, W being Subset of T such that
A8: ( V is open & W is open & x in V & A c= W & V misses W ) by A3, A4, A7, COMPTS_1:def_2;
take W ; ::_thesis: ex V being Subset of T st
( W is open & V is open & A c= W & x in V & W misses V )
take V ; ::_thesis: ( W is open & V is open & A c= W & x in V & W misses V )
thus ( W is open & V is open & A c= W & x in V & W misses V ) by A8; ::_thesis: verum
end;
then consider Y, Z being Subset of T such that
A9: ( Y is open & Z is open & A c= Y & B c= Z & Y misses Z ) by A2, A5, Th23;
take Y ; ::_thesis: ex V being Subset of T st
( Y is open & V is open & A c= Y & B c= V & Y misses V )
take Z ; ::_thesis: ( Y is open & Z is open & A c= Y & B c= Z & Y misses Z )
thus ( Y is open & Z is open & A c= Y & B c= Z & Y misses Z ) by A9; ::_thesis: verum
end;
hence T is normal by COMPTS_1:def_3; ::_thesis: verum
end;
definition
let PM be MetrStruct ;
func Family_open_set PM -> Subset-Family of PM means :Def4: :: PCOMPS_1:def 4
for V being Subset of PM holds
( V in it iff for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) );
existence
ex b1 being Subset-Family of PM st
for V being Subset of PM holds
( V in b1 iff for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) )
proof
defpred S1[ set ] means for x being Element of PM st x in $1 holds
ex r being Real st
( r > 0 & Ball (x,r) c= $1 );
thus ex S being Subset-Family of PM st
for V being Subset of PM holds
( V in S iff S1[V] ) from SUBSET_1:sch_3(); ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset-Family of PM st ( for V being Subset of PM holds
( V in b1 iff for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) ) ) & ( for V being Subset of PM holds
( V in b2 iff for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) ) ) holds
b1 = b2
proof
let FX, GX be Subset-Family of PM; ::_thesis: ( ( for V being Subset of PM holds
( V in FX iff for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) ) ) & ( for V being Subset of PM holds
( V in GX iff for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) ) ) implies FX = GX )
assume A1: for V being Subset of PM holds
( V in FX iff for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) ) ; ::_thesis: ( ex V being Subset of PM st
( ( V in GX implies for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) ) implies ( ( for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) ) & not V in GX ) ) or FX = GX )
assume A2: for W being Subset of PM holds
( W in GX iff for y being Element of PM st y in W holds
ex p being Real st
( p > 0 & Ball (y,p) c= W ) ) ; ::_thesis: FX = GX
for Y being Subset of PM holds
( Y in FX iff Y in GX )
proof
let Y be Subset of PM; ::_thesis: ( Y in FX iff Y in GX )
A3: now__::_thesis:_(_Y_in_GX_implies_Y_in_FX_)
assume Y in GX ; ::_thesis: Y in FX
then for x being Element of PM st x in Y holds
ex r being Real st
( r > 0 & Ball (x,r) c= Y ) by A2;
hence Y in FX by A1; ::_thesis: verum
end;
now__::_thesis:_(_Y_in_FX_implies_Y_in_GX_)
assume Y in FX ; ::_thesis: Y in GX
then for x being Element of PM st x in Y holds
ex r being Real st
( r > 0 & Ball (x,r) c= Y ) by A1;
hence Y in GX by A2; ::_thesis: verum
end;
hence ( Y in FX iff Y in GX ) by A3; ::_thesis: verum
end;
hence FX = GX by SETFAM_1:31; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines Family_open_set PCOMPS_1:def_4_:_
for PM being MetrStruct
for b2 being Subset-Family of PM holds
( b2 = Family_open_set PM iff for V being Subset of PM holds
( V in b2 iff for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) ) );
theorem Th26: :: PCOMPS_1:26
for PM being MetrStruct
for x being Element of PM ex r being Real st
( r > 0 & Ball (x,r) c= the carrier of PM )
proof
let PM be MetrStruct ; ::_thesis: for x being Element of PM ex r being Real st
( r > 0 & Ball (x,r) c= the carrier of PM )
let x be Element of PM; ::_thesis: ex r being Real st
( r > 0 & Ball (x,r) c= the carrier of PM )
consider r being Real such that
A1: r = 1 ;
take r ; ::_thesis: ( r > 0 & Ball (x,r) c= the carrier of PM )
thus r > 0 by A1; ::_thesis: Ball (x,r) c= the carrier of PM
thus Ball (x,r) c= the carrier of PM ; ::_thesis: verum
end;
theorem Th27: :: PCOMPS_1:27
for PM being MetrStruct
for y, x being Element of PM
for r being real number st PM is triangle & y in Ball (x,r) holds
ex p being Real st
( p > 0 & Ball (y,p) c= Ball (x,r) )
proof
let PM be MetrStruct ; ::_thesis: for y, x being Element of PM
for r being real number st PM is triangle & y in Ball (x,r) holds
ex p being Real st
( p > 0 & Ball (y,p) c= Ball (x,r) )
let y, x be Element of PM; ::_thesis: for r being real number st PM is triangle & y in Ball (x,r) holds
ex p being Real st
( p > 0 & Ball (y,p) c= Ball (x,r) )
let r be real number ; ::_thesis: ( PM is triangle & y in Ball (x,r) implies ex p being Real st
( p > 0 & Ball (y,p) c= Ball (x,r) ) )
reconsider r9 = r as Real by XREAL_0:def_1;
assume A1: PM is triangle ; ::_thesis: ( not y in Ball (x,r) or ex p being Real st
( p > 0 & Ball (y,p) c= Ball (x,r) ) )
assume A2: y in Ball (x,r) ; ::_thesis: ex p being Real st
( p > 0 & Ball (y,p) c= Ball (x,r) )
then A3: dist (x,y) < r by METRIC_1:11;
A4: not PM is empty by A2;
thus ex p being Real st
( p > 0 & Ball (y,p) c= Ball (x,r) ) ::_thesis: verum
proof
set p = r9 - (dist (x,y));
take r9 - (dist (x,y)) ; ::_thesis: ( r9 - (dist (x,y)) > 0 & Ball (y,(r9 - (dist (x,y)))) c= Ball (x,r) )
thus r9 - (dist (x,y)) > 0 by A3, XREAL_1:50; ::_thesis: Ball (y,(r9 - (dist (x,y)))) c= Ball (x,r)
for z being Element of PM st z in Ball (y,(r9 - (dist (x,y)))) holds
z in Ball (x,r)
proof
let z be Element of PM; ::_thesis: ( z in Ball (y,(r9 - (dist (x,y)))) implies z in Ball (x,r) )
assume z in Ball (y,(r9 - (dist (x,y)))) ; ::_thesis: z in Ball (x,r)
then dist (y,z) < r9 - (dist (x,y)) by METRIC_1:11;
then A5: (dist (x,y)) + (dist (y,z)) < r by XREAL_1:20;
(dist (x,y)) + (dist (y,z)) >= dist (x,z) by A1, METRIC_1:4;
then dist (x,z) < r by A5, XXREAL_0:2;
hence z in Ball (x,r) by A4, METRIC_1:11; ::_thesis: verum
end;
hence Ball (y,(r9 - (dist (x,y)))) c= Ball (x,r) by SUBSET_1:2; ::_thesis: verum
end;
end;
theorem :: PCOMPS_1:28
for PM being MetrStruct
for r, p being Real
for y, x, z being Element of PM st PM is triangle & y in (Ball (x,r)) /\ (Ball (z,p)) holds
ex q being Real st
( Ball (y,q) c= Ball (x,r) & Ball (y,q) c= Ball (z,p) )
proof
let PM be MetrStruct ; ::_thesis: for r, p being Real
for y, x, z being Element of PM st PM is triangle & y in (Ball (x,r)) /\ (Ball (z,p)) holds
ex q being Real st
( Ball (y,q) c= Ball (x,r) & Ball (y,q) c= Ball (z,p) )
let r, p be Real; ::_thesis: for y, x, z being Element of PM st PM is triangle & y in (Ball (x,r)) /\ (Ball (z,p)) holds
ex q being Real st
( Ball (y,q) c= Ball (x,r) & Ball (y,q) c= Ball (z,p) )
let y, x, z be Element of PM; ::_thesis: ( PM is triangle & y in (Ball (x,r)) /\ (Ball (z,p)) implies ex q being Real st
( Ball (y,q) c= Ball (x,r) & Ball (y,q) c= Ball (z,p) ) )
assume A1: PM is triangle ; ::_thesis: ( not y in (Ball (x,r)) /\ (Ball (z,p)) or ex q being Real st
( Ball (y,q) c= Ball (x,r) & Ball (y,q) c= Ball (z,p) ) )
assume A2: y in (Ball (x,r)) /\ (Ball (z,p)) ; ::_thesis: ex q being Real st
( Ball (y,q) c= Ball (x,r) & Ball (y,q) c= Ball (z,p) )
then y in Ball (x,r) by XBOOLE_0:def_4;
then consider s being Real such that
s > 0 and
A3: Ball (y,s) c= Ball (x,r) by A1, Th27;
y in Ball (z,p) by A2, XBOOLE_0:def_4;
then consider t being Real such that
t > 0 and
A4: Ball (y,t) c= Ball (z,p) by A1, Th27;
take q = min (s,t); ::_thesis: ( Ball (y,q) c= Ball (x,r) & Ball (y,q) c= Ball (z,p) )
Ball (y,q) c= Ball (y,s) by Th1, XXREAL_0:17;
hence Ball (y,q) c= Ball (x,r) by A3, XBOOLE_1:1; ::_thesis: Ball (y,q) c= Ball (z,p)
Ball (y,q) c= Ball (y,t) by Th1, XXREAL_0:17;
hence Ball (y,q) c= Ball (z,p) by A4, XBOOLE_1:1; ::_thesis: verum
end;
theorem Th29: :: PCOMPS_1:29
for PM being MetrStruct
for x being Element of PM
for r being real number st PM is triangle holds
Ball (x,r) in Family_open_set PM
proof
let PM be MetrStruct ; ::_thesis: for x being Element of PM
for r being real number st PM is triangle holds
Ball (x,r) in Family_open_set PM
let x be Element of PM; ::_thesis: for r being real number st PM is triangle holds
Ball (x,r) in Family_open_set PM
let r be real number ; ::_thesis: ( PM is triangle implies Ball (x,r) in Family_open_set PM )
assume PM is triangle ; ::_thesis: Ball (x,r) in Family_open_set PM
then for y being Element of PM st y in Ball (x,r) holds
ex p being Real st
( p > 0 & Ball (y,p) c= Ball (x,r) ) by Th27;
hence Ball (x,r) in Family_open_set PM by Def4; ::_thesis: verum
end;
theorem Th30: :: PCOMPS_1:30
for PM being MetrStruct holds the carrier of PM in Family_open_set PM
proof
let PM be MetrStruct ; ::_thesis: the carrier of PM in Family_open_set PM
( the carrier of PM c= the carrier of PM & ( for y being Element of PM st y in the carrier of PM holds
ex p being Real st
( p > 0 & Ball (y,p) c= the carrier of PM ) ) ) by Th26;
hence the carrier of PM in Family_open_set PM by Def4; ::_thesis: verum
end;
theorem Th31: :: PCOMPS_1:31
for PM being MetrStruct
for V, W being Subset of PM st V in Family_open_set PM & W in Family_open_set PM holds
V /\ W in Family_open_set PM
proof
let PM be MetrStruct ; ::_thesis: for V, W being Subset of PM st V in Family_open_set PM & W in Family_open_set PM holds
V /\ W in Family_open_set PM
let V, W be Subset of PM; ::_thesis: ( V in Family_open_set PM & W in Family_open_set PM implies V /\ W in Family_open_set PM )
assume that
A1: V in Family_open_set PM and
A2: W in Family_open_set PM ; ::_thesis: V /\ W in Family_open_set PM
for z being Element of PM st z in V /\ W holds
ex q being Real st
( q > 0 & Ball (z,q) c= V /\ W )
proof
let z be Element of PM; ::_thesis: ( z in V /\ W implies ex q being Real st
( q > 0 & Ball (z,q) c= V /\ W ) )
assume A3: z in V /\ W ; ::_thesis: ex q being Real st
( q > 0 & Ball (z,q) c= V /\ W )
then z in V by XBOOLE_0:def_4;
then consider p being Real such that
A4: p > 0 and
A5: Ball (z,p) c= V by A1, Def4;
z in W by A3, XBOOLE_0:def_4;
then consider r being Real such that
A6: r > 0 and
A7: Ball (z,r) c= W by A2, Def4;
take q = min (p,r); ::_thesis: ( q > 0 & Ball (z,q) c= V /\ W )
thus q > 0 by A4, A6, XXREAL_0:15; ::_thesis: Ball (z,q) c= V /\ W
Ball (z,q) c= Ball (z,r) by Th1, XXREAL_0:17;
then A8: Ball (z,q) c= W by A7, XBOOLE_1:1;
Ball (z,q) c= Ball (z,p) by Th1, XXREAL_0:17;
then Ball (z,q) c= V by A5, XBOOLE_1:1;
hence Ball (z,q) c= V /\ W by A8, XBOOLE_1:19; ::_thesis: verum
end;
hence V /\ W in Family_open_set PM by Def4; ::_thesis: verum
end;
theorem Th32: :: PCOMPS_1:32
for PM being MetrStruct
for A being Subset-Family of PM st A c= Family_open_set PM holds
union A in Family_open_set PM
proof
let PM be MetrStruct ; ::_thesis: for A being Subset-Family of PM st A c= Family_open_set PM holds
union A in Family_open_set PM
let A be Subset-Family of PM; ::_thesis: ( A c= Family_open_set PM implies union A in Family_open_set PM )
assume A1: A c= Family_open_set PM ; ::_thesis: union A in Family_open_set PM
for x being Element of PM st x in union A holds
ex r being Real st
( r > 0 & Ball (x,r) c= union A )
proof
let x be Element of PM; ::_thesis: ( x in union A implies ex r being Real st
( r > 0 & Ball (x,r) c= union A ) )
assume x in union A ; ::_thesis: ex r being Real st
( r > 0 & Ball (x,r) c= union A )
then consider W being set such that
A2: x in W and
A3: W in A by TARSKI:def_4;
reconsider W = W as Subset of PM by A3;
consider r being Real such that
A4: r > 0 and
A5: Ball (x,r) c= W by A1, A2, A3, Def4;
take r ; ::_thesis: ( r > 0 & Ball (x,r) c= union A )
thus r > 0 by A4; ::_thesis: Ball (x,r) c= union A
W c= union A by A3, ZFMISC_1:74;
hence Ball (x,r) c= union A by A5, XBOOLE_1:1; ::_thesis: verum
end;
hence union A in Family_open_set PM by Def4; ::_thesis: verum
end;
theorem Th33: :: PCOMPS_1:33
for PM being MetrStruct holds TopStruct(# the carrier of PM,(Family_open_set PM) #) is TopSpace
proof
let PM be MetrStruct ; ::_thesis: TopStruct(# the carrier of PM,(Family_open_set PM) #) is TopSpace
set T = TopStruct(# the carrier of PM,(Family_open_set PM) #);
A1: for p, q being Subset of TopStruct(# the carrier of PM,(Family_open_set PM) #) st p in the topology of TopStruct(# the carrier of PM,(Family_open_set PM) #) & q in the topology of TopStruct(# the carrier of PM,(Family_open_set PM) #) holds
p /\ q in the topology of TopStruct(# the carrier of PM,(Family_open_set PM) #) by Th31;
( the carrier of TopStruct(# the carrier of PM,(Family_open_set PM) #) in the topology of TopStruct(# the carrier of PM,(Family_open_set PM) #) & ( for a being Subset-Family of TopStruct(# the carrier of PM,(Family_open_set PM) #) st a c= the topology of TopStruct(# the carrier of PM,(Family_open_set PM) #) holds
union a in the topology of TopStruct(# the carrier of PM,(Family_open_set PM) #) ) ) by Th30, Th32;
hence TopStruct(# the carrier of PM,(Family_open_set PM) #) is TopSpace by A1, PRE_TOPC:def_1; ::_thesis: verum
end;
definition
let PM be MetrStruct ;
func TopSpaceMetr PM -> TopStruct equals :: PCOMPS_1:def 5
TopStruct(# the carrier of PM,(Family_open_set PM) #);
coherence
TopStruct(# the carrier of PM,(Family_open_set PM) #) is TopStruct ;
end;
:: deftheorem defines TopSpaceMetr PCOMPS_1:def_5_:_
for PM being MetrStruct holds TopSpaceMetr PM = TopStruct(# the carrier of PM,(Family_open_set PM) #);
registration
let PM be MetrStruct ;
cluster TopSpaceMetr PM -> strict TopSpace-like ;
coherence
( TopSpaceMetr PM is strict & TopSpaceMetr PM is TopSpace-like ) by Th33;
end;
registration
let PM be non empty MetrStruct ;
cluster TopSpaceMetr PM -> non empty ;
coherence
not TopSpaceMetr PM is empty ;
end;
theorem Th34: :: PCOMPS_1:34
for PM being non empty MetrSpace holds TopSpaceMetr PM is T_2
proof
let PM be non empty MetrSpace; ::_thesis: TopSpaceMetr PM is T_2
set TPS = TopSpaceMetr PM;
for x, y being Element of (TopSpaceMetr PM) st not x = y holds
ex W, V being Subset of (TopSpaceMetr PM) st
( W is open & V is open & x in W & y in V & W misses V )
proof
let x, y be Element of (TopSpaceMetr PM); ::_thesis: ( not x = y implies ex W, V being Subset of (TopSpaceMetr PM) st
( W is open & V is open & x in W & y in V & W misses V ) )
assume A1: not x = y ; ::_thesis: ex W, V being Subset of (TopSpaceMetr PM) st
( W is open & V is open & x in W & y in V & W misses V )
reconsider x = x, y = y as Element of PM ;
set r = (dist (x,y)) / 2;
dist (x,y) <> 0 by A1, METRIC_1:2;
then dist (x,y) > 0 by METRIC_1:5;
then A2: (dist (x,y)) / 2 > 0 by XREAL_1:139;
ex W, V being Subset of (TopSpaceMetr PM) st
( W is open & V is open & x in W & y in V & W misses V )
proof
set V = Ball (y,((dist (x,y)) / 2));
set W = Ball (x,((dist (x,y)) / 2));
A3: ( Ball (x,((dist (x,y)) / 2)) in Family_open_set PM & Ball (y,((dist (x,y)) / 2)) in Family_open_set PM ) by Th29;
reconsider W = Ball (x,((dist (x,y)) / 2)), V = Ball (y,((dist (x,y)) / 2)) as Subset of (TopSpaceMetr PM) ;
A4: for z being set holds not z in W /\ V
proof
let z be set ; ::_thesis: not z in W /\ V
assume A5: z in W /\ V ; ::_thesis: contradiction
then reconsider z = z as Element of PM ;
z in V by A5, XBOOLE_0:def_4;
then A6: dist (y,z) < (dist (x,y)) / 2 by METRIC_1:11;
z in W by A5, XBOOLE_0:def_4;
then dist (x,z) < (dist (x,y)) / 2 by METRIC_1:11;
then (dist (x,z)) + (dist (y,z)) < ((dist (x,y)) / 2) + ((dist (x,y)) / 2) by A6, XREAL_1:8;
hence contradiction by METRIC_1:4; ::_thesis: verum
end;
take W ; ::_thesis: ex V being Subset of (TopSpaceMetr PM) st
( W is open & V is open & x in W & y in V & W misses V )
take V ; ::_thesis: ( W is open & V is open & x in W & y in V & W misses V )
( dist (x,x) = 0 & dist (y,y) = 0 ) by METRIC_1:1;
hence ( W is open & V is open & x in W & y in V & W misses V ) by A2, A3, A4, METRIC_1:11, PRE_TOPC:def_2, XBOOLE_0:4; ::_thesis: verum
end;
hence ex W, V being Subset of (TopSpaceMetr PM) st
( W is open & V is open & x in W & y in V & W misses V ) ; ::_thesis: verum
end;
hence TopSpaceMetr PM is T_2 by PRE_TOPC:def_10; ::_thesis: verum
end;
registration
cluster non empty strict TopSpace-like T_2 for TopStruct ;
existence
ex b1 being TopSpace st
( b1 is T_2 & not b1 is empty & b1 is strict )
proof
set M = the non empty MetrSpace;
take TopSpaceMetr the non empty MetrSpace ; ::_thesis: ( TopSpaceMetr the non empty MetrSpace is T_2 & not TopSpaceMetr the non empty MetrSpace is empty & TopSpaceMetr the non empty MetrSpace is strict )
thus ( TopSpaceMetr the non empty MetrSpace is T_2 & not TopSpaceMetr the non empty MetrSpace is empty & TopSpaceMetr the non empty MetrSpace is strict ) by Th34; ::_thesis: verum
end;
end;
definition
let D be set ;
let f be Function of [:D,D:],REAL;
predf is_metric_of D means :Def6: :: PCOMPS_1:def 6
for a, b, c being Element of D holds
( ( f . (a,b) = 0 implies a = b ) & ( a = b implies f . (a,b) = 0 ) & f . (a,b) = f . (b,a) & f . (a,c) <= (f . (a,b)) + (f . (b,c)) );
end;
:: deftheorem Def6 defines is_metric_of PCOMPS_1:def_6_:_
for D being set
for f being Function of [:D,D:],REAL holds
( f is_metric_of D iff for a, b, c being Element of D holds
( ( f . (a,b) = 0 implies a = b ) & ( a = b implies f . (a,b) = 0 ) & f . (a,b) = f . (b,a) & f . (a,c) <= (f . (a,b)) + (f . (b,c)) ) );
theorem Th35: :: PCOMPS_1:35
for D being set
for f being Function of [:D,D:],REAL holds
( f is_metric_of D iff MetrStruct(# D,f #) is MetrSpace )
proof
let D be set ; ::_thesis: for f being Function of [:D,D:],REAL holds
( f is_metric_of D iff MetrStruct(# D,f #) is MetrSpace )
let f be Function of [:D,D:],REAL; ::_thesis: ( f is_metric_of D iff MetrStruct(# D,f #) is MetrSpace )
set DF = MetrStruct(# D,f #);
A1: ( MetrStruct(# D,f #) is MetrSpace implies f is_metric_of D )
proof
assume MetrStruct(# D,f #) is MetrSpace ; ::_thesis: f is_metric_of D
then reconsider DF = MetrStruct(# D,f #) as MetrSpace ;
for a, b, c being Element of DF holds
( ( the distance of DF . (a,b) = 0 implies a = b ) & ( a = b implies the distance of DF . (a,b) = 0 ) & the distance of DF . (a,b) = the distance of DF . (b,a) & the distance of DF . (a,c) <= ( the distance of DF . (a,b)) + ( the distance of DF . (b,c)) )
proof
let a, b, c be Element of DF; ::_thesis: ( ( the distance of DF . (a,b) = 0 implies a = b ) & ( a = b implies the distance of DF . (a,b) = 0 ) & the distance of DF . (a,b) = the distance of DF . (b,a) & the distance of DF . (a,c) <= ( the distance of DF . (a,b)) + ( the distance of DF . (b,c)) )
A2: the distance of DF . (a,b) = dist (a,b) by METRIC_1:def_1;
hence ( the distance of DF . (a,b) = 0 iff a = b ) by METRIC_1:1, METRIC_1:2; ::_thesis: ( the distance of DF . (a,b) = the distance of DF . (b,a) & the distance of DF . (a,c) <= ( the distance of DF . (a,b)) + ( the distance of DF . (b,c)) )
the distance of DF . (b,a) = dist (b,a) by METRIC_1:def_1;
hence the distance of DF . (a,b) = the distance of DF . (b,a) by A2; ::_thesis: the distance of DF . (a,c) <= ( the distance of DF . (a,b)) + ( the distance of DF . (b,c))
( the distance of DF . (a,c) = dist (a,c) & the distance of DF . (b,c) = dist (b,c) ) by METRIC_1:def_1;
hence the distance of DF . (a,c) <= ( the distance of DF . (a,b)) + ( the distance of DF . (b,c)) by A2, METRIC_1:4; ::_thesis: verum
end;
hence f is_metric_of D by Def6; ::_thesis: verum
end;
( f is_metric_of D implies MetrStruct(# D,f #) is MetrSpace )
proof
assume A3: f is_metric_of D ; ::_thesis: MetrStruct(# D,f #) is MetrSpace
for a, b, c being Element of MetrStruct(# D,f #) holds
( ( dist (a,b) = 0 implies a = b ) & ( a = b implies dist (a,b) = 0 ) & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )
proof
let a, b, c be Element of MetrStruct(# D,f #); ::_thesis: ( ( dist (a,b) = 0 implies a = b ) & ( a = b implies dist (a,b) = 0 ) & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )
A4: the distance of MetrStruct(# D,f #) . (a,b) = dist (a,b) by METRIC_1:def_1;
hence ( dist (a,b) = 0 iff a = b ) by A3, Def6; ::_thesis: ( dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )
the distance of MetrStruct(# D,f #) . (b,a) = dist (b,a) by METRIC_1:def_1;
hence dist (a,b) = dist (b,a) by A3, A4, Def6; ::_thesis: dist (a,c) <= (dist (a,b)) + (dist (b,c))
( the distance of MetrStruct(# D,f #) . (a,c) = dist (a,c) & the distance of MetrStruct(# D,f #) . (b,c) = dist (b,c) ) by METRIC_1:def_1;
hence dist (a,c) <= (dist (a,b)) + (dist (b,c)) by A3, A4, Def6; ::_thesis: verum
end;
hence MetrStruct(# D,f #) is MetrSpace by METRIC_1:6; ::_thesis: verum
end;
hence ( f is_metric_of D iff MetrStruct(# D,f #) is MetrSpace ) by A1; ::_thesis: verum
end;
definition
let D be set ;
let f be Function of [:D,D:],REAL;
assume A1: f is_metric_of D ;
func SpaceMetr (D,f) -> strict MetrSpace equals :Def7: :: PCOMPS_1:def 7
MetrStruct(# D,f #);
coherence
MetrStruct(# D,f #) is strict MetrSpace by A1, Th35;
end;
:: deftheorem Def7 defines SpaceMetr PCOMPS_1:def_7_:_
for D being set
for f being Function of [:D,D:],REAL st f is_metric_of D holds
SpaceMetr (D,f) = MetrStruct(# D,f #);
definition
let IT be TopStruct ;
attrIT is metrizable means :: PCOMPS_1:def 8
ex f being Function of [: the carrier of IT, the carrier of IT:],REAL st
( f is_metric_of the carrier of IT & Family_open_set (SpaceMetr ( the carrier of IT,f)) = the topology of IT );
end;
:: deftheorem defines metrizable PCOMPS_1:def_8_:_
for IT being TopStruct holds
( IT is metrizable iff ex f being Function of [: the carrier of IT, the carrier of IT:],REAL st
( f is_metric_of the carrier of IT & Family_open_set (SpaceMetr ( the carrier of IT,f)) = the topology of IT ) );
registration
cluster non empty strict TopSpace-like metrizable for TopStruct ;
existence
ex b1 being non empty TopSpace st
( b1 is strict & b1 is metrizable )
proof
set MS = the non empty strict MetrSpace;
take TS = TopSpaceMetr the non empty strict MetrSpace; ::_thesis: ( TS is strict & TS is metrizable )
reconsider f = the distance of the non empty strict MetrSpace as Function of [: the carrier of TS, the carrier of TS:],REAL ;
thus TS is strict ; ::_thesis: TS is metrizable
take f ; :: according to PCOMPS_1:def_8 ::_thesis: ( f is_metric_of the carrier of TS & Family_open_set (SpaceMetr ( the carrier of TS,f)) = the topology of TS )
thus f is_metric_of the carrier of TS by Th35; ::_thesis: Family_open_set (SpaceMetr ( the carrier of TS,f)) = the topology of TS
hence Family_open_set (SpaceMetr ( the carrier of TS,f)) = the topology of TS by Def7; ::_thesis: verum
end;
end;
theorem :: PCOMPS_1:36
for D being non empty set
for f being Function of [:D,D:],REAL st f is_metric_of D holds
not SpaceMetr (D,f) is empty
proof
let D be non empty set ; ::_thesis: for f being Function of [:D,D:],REAL st f is_metric_of D holds
not SpaceMetr (D,f) is empty
let f be Function of [:D,D:],REAL; ::_thesis: ( f is_metric_of D implies not SpaceMetr (D,f) is empty )
assume f is_metric_of D ; ::_thesis: not SpaceMetr (D,f) is empty
then SpaceMetr (D,f) = MetrStruct(# D,f #) by Def7;
hence not SpaceMetr (D,f) is empty ; ::_thesis: verum
end;