:: 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;