:: NAGATA_1 semantic presentation begin Lm1: for r, s, t being Real st r >= 0 & s >= 0 & r + s < t holds ( r < t & s < t ) proof let r, s, t be Real; ::_thesis: ( r >= 0 & s >= 0 & r + s < t implies ( r < t & s < t ) ) assume that A1: ( r >= 0 & s >= 0 ) and A2: r + s < t ; ::_thesis: ( r < t & s < t ) assume ( r >= t or s >= t ) ; ::_thesis: contradiction then ( r + s >= t + 0 or s + r >= t + 0 ) by A1, XREAL_1:7; hence contradiction by A2; ::_thesis: verum end; Lm2: for r1, r2, r3, r4 being Real holds abs (r1 - r4) <= ((abs (r1 - r2)) + (abs (r2 - r3))) + (abs (r3 - r4)) proof let r1, r2, r3, r4 be Real; ::_thesis: abs (r1 - r4) <= ((abs (r1 - r2)) + (abs (r2 - r3))) + (abs (r3 - r4)) r2 - r4 = (r2 - r3) + (r3 - r4) ; then abs (r2 - r4) <= (abs (r2 - r3)) + (abs (r3 - r4)) by COMPLEX1:56; then A1: (abs (r1 - r2)) + (abs (r2 - r4)) <= (abs (r1 - r2)) + ((abs (r2 - r3)) + (abs (r3 - r4))) by XREAL_1:7; r1 - r4 = (r1 - r2) + (r2 - r4) ; then abs (r1 - r4) <= (abs (r1 - r2)) + (abs (r2 - r4)) by COMPLEX1:56; hence abs (r1 - r4) <= ((abs (r1 - r2)) + (abs (r2 - r3))) + (abs (r3 - r4)) by A1, XXREAL_0:2; ::_thesis: verum end; definition let T be TopSpace; let F be Subset-Family of T; attrF is discrete means :Def1: :: NAGATA_1:def 1 for p being Point of T ex O being open Subset of T st ( p in O & ( for A, B being Subset of T st A in F & B in F & O meets A & O meets B holds A = B ) ); end; :: deftheorem Def1 defines discrete NAGATA_1:def_1_:_ for T being TopSpace for F being Subset-Family of T holds ( F is discrete iff for p being Point of T ex O being open Subset of T st ( p in O & ( for A, B being Subset of T st A in F & B in F & O meets A & O meets B holds A = B ) ) ); registration let T be non empty TopSpace; cluster discrete for Element of bool (bool the carrier of T); existence ex b1 being Subset-Family of T st b1 is discrete proof set F = {{}, the carrier of T}; {{}, the carrier of T} c= bool the carrier of T proof let f be set ; :: according to TARSKI:def_3 ::_thesis: ( not f in {{}, the carrier of T} or f in bool the carrier of T ) assume f in {{}, the carrier of T} ; ::_thesis: f in bool the carrier of T then ( f = {} or f = the carrier of T ) by TARSKI:def_2; then f c= the carrier of T by XBOOLE_1:2; hence f in bool the carrier of T ; ::_thesis: verum end; then reconsider F = {{}, the carrier of T} as Subset-Family of T ; take F ; ::_thesis: F is discrete let p be Point of T; :: according to NAGATA_1:def_1 ::_thesis: ex O being open Subset of T st ( p in O & ( for A, B being Subset of T st A in F & B in F & O meets A & O meets B holds A = B ) ) take O = [#] T; ::_thesis: ( p in O & ( for A, B being Subset of T st A in F & B in F & O meets A & O meets B holds A = B ) ) thus p in O ; ::_thesis: for A, B being Subset of T st A in F & B in F & O meets A & O meets B holds A = B now__::_thesis:_for_A,_B_being_Subset_of_T_st_A_in_F_&_B_in_F_&_O_meets_A_&_O_meets_B_holds_ A_=_B let A, B be Subset of T; ::_thesis: ( A in F & B in F & O meets A & O meets B implies A = B ) assume that A1: A in F and A2: B in F ; ::_thesis: ( O meets A & O meets B implies A = B ) A3: ( B = {} or B = the carrier of T ) by A2, TARSKI:def_2; assume ( O meets A & O meets B ) ; ::_thesis: A = B then A4: ( O /\ A <> {} & O /\ B <> {} ) by XBOOLE_0:def_7; ( A = {} or A = the carrier of T ) by A1, TARSKI:def_2; hence A = B by A3, A4; ::_thesis: verum end; hence for A, B being Subset of T st A in F & B in F & O meets A & O meets B holds A = B ; ::_thesis: verum end; end; registration let T be non empty TopSpace; cluster empty discrete for Element of bool (bool the carrier of T); existence ex b1 being Subset-Family of T st ( b1 is empty & b1 is discrete ) proof reconsider F = {} as Subset-Family of T by XBOOLE_1:2; take F ; ::_thesis: ( F is empty & F is discrete ) thus F is empty ; ::_thesis: F is discrete let p be Point of T; :: according to NAGATA_1:def_1 ::_thesis: ex O being open Subset of T st ( p in O & ( for A, B being Subset of T st A in F & B in F & O meets A & O meets B holds A = B ) ) take [#] T ; ::_thesis: ( p in [#] T & ( for A, B being Subset of T st A in F & B in F & [#] T meets A & [#] T meets B holds A = B ) ) thus ( p in [#] T & ( for A, B being Subset of T st A in F & B in F & [#] T meets A & [#] T meets B holds A = B ) ) ; ::_thesis: verum end; end; theorem Th1: :: NAGATA_1:1 for T being non empty TopSpace for F being Subset-Family of T st ex A being Subset of T st F = {A} holds F is discrete proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st ex A being Subset of T st F = {A} holds F is discrete let F be Subset-Family of T; ::_thesis: ( ex A being Subset of T st F = {A} implies F is discrete ) assume ex A being Subset of T st F = {A} ; ::_thesis: F is discrete then consider A being Subset of T such that A1: F = {A} ; now__::_thesis:_for_p_being_Point_of_T_ex_O_being_Element_of_bool_the_carrier_of_T_st_ (_p_in_O_&_(_for_B,_C_being_Subset_of_T_st_B_in_F_&_C_in_F_&_O_meets_B_&_O_meets_C_holds_ B_=_C_)_) let p be Point of T; ::_thesis: ex O being Element of bool the carrier of T st ( p in O & ( for B, C being Subset of T st B in F & C in F & O meets B & O meets C holds B = C ) ) take O = [#] T; ::_thesis: ( p in O & ( for B, C being Subset of T st B in F & C in F & O meets B & O meets C holds B = C ) ) thus p in O ; ::_thesis: for B, C being Subset of T st B in F & C in F & O meets B & O meets C holds B = C now__::_thesis:_for_B,_C_being_Subset_of_T_st_B_in_F_&_C_in_F_holds_ B_=_C let B, C be Subset of T; ::_thesis: ( B in F & C in F implies B = C ) assume that A2: B in F and A3: C in F ; ::_thesis: B = C {B} c= {A} by A1, A2, ZFMISC_1:31; then A4: B = A by ZFMISC_1:3; {C} c= {A} by A1, A3, ZFMISC_1:31; hence B = C by A4, ZFMISC_1:3; ::_thesis: verum end; hence for B, C being Subset of T st B in F & C in F & O meets B & O meets C holds B = C ; ::_thesis: verum end; hence F is discrete by Def1; ::_thesis: verum end; theorem Th2: :: NAGATA_1:2 for T being non empty TopSpace for F, G being Subset-Family of T st F c= G & G is discrete holds F is discrete proof let T be non empty TopSpace; ::_thesis: for F, G being Subset-Family of T st F c= G & G is discrete holds F is discrete let F, G be Subset-Family of T; ::_thesis: ( F c= G & G is discrete implies F is discrete ) assume that A1: F c= G and A2: G is discrete ; ::_thesis: F is discrete now__::_thesis:_for_p_being_Point_of_T_holds_ (_ex_O_being_open_Subset_of_T_st_ (_p_in_O_&_(_for_C,_D_being_Subset_of_T_st_C_in_F_&_D_in_F_&_O_meets_C_&_O_meets_D_holds_ C_=_D_)_)_&_ex_O_being_open_Subset_of_T_st_ (_p_in_O_&_(_for_C,_D_being_Subset_of_T_st_C_in_F_&_D_in_F_&_O_meets_C_&_O_meets_D_holds_ C_=_D_)_)_) let p be Point of T; ::_thesis: ( ex O being open Subset of T st ( p in O & ( for C, D being Subset of T st C in F & D in F & O meets C & O meets D holds C = D ) ) & ex O being open Subset of T st ( p in O & ( for C, D being Subset of T st C in F & D in F & O meets C & O meets D holds C = D ) ) ) thus ex O being open Subset of T st ( p in O & ( for C, D being Subset of T st C in F & D in F & O meets C & O meets D holds C = D ) ) ::_thesis: ex O being open Subset of T st ( p in O & ( for C, D being Subset of T st C in F & D in F & O meets C & O meets D holds C = D ) ) proof consider U being open Subset of T such that A3: ( p in U & ( for C, D being Subset of T st C in G & D in G & U meets C & U meets D holds C = D ) ) by A2, Def1; take O = U; ::_thesis: ( p in O & ( for C, D being Subset of T st C in F & D in F & O meets C & O meets D holds C = D ) ) thus ( p in O & ( for C, D being Subset of T st C in F & D in F & O meets C & O meets D holds C = D ) ) by A1, A3; ::_thesis: verum end; hence ex O being open Subset of T st ( p in O & ( for C, D being Subset of T st C in F & D in F & O meets C & O meets D holds C = D ) ) ; ::_thesis: verum end; hence F is discrete by Def1; ::_thesis: verum end; theorem :: NAGATA_1:3 for T being non empty TopSpace for F, G being Subset-Family of T st F is discrete holds F /\ G is discrete by Th2, XBOOLE_1:17; theorem :: NAGATA_1:4 for T being non empty TopSpace for F, G being Subset-Family of T st F is discrete holds F \ G is discrete by Th2, XBOOLE_1:36; theorem :: NAGATA_1:5 for T being non empty TopSpace for F, G, H being Subset-Family of T st F is discrete & G is discrete & INTERSECTION (F,G) = H holds H is discrete proof let T be non empty TopSpace; ::_thesis: for F, G, H being Subset-Family of T st F is discrete & G is discrete & INTERSECTION (F,G) = H holds H is discrete let F, G, H be Subset-Family of T; ::_thesis: ( F is discrete & G is discrete & INTERSECTION (F,G) = H implies H is discrete ) assume that A1: F is discrete and A2: G is discrete and A3: INTERSECTION (F,G) = H ; ::_thesis: H is discrete now__::_thesis:_for_p_being_Point_of_T_ex_Q_being_open_Subset_of_T_st_ (_p_in_Q_&_(_for_A,_B_being_Subset_of_T_st_A_in_H_&_B_in_H_&_Q_meets_A_&_Q_meets_B_holds_ A_=_B_)_) let p be Point of T; ::_thesis: ex Q being open Subset of T st ( p in Q & ( for A, B being Subset of T st A in H & B in H & Q meets A & Q meets B holds A = B ) ) consider O being open Subset of T such that A4: p in O and A5: for A, B being Subset of T st A in F & B in F & O meets A & O meets B holds A = B by A1, Def1; consider U being open Subset of T such that A6: p in U and A7: for A, B being Subset of T st A in G & B in G & U meets A & U meets B holds A = B by A2, Def1; A8: now__::_thesis:_for_A,_B_being_Subset_of_T_st_A_in_INTERSECTION_(F,G)_&_B_in_INTERSECTION_(F,G)_&_O_/\_U_meets_A_&_O_/\_U_meets_B_holds_ A_=_B let A, B be Subset of T; ::_thesis: ( A in INTERSECTION (F,G) & B in INTERSECTION (F,G) & O /\ U meets A & O /\ U meets B implies A = B ) assume that A9: A in INTERSECTION (F,G) and A10: B in INTERSECTION (F,G) ; ::_thesis: ( O /\ U meets A & O /\ U meets B implies A = B ) consider af, ag being set such that A11: af in F and A12: ag in G and A13: A = af /\ ag by A9, SETFAM_1:def_5; assume that A14: O /\ U meets A and A15: O /\ U meets B ; ::_thesis: A = B consider bf, bg being set such that A16: bf in F and A17: bg in G and A18: B = bf /\ bg by A10, SETFAM_1:def_5; (O /\ U) /\ (bf /\ bg) <> {} by A18, A15, XBOOLE_0:def_7; then ((O /\ U) /\ bf) /\ bg <> {} by XBOOLE_1:16; then A19: ((O /\ bf) /\ U) /\ bg <> {} by XBOOLE_1:16; then O /\ bf <> {} ; then A20: O meets bf by XBOOLE_0:def_7; (O /\ U) /\ (af /\ ag) <> {} by A13, A14, XBOOLE_0:def_7; then ((O /\ U) /\ af) /\ ag <> {} by XBOOLE_1:16; then A21: ((O /\ af) /\ U) /\ ag <> {} by XBOOLE_1:16; then (O /\ af) /\ (U /\ ag) <> {} by XBOOLE_1:16; then U /\ ag <> {} ; then A22: U meets ag by XBOOLE_0:def_7; (O /\ bf) /\ (U /\ bg) <> {} by A19, XBOOLE_1:16; then U /\ bg <> {} ; then A23: U meets bg by XBOOLE_0:def_7; O /\ af <> {} by A21; then O meets af by XBOOLE_0:def_7; then af = bf by A5, A11, A16, A20; hence A = B by A7, A12, A13, A17, A18, A22, A23; ::_thesis: verum end; set Q = O /\ U; p in O /\ U by A4, A6, XBOOLE_0:def_4; hence ex Q being open Subset of T st ( p in Q & ( for A, B being Subset of T st A in H & B in H & Q meets A & Q meets B holds A = B ) ) by A3, A8; ::_thesis: verum end; hence H is discrete by Def1; ::_thesis: verum end; theorem Th6: :: NAGATA_1:6 for T being non empty TopSpace for F being Subset-Family of T for A, B being Subset of T st F is discrete & A in F & B in F & not A = B holds A misses B proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T for A, B being Subset of T st F is discrete & A in F & B in F & not A = B holds A misses B let F be Subset-Family of T; ::_thesis: for A, B being Subset of T st F is discrete & A in F & B in F & not A = B holds A misses B let A, B be Subset of T; ::_thesis: ( F is discrete & A in F & B in F & not A = B implies A misses B ) assume that A1: F is discrete and A2: ( A in F & B in F ) ; ::_thesis: ( A = B or A misses B ) assume that A3: A <> B and A4: A meets B ; ::_thesis: contradiction A /\ B <> {} T by A4, XBOOLE_0:def_7; then consider p being Point of T such that A5: p in A /\ B by PRE_TOPC:12; consider O being open Subset of T such that A6: p in O and A7: for C, D being Subset of T st C in F & D in F & O meets C & O meets D holds C = D by A1, Def1; A8: {p} c= O by A6, ZFMISC_1:31; p in B by A5, XBOOLE_0:def_4; then {p} c= B by ZFMISC_1:31; then {p} c= O /\ B by A8, XBOOLE_1:19; then A9: p in O /\ B by ZFMISC_1:31; p in A by A5, XBOOLE_0:def_4; then {p} c= A by ZFMISC_1:31; then {p} c= O /\ A by A8, XBOOLE_1:19; then A10: p in O /\ A by ZFMISC_1:31; ( O meets A & O meets B implies A = B ) by A2, A7; hence contradiction by A3, A10, A9, XBOOLE_0:4; ::_thesis: verum end; theorem Th7: :: NAGATA_1:7 for T being non empty TopSpace for F being Subset-Family of T st F is discrete holds for p being Point of T ex O being open Subset of T st ( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is discrete holds for p being Point of T ex O being open Subset of T st ( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) let F be Subset-Family of T; ::_thesis: ( F is discrete implies for p being Point of T ex O being open Subset of T st ( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) ) assume A1: F is discrete ; ::_thesis: for p being Point of T ex O being open Subset of T st ( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) let p be Point of T; ::_thesis: ex O being open Subset of T st ( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) consider O being open Subset of T such that A2: p in O and A3: for C, D being Subset of T st C in F & D in F & O meets C & O meets D holds C = D by A1, Def1; set I = INTERSECTION ({O},F); A4: for f, g being set st f in INTERSECTION ({O},F) & g in INTERSECTION ({O},F) & not f = g & not f = {} holds g = {} proof let f, g be set ; ::_thesis: ( f in INTERSECTION ({O},F) & g in INTERSECTION ({O},F) & not f = g & not f = {} implies g = {} ) assume that A5: f in INTERSECTION ({O},F) and A6: g in INTERSECTION ({O},F) ; ::_thesis: ( f = g or f = {} or g = {} ) consider o1, f1 being set such that A7: o1 in {O} and A8: f1 in F and A9: f = o1 /\ f1 by A5, SETFAM_1:def_5; consider o2, g1 being set such that A10: o2 in {O} and A11: g1 in F and A12: g = o2 /\ g1 by A6, SETFAM_1:def_5; {o2} c= {O} by A10, ZFMISC_1:31; then A13: o2 = O by ZFMISC_1:3; {o1} c= {O} by A7, ZFMISC_1:31; then A14: o1 = O by ZFMISC_1:3; then ( ( O meets f1 & O meets g1 ) or f = {} or g = {} ) by A9, A12, A13, XBOOLE_0:def_7; hence ( f = g or f = {} or g = {} ) by A3, A8, A9, A11, A12, A14, A13; ::_thesis: verum end; A15: for f being set st f <> {} & f in INTERSECTION ({O},F) holds INTERSECTION ({O},F) c= {{},f} proof let f be set ; ::_thesis: ( f <> {} & f in INTERSECTION ({O},F) implies INTERSECTION ({O},F) c= {{},f} ) assume A16: ( f <> {} & f in INTERSECTION ({O},F) ) ; ::_thesis: INTERSECTION ({O},F) c= {{},f} now__::_thesis:_for_g_being_set_st_g_in_INTERSECTION_({O},F)_holds_ g_in_{{},f} let g be set ; ::_thesis: ( g in INTERSECTION ({O},F) implies g in {{},f} ) assume g in INTERSECTION ({O},F) ; ::_thesis: g in {{},f} then ( f = g or g = {} ) by A4, A16; hence g in {{},f} by TARSKI:def_2; ::_thesis: verum end; hence INTERSECTION ({O},F) c= {{},f} by TARSKI:def_3; ::_thesis: verum end; now__::_thesis:_(INTERSECTION_({O},F))_\_{{}}_is_trivial percases ( (INTERSECTION ({O},F)) \ {{}} <> {} or (INTERSECTION ({O},F)) \ {{}} = {} ) ; suppose (INTERSECTION ({O},F)) \ {{}} <> {} ; ::_thesis: (INTERSECTION ({O},F)) \ {{}} is trivial then consider f being set such that A17: f in (INTERSECTION ({O},F)) \ {{}} by XBOOLE_0:def_1; f <> {} by A17, ZFMISC_1:56; then A18: INTERSECTION ({O},F) c= {{},f} by A15, A17; now__::_thesis:_for_g_being_set_st_g_in_INTERSECTION_({O},F)_holds_ g_in_{{}}_\/_{f} let g be set ; ::_thesis: ( g in INTERSECTION ({O},F) implies g in {{}} \/ {f} ) assume g in INTERSECTION ({O},F) ; ::_thesis: g in {{}} \/ {f} then {g} c= {{},f} by A18, ZFMISC_1:31; then ( g = {} or g = f ) by ZFMISC_1:19; then ( g in {{}} or g in {f} ) by ZFMISC_1:31; hence g in {{}} \/ {f} by XBOOLE_0:def_3; ::_thesis: verum end; then INTERSECTION ({O},F) c= {{}} \/ {f} by TARSKI:def_3; then (INTERSECTION ({O},F)) \ {{}} c= {f} by XBOOLE_1:43; then ( (INTERSECTION ({O},F)) \ {{}} = {} or (INTERSECTION ({O},F)) \ {{}} = {f} ) by ZFMISC_1:33; hence (INTERSECTION ({O},F)) \ {{}} is trivial ; ::_thesis: verum end; suppose (INTERSECTION ({O},F)) \ {{}} = {} ; ::_thesis: (INTERSECTION ({O},F)) \ {{}} is trivial hence (INTERSECTION ({O},F)) \ {{}} is trivial ; ::_thesis: verum end; end; end; hence ex O being open Subset of T st ( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) by A2; ::_thesis: verum end; theorem :: NAGATA_1:8 for T being non empty TopSpace for F being Subset-Family of T holds ( F is discrete iff ( ( for p being Point of T ex O being open Subset of T st ( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) ) & ( for A, B being Subset of T st A in F & B in F & not A = B holds A misses B ) ) ) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds ( F is discrete iff ( ( for p being Point of T ex O being open Subset of T st ( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) ) & ( for A, B being Subset of T st A in F & B in F & not A = B holds A misses B ) ) ) let F be Subset-Family of T; ::_thesis: ( F is discrete iff ( ( for p being Point of T ex O being open Subset of T st ( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) ) & ( for A, B being Subset of T st A in F & B in F & not A = B holds A misses B ) ) ) now__::_thesis:_for_F_being_Subset-Family_of_T_holds_ (_F_is_discrete_iff_(_(_for_p_being_Point_of_T_ex_O_being_open_Subset_of_T_st_ (_p_in_O_&_(INTERSECTION_({O},F))_\_{{}}_is_trivial_)_)_&_(_for_A,_B_being_Subset_of_T_st_A_in_F_&_B_in_F_&_not_A_=_B_holds_ A_misses_B_)_)_) let F be Subset-Family of T; ::_thesis: ( F is discrete iff ( ( for p being Point of T ex O being open Subset of T st ( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) ) & ( for A, B being Subset of T st A in F & B in F & not A = B holds A misses B ) ) ) ( ( for p being Point of T ex O being open Subset of T st ( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) ) & ( for A, B being Subset of T st A in F & B in F & not A = B holds A misses B ) implies F is discrete ) proof assume that A1: for p being Point of T ex O being open Subset of T st ( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) and A2: for A, B being Subset of T st A in F & B in F & not A = B holds A misses B ; ::_thesis: F is discrete assume not F is discrete ; ::_thesis: contradiction then consider p being Point of T such that A3: for O being open Subset of T holds ( not p in O or ex A, B being Subset of T st ( A in F & B in F & O meets A & O meets B & not A = B ) ) by Def1; consider O being open Subset of T such that A4: p in O and A5: (INTERSECTION ({O},F)) \ {{}} is trivial by A1; consider A, B being Subset of T such that A6: A in F and A7: B in F and A8: O meets A and A9: O meets B and A10: A <> B by A3, A4; A11: O /\ B <> {} by A9, XBOOLE_0:def_7; set I = INTERSECTION ({O},F); consider a being set such that A12: ( (INTERSECTION ({O},F)) \ {{}} = {} or (INTERSECTION ({O},F)) \ {{}} = {a} ) by A5, ZFMISC_1:131; A13: O in {O} by ZFMISC_1:31; then O /\ B in INTERSECTION ({O},F) by A7, SETFAM_1:def_5; then O /\ B in (INTERSECTION ({O},F)) \ {{}} by A11, ZFMISC_1:56; then {(O /\ B)} c= {a} by A12, ZFMISC_1:31; then A14: O /\ B = a by ZFMISC_1:3; A15: O /\ A <> {} by A8, XBOOLE_0:def_7; then consider f being set such that A16: f in O /\ A by XBOOLE_0:def_1; A17: f in A by A16, XBOOLE_0:def_4; O /\ A in INTERSECTION ({O},F) by A6, A13, SETFAM_1:def_5; then O /\ A in (INTERSECTION ({O},F)) \ {{}} by A15, ZFMISC_1:56; then {(O /\ A)} c= {a} by A12, ZFMISC_1:31; then O /\ A = a by ZFMISC_1:3; then f in B by A14, A16, XBOOLE_0:def_4; then A18: f in A /\ B by A17, XBOOLE_0:def_4; A misses B by A2, A6, A7, A10; hence contradiction by A18, XBOOLE_0:def_7; ::_thesis: verum end; hence ( F is discrete iff ( ( for p being Point of T ex O being open Subset of T st ( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) ) & ( for A, B being Subset of T st A in F & B in F & not A = B holds A misses B ) ) ) by Th6, Th7; ::_thesis: verum end; hence ( F is discrete iff ( ( for p being Point of T ex O being open Subset of T st ( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) ) & ( for A, B being Subset of T st A in F & B in F & not A = B holds A misses B ) ) ) ; ::_thesis: verum end; Lm3: for T being non empty TopSpace for O being open Subset of T for A being Subset of T st O meets Cl A holds O meets A proof let T be non empty TopSpace; ::_thesis: for O being open Subset of T for A being Subset of T st O meets Cl A holds O meets A let O be open Subset of T; ::_thesis: for A being Subset of T st O meets Cl A holds O meets A let A be Subset of T; ::_thesis: ( O meets Cl A implies O meets A ) ( O misses A implies O misses Cl A ) proof assume O misses A ; ::_thesis: O misses Cl A then A c= O ` by SUBSET_1:23; then Cl A c= O ` by TOPS_1:5; hence O misses Cl A by SUBSET_1:23; ::_thesis: verum end; hence ( O meets Cl A implies O meets A ) ; ::_thesis: verum end; registration let T be non empty TopSpace; let F be discrete Subset-Family of T; cluster clf F -> discrete ; coherence clf F is discrete proof thus clf F is discrete ::_thesis: verum proof let p be Point of T; :: according to NAGATA_1:def_1 ::_thesis: ex O being open Subset of T st ( p in O & ( for A, B being Subset of T st A in clf F & B in clf F & O meets A & O meets B holds A = B ) ) consider O being open Subset of T such that A1: p in O and A2: for A, B being Subset of T st A in F & B in F & O meets A & O meets B holds A = B by Def1; now__::_thesis:_for_A,_B_being_Subset_of_T_st_A_in_clf_F_&_B_in_clf_F_&_O_meets_A_&_O_meets_B_holds_ A_=_B let A, B be Subset of T; ::_thesis: ( A in clf F & B in clf F & O meets A & O meets B implies A = B ) assume that A3: A in clf F and A4: B in clf F ; ::_thesis: ( O meets A & O meets B implies A = B ) consider C being Subset of T such that A5: A = Cl C and A6: C in F by A3, PCOMPS_1:def_2; assume that A7: O meets A and A8: O meets B ; ::_thesis: A = B consider D being Subset of T such that A9: B = Cl D and A10: D in F by A4, PCOMPS_1:def_2; A11: O meets D by A9, A8, Lm3; O meets C by A5, A7, Lm3; hence A = B by A2, A5, A6, A9, A10, A11; ::_thesis: verum end; hence ex O being open Subset of T st ( p in O & ( for A, B being Subset of T st A in clf F & B in clf F & O meets A & O meets B holds A = B ) ) by A1; ::_thesis: verum end; end; end; Lm4: for T being non empty TopSpace for F being Subset-Family of T for A being Subset of T st A in F holds Cl A c= Cl (union F) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T for A being Subset of T st A in F holds Cl A c= Cl (union F) let F be Subset-Family of T; ::_thesis: for A being Subset of T st A in F holds Cl A c= Cl (union F) let A be Subset of T; ::_thesis: ( A in F implies Cl A c= Cl (union F) ) assume A in F ; ::_thesis: Cl A c= Cl (union F) then for f being set st f in A holds f in union F by TARSKI:def_4; then A c= union F by TARSKI:def_3; hence Cl A c= Cl (union F) by PRE_TOPC:19; ::_thesis: verum end; theorem :: NAGATA_1:9 for T being non empty TopSpace for F being Subset-Family of T st F is discrete holds for A, B being Subset of T st A in F & B in F holds Cl (A /\ B) = (Cl A) /\ (Cl B) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is discrete holds for A, B being Subset of T st A in F & B in F holds Cl (A /\ B) = (Cl A) /\ (Cl B) let F be Subset-Family of T; ::_thesis: ( F is discrete implies for A, B being Subset of T st A in F & B in F holds Cl (A /\ B) = (Cl A) /\ (Cl B) ) assume A1: F is discrete ; ::_thesis: for A, B being Subset of T st A in F & B in F holds Cl (A /\ B) = (Cl A) /\ (Cl B) let A, B be Subset of T; ::_thesis: ( A in F & B in F implies Cl (A /\ B) = (Cl A) /\ (Cl B) ) assume A2: ( A in F & B in F ) ; ::_thesis: Cl (A /\ B) = (Cl A) /\ (Cl B) now__::_thesis:_Cl_(A_/\_B)_=_(Cl_A)_/\_(Cl_B) percases ( A misses B or A = B ) by A1, A2, Th6; suppose A misses B ; ::_thesis: Cl (A /\ B) = (Cl A) /\ (Cl B) then A3: A /\ B = {} T by XBOOLE_0:def_7; (Cl A) /\ (Cl B) = {} proof assume (Cl A) /\ (Cl B) <> {} ; ::_thesis: contradiction then consider x being set such that A4: x in (Cl A) /\ (Cl B) by XBOOLE_0:def_1; consider O being open Subset of T such that A5: x in O and A6: for A, B being Subset of T st A in F & B in F & O meets A & O meets B holds A = B by A1, A4, Def1; x in Cl A by A4, XBOOLE_0:def_4; then A7: O meets A by A5, PRE_TOPC:def_7; x in Cl B by A4, XBOOLE_0:def_4; then O meets B by A5, PRE_TOPC:def_7; then A = B by A2, A6, A7; hence contradiction by A3, A7, XBOOLE_1:65; ::_thesis: verum end; hence Cl (A /\ B) = (Cl A) /\ (Cl B) by A3, PRE_TOPC:22; ::_thesis: verum end; suppose A = B ; ::_thesis: Cl (A /\ B) = (Cl A) /\ (Cl B) hence Cl (A /\ B) = (Cl A) /\ (Cl B) ; ::_thesis: verum end; end; end; hence Cl (A /\ B) = (Cl A) /\ (Cl B) ; ::_thesis: verum end; theorem :: NAGATA_1:10 for T being non empty TopSpace for F being Subset-Family of T st F is discrete holds Cl (union F) = union (clf F) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is discrete holds Cl (union F) = union (clf F) let F be Subset-Family of T; ::_thesis: ( F is discrete implies Cl (union F) = union (clf F) ) assume A1: F is discrete ; ::_thesis: Cl (union F) = union (clf F) A2: Cl (union F) c= union (clf F) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl (union F) or x in union (clf F) ) assume A3: x in Cl (union F) ; ::_thesis: x in union (clf F) then consider O being open Subset of T such that A4: x in O and A5: for A, B being Subset of T st A in F & B in F & O meets A & O meets B holds A = B by A1, Def1; not O misses union F by A3, A4, PRE_TOPC:def_7; then consider f being set such that A6: f in O and A7: f in union F by XBOOLE_0:3; consider AF being set such that A8: f in AF and A9: AF in F by A7, TARSKI:def_4; reconsider AF = AF as Subset of T by A9; A10: O meets AF by A6, A8, XBOOLE_0:3; for D being Subset of T st D is open & x in D holds not D misses AF proof assume ex D being Subset of T st ( D is open & x in D & D misses AF ) ; ::_thesis: contradiction then consider D being Subset of T such that A11: D is open and A12: x in D and A13: D misses AF ; x in D /\ O by A4, A12, XBOOLE_0:def_4; then D /\ O meets union F by A3, A11, PRE_TOPC:def_7; then consider y being set such that A14: y in D /\ O and A15: y in union F by XBOOLE_0:3; consider BF being set such that A16: y in BF and A17: BF in F by A15, TARSKI:def_4; y in D by A14, XBOOLE_0:def_4; then y in D /\ BF by A16, XBOOLE_0:def_4; then A18: D meets BF by XBOOLE_0:def_7; y in O by A14, XBOOLE_0:def_4; then y in O /\ BF by A16, XBOOLE_0:def_4; then O meets BF by XBOOLE_0:def_7; hence contradiction by A5, A9, A10, A13, A17, A18; ::_thesis: verum end; then A19: x in Cl AF by A3, PRE_TOPC:def_7; Cl AF in clf F by A9, PCOMPS_1:def_2; hence x in union (clf F) by A19, TARSKI:def_4; ::_thesis: verum end; union (clf F) c= Cl (union F) proof let f be set ; :: according to TARSKI:def_3 ::_thesis: ( not f in union (clf F) or f in Cl (union F) ) assume f in union (clf F) ; ::_thesis: f in Cl (union F) then consider Af being set such that A20: f in Af and A21: Af in clf F by TARSKI:def_4; reconsider Af = Af as Subset of T by A21; ex A being Subset of T st ( Cl A = Af & A in F ) by A21, PCOMPS_1:def_2; then Af c= Cl (union F) by Lm4; hence f in Cl (union F) by A20; ::_thesis: verum end; hence Cl (union F) = union (clf F) by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th11: :: NAGATA_1:11 for T being non empty TopSpace for F being Subset-Family of T st F is discrete holds F is locally_finite proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is discrete holds F is locally_finite let F be Subset-Family of T; ::_thesis: ( F is discrete implies F is locally_finite ) assume A1: F is discrete ; ::_thesis: F is locally_finite for p being Point of T ex A being Subset of T st ( p in A & A is open & { D where D is Subset of T : ( D in F & D meets A ) } is finite ) proof let p be Point of T; ::_thesis: ex A being Subset of T st ( p in A & A is open & { D where D is Subset of T : ( D in F & D meets A ) } is finite ) consider U being open Subset of T such that A2: p in U and A3: for A, B being Subset of T st A in F & B in F & U meets A & U meets B holds A = B by A1, Def1; set SF = { D where D is Subset of T : ( D in F & D meets U ) } ; take O = U; ::_thesis: ( p in O & O is open & { D where D is Subset of T : ( D in F & D meets O ) } is finite ) ( { D where D is Subset of T : ( D in F & D meets U ) } <> {} implies ex A being Subset of T st { D where D is Subset of T : ( D in F & D meets U ) } = {A} ) proof assume { D where D is Subset of T : ( D in F & D meets U ) } <> {} ; ::_thesis: ex A being Subset of T st { D where D is Subset of T : ( D in F & D meets U ) } = {A} then consider a being set such that A4: a in { D where D is Subset of T : ( D in F & D meets U ) } by XBOOLE_0:def_1; consider D being Subset of T such that A5: a = D and A6: ( D in F & D meets O ) by A4; now__::_thesis:_for_b_being_set_st_b_in__{__D_where_D_is_Subset_of_T_:_(_D_in_F_&_D_meets_U_)__}__holds_ b_in_{D} let b be set ; ::_thesis: ( b in { D where D is Subset of T : ( D in F & D meets U ) } implies b in {D} ) assume b in { D where D is Subset of T : ( D in F & D meets U ) } ; ::_thesis: b in {D} then ex C being Subset of T st ( b = C & C in F & C meets O ) ; then b = D by A3, A6; hence b in {D} by TARSKI:def_1; ::_thesis: verum end; then A7: { D where D is Subset of T : ( D in F & D meets U ) } c= {D} by TARSKI:def_3; {D} c= { D where D is Subset of T : ( D in F & D meets U ) } by A4, A5, ZFMISC_1:31; then { D where D is Subset of T : ( D in F & D meets U ) } = {D} by A7, XBOOLE_0:def_10; hence ex A being Subset of T st { D where D is Subset of T : ( D in F & D meets U ) } = {A} ; ::_thesis: verum end; hence ( p in O & O is open & { D where D is Subset of T : ( D in F & D meets O ) } is finite ) by A2; ::_thesis: verum end; hence F is locally_finite by PCOMPS_1:def_1; ::_thesis: verum end; definition let T be TopSpace; mode FamilySequence of T is Function of NAT,(bool (bool the carrier of T)); end; definition let T be non empty TopSpace; let Un be FamilySequence of T; let n be Element of NAT ; :: original: . redefine funcUn . n -> Subset-Family of T; coherence Un . n is Subset-Family of T proof Un . n c= bool the carrier of T ; hence Un . n is Subset-Family of T ; ::_thesis: verum end; end; definition let T be non empty TopSpace; let Un be FamilySequence of T; :: original: Union redefine func Union Un -> Subset-Family of T; coherence Union Un is Subset-Family of T proof Union Un c= bool the carrier of T ; hence Union Un is Subset-Family of T ; ::_thesis: verum end; end; definition let T be non empty TopSpace; let Un be FamilySequence of T; attrUn is sigma_discrete means :Def2: :: NAGATA_1:def 2 for n being Element of NAT holds Un . n is discrete ; end; :: deftheorem Def2 defines sigma_discrete NAGATA_1:def_2_:_ for T being non empty TopSpace for Un being FamilySequence of T holds ( Un is sigma_discrete iff for n being Element of NAT holds Un . n is discrete ); Lm5: for T being non empty TopSpace ex Un being FamilySequence of T st Un is sigma_discrete proof let T be non empty TopSpace; ::_thesis: ex Un being FamilySequence of T st Un is sigma_discrete set C = { the carrier of T}; the carrier of T in bool the carrier of T by ZFMISC_1:def_1; then { the carrier of T} c= bool the carrier of T by ZFMISC_1:31; then reconsider f = NAT --> { the carrier of T} as Function of NAT,(bool (bool the carrier of T)) by FUNCOP_1:45; take f ; ::_thesis: f is sigma_discrete now__::_thesis:_for_n_being_Element_of_NAT_holds_f_._n_is_discrete let n be Element of NAT ; ::_thesis: f . n is discrete the carrier of T is Subset of T by ZFMISC_1:def_1; hence f . n is discrete by Th1, FUNCOP_1:7; ::_thesis: verum end; hence f is sigma_discrete by Def2; ::_thesis: verum end; registration let T be non empty TopSpace; cluster Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty V14( NAT ) quasi_total sigma_discrete for Element of bool [:NAT,(bool (bool the carrier of T)):]; existence ex b1 being FamilySequence of T st b1 is sigma_discrete by Lm5; end; definition let T be non empty TopSpace; let Un be FamilySequence of T; attrUn is sigma_locally_finite means :Def3: :: NAGATA_1:def 3 for n being Element of NAT holds Un . n is locally_finite ; end; :: deftheorem Def3 defines sigma_locally_finite NAGATA_1:def_3_:_ for T being non empty TopSpace for Un being FamilySequence of T holds ( Un is sigma_locally_finite iff for n being Element of NAT holds Un . n is locally_finite ); definition let T be non empty TopSpace; let F be Subset-Family of T; attrF is sigma_discrete means :Def4: :: NAGATA_1:def 4 ex f being sigma_discrete FamilySequence of T st F = Union f; end; :: deftheorem Def4 defines sigma_discrete NAGATA_1:def_4_:_ for T being non empty TopSpace for F being Subset-Family of T holds ( F is sigma_discrete iff ex f being sigma_discrete FamilySequence of T st F = Union f ); notation let X be set ; antonym uncountable X for countable ; end; registration cluster uncountable -> non empty for set ; coherence for b1 being set st b1 is uncountable holds not b1 is empty ; end; registration let T be non empty TopSpace; cluster Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty V14( NAT ) quasi_total sigma_locally_finite for Element of bool [:NAT,(bool (bool the carrier of T)):]; existence ex b1 being FamilySequence of T st b1 is sigma_locally_finite proof thus ex Un being FamilySequence of T st Un is sigma_locally_finite ::_thesis: verum proof consider Un being FamilySequence of T such that A1: Un is sigma_discrete by Lm5; take Un ; ::_thesis: Un is sigma_locally_finite now__::_thesis:_for_n_being_Element_of_NAT_holds_Un_._n_is_locally_finite let n be Element of NAT ; ::_thesis: Un . n is locally_finite Un . n is discrete by A1, Def2; hence Un . n is locally_finite by Th11; ::_thesis: verum end; hence Un is sigma_locally_finite by Def3; ::_thesis: verum end; end; end; theorem :: NAGATA_1:12 for T being non empty TopSpace for Un being FamilySequence of T st Un is sigma_discrete holds Un is sigma_locally_finite proof let T be non empty TopSpace; ::_thesis: for Un being FamilySequence of T st Un is sigma_discrete holds Un is sigma_locally_finite let Un be FamilySequence of T; ::_thesis: ( Un is sigma_discrete implies Un is sigma_locally_finite ) assume A1: Un is sigma_discrete ; ::_thesis: Un is sigma_locally_finite let n be Element of NAT ; :: according to NAGATA_1:def_3 ::_thesis: Un . n is locally_finite Un . n is discrete by A1, Def2; hence Un . n is locally_finite by Th11; ::_thesis: verum end; theorem :: NAGATA_1:13 for A being uncountable set ex F being Subset-Family of (1TopSp [:A,A:]) st ( F is locally_finite & not F is sigma_discrete ) proof let A be uncountable set ; ::_thesis: ex F being Subset-Family of (1TopSp [:A,A:]) st ( F is locally_finite & not F is sigma_discrete ) set TS = 1TopSp [:A,A:]; set F = { ([:{a},A:] \/ [:A,{a}:]) where a is Element of A : a in A } ; { ([:{a},A:] \/ [:A,{a}:]) where a is Element of A : a in A } c= bool [:A,A:] proof let f be set ; :: according to TARSKI:def_3 ::_thesis: ( not f in { ([:{a},A:] \/ [:A,{a}:]) where a is Element of A : a in A } or f in bool [:A,A:] ) assume f in { ([:{a},A:] \/ [:A,{a}:]) where a is Element of A : a in A } ; ::_thesis: f in bool [:A,A:] then consider a being Element of A such that A1: f = [:{a},A:] \/ [:A,{a}:] and a in A ; ( [:{a},A:] c= [:A,A:] & [:A,{a}:] c= [:A,A:] ) by ZFMISC_1:96; then [:{a},A:] \/ [:A,{a}:] c= [:A,A:] by XBOOLE_1:8; hence f in bool [:A,A:] by A1; ::_thesis: verum end; then reconsider F = { ([:{a},A:] \/ [:A,{a}:]) where a is Element of A : a in A } as Subset-Family of (1TopSp [:A,A:]) ; take F ; ::_thesis: ( F is locally_finite & not F is sigma_discrete ) for z being Point of (1TopSp [:A,A:]) ex Z being Subset of (1TopSp [:A,A:]) st ( z in Z & Z is open & { O where O is Subset of (1TopSp [:A,A:]) : ( O in F & O meets Z ) } is finite ) proof let z be Point of (1TopSp [:A,A:]); ::_thesis: ex Z being Subset of (1TopSp [:A,A:]) st ( z in Z & Z is open & { O where O is Subset of (1TopSp [:A,A:]) : ( O in F & O meets Z ) } is finite ) set Z = {z}; reconsider Z = {z} as Subset of (1TopSp [:A,A:]) ; consider x, y being set such that x in A and y in A and A2: z = [x,y] by ZFMISC_1:def_2; set yAAy = {([:{y},A:] \/ [:A,{y}:])}; set xAAx = {([:{x},A:] \/ [:A,{x}:])}; set UZ = { O where O is Subset of (1TopSp [:A,A:]) : ( O in F & O meets Z ) } ; A3: { O where O is Subset of (1TopSp [:A,A:]) : ( O in F & O meets Z ) } c= {([:{x},A:] \/ [:A,{x}:])} \/ {([:{y},A:] \/ [:A,{y}:])} proof let U be set ; :: according to TARSKI:def_3 ::_thesis: ( not U in { O where O is Subset of (1TopSp [:A,A:]) : ( O in F & O meets Z ) } or U in {([:{x},A:] \/ [:A,{x}:])} \/ {([:{y},A:] \/ [:A,{y}:])} ) assume U in { O where O is Subset of (1TopSp [:A,A:]) : ( O in F & O meets Z ) } ; ::_thesis: U in {([:{x},A:] \/ [:A,{x}:])} \/ {([:{y},A:] \/ [:A,{y}:])} then consider O being Subset of (1TopSp [:A,A:]) such that A4: U = O and A5: O in F and A6: O meets Z ; consider u being set such that A7: u in O and A8: u in Z by A6, XBOOLE_0:3; consider a being Element of A such that A9: O = [:{a},A:] \/ [:A,{a}:] and a in A by A5; now__::_thesis:_O_in_{([:{x},A:]_\/_[:A,{x}:])}_\/_{([:{y},A:]_\/_[:A,{y}:])} percases ( u in [:{a},A:] or u in [:A,{a}:] ) by A9, A7, XBOOLE_0:def_3; suppose u in [:{a},A:] ; ::_thesis: O in {([:{x},A:] \/ [:A,{x}:])} \/ {([:{y},A:] \/ [:A,{y}:])} then [x,y] in [:{a},A:] by A2, A8, TARSKI:def_1; then x in {a} by ZFMISC_1:87; then x = a by TARSKI:def_1; then O in {([:{x},A:] \/ [:A,{x}:])} by A9, TARSKI:def_1; hence O in {([:{x},A:] \/ [:A,{x}:])} \/ {([:{y},A:] \/ [:A,{y}:])} by XBOOLE_0:def_3; ::_thesis: verum end; suppose u in [:A,{a}:] ; ::_thesis: O in {([:{x},A:] \/ [:A,{x}:])} \/ {([:{y},A:] \/ [:A,{y}:])} then [x,y] in [:A,{a}:] by A2, A8, TARSKI:def_1; then y in {a} by ZFMISC_1:87; then y = a by TARSKI:def_1; then O in {([:{y},A:] \/ [:A,{y}:])} by A9, TARSKI:def_1; hence O in {([:{x},A:] \/ [:A,{x}:])} \/ {([:{y},A:] \/ [:A,{y}:])} by XBOOLE_0:def_3; ::_thesis: verum end; end; end; hence U in {([:{x},A:] \/ [:A,{x}:])} \/ {([:{y},A:] \/ [:A,{y}:])} by A4; ::_thesis: verum end; ( z in Z & Z is open ) by PRE_TOPC:def_2, ZFMISC_1:31; hence ex Z being Subset of (1TopSp [:A,A:]) st ( z in Z & Z is open & { O where O is Subset of (1TopSp [:A,A:]) : ( O in F & O meets Z ) } is finite ) by A3; ::_thesis: verum end; hence F is locally_finite by PCOMPS_1:def_1; ::_thesis: not F is sigma_discrete not F is sigma_discrete proof consider a being set such that A10: a in A by XBOOLE_0:def_1; reconsider a = a as Element of A by A10; set aAAa = [:{a},A:] \/ [:A,{a}:]; A11: card A c= card F proof deffunc H1( set ) -> set = [:{$1},A:] \/ [:A,{$1}:]; consider d being Function such that A12: ( dom d = A & ( for x being set st x in A holds d . x = H1(x) ) ) from FUNCT_1:sch_3(); for a1, a2 being set st a1 in dom d & a2 in dom d & d . a1 = d . a2 holds a1 = a2 proof let a1, a2 be set ; ::_thesis: ( a1 in dom d & a2 in dom d & d . a1 = d . a2 implies a1 = a2 ) assume that A13: a1 in dom d and A14: a2 in dom d and A15: d . a1 = d . a2 ; ::_thesis: a1 = a2 a1 in {a1} by ZFMISC_1:31; then A16: [a1,a1] in [:{a1},A:] by A12, A13, ZFMISC_1:87; ( H1(a1) = d . a1 & H1(a2) = d . a2 ) by A12, A13, A14; then [a1,a1] in [:{a2},A:] \/ [:A,{a2}:] by A15, A16, XBOOLE_0:def_3; then ( [a1,a1] in [:{a2},A:] or [a1,a1] in [:A,{a2}:] ) by XBOOLE_0:def_3; then A17: a1 in {a2} by ZFMISC_1:87; assume a1 <> a2 ; ::_thesis: contradiction hence contradiction by A17, TARSKI:def_1; ::_thesis: verum end; then A18: d is one-to-one by FUNCT_1:def_4; rng d c= F proof let AA be set ; :: according to TARSKI:def_3 ::_thesis: ( not AA in rng d or AA in F ) assume AA in rng d ; ::_thesis: AA in F then consider a being set such that A19: a in dom d and A20: AA = d . a by FUNCT_1:def_3; reconsider a = a as Element of A by A12, A19; AA = [:{a},A:] \/ [:A,{a}:] by A12, A20; hence AA in F ; ::_thesis: verum end; hence card A c= card F by A12, A18, CARD_1:10; ::_thesis: verum end; assume F is sigma_discrete ; ::_thesis: contradiction then consider f being sigma_discrete FamilySequence of (1TopSp [:A,A:]) such that A21: F = Union f by Def4; defpred S1[ set , set ] means ( ( $2 in f . $1 & not f . $1 is empty ) or ( $2 = [:{a},A:] \/ [:A,{a}:] & f . $1 is empty ) ); A22: for k being set st k in NAT holds ex f being set st ( f in F & S1[k,f] ) proof let k be set ; ::_thesis: ( k in NAT implies ex f being set st ( f in F & S1[k,f] ) ) assume k in NAT ; ::_thesis: ex f being set st ( f in F & S1[k,f] ) then reconsider k = k as Element of NAT ; now__::_thesis:_ex_A_being_set_st_ (_A_in_F_&_S1[k,A]_) percases ( f . k is empty or not f . k is empty ) ; supposeA23: f . k is empty ; ::_thesis: ex A being set st ( A in F & S1[k,A] ) [:{a},A:] \/ [:A,{a}:] in F ; hence ex A being set st ( A in F & S1[k,A] ) by A23; ::_thesis: verum end; suppose not f . k is empty ; ::_thesis: ex A being set st ( A in F & S1[k,A] ) then consider A being set such that A24: A in f . k by XBOOLE_0:def_1; A in F by A21, A24, PROB_1:12; hence ex A being set st ( A in F & S1[k,A] ) by A24; ::_thesis: verum end; end; end; hence ex f being set st ( f in F & S1[k,f] ) ; ::_thesis: verum end; consider Df being Function of NAT,F such that A25: for k being set st k in NAT holds S1[k,Df . k] from FUNCT_2:sch_1(A22); A26: for n being Element of NAT for AD, BD being Element of F st S1[n,AD] & S1[n,BD] holds AD = BD proof let n be Element of NAT ; ::_thesis: for AD, BD being Element of F st S1[n,AD] & S1[n,BD] holds AD = BD let AD, BD be Element of F; ::_thesis: ( S1[n,AD] & S1[n,BD] implies AD = BD ) assume that A27: S1[n,AD] and A28: S1[n,BD] ; ::_thesis: AD = BD now__::_thesis:_AD_=_BD A29: f . n is discrete by Def2; BD in F by A21, A28, PROB_1:12; then consider b being Element of A such that A30: BD = [:{b},A:] \/ [:A,{b}:] and b in A ; AD in F by A21, A27, PROB_1:12; then consider a being Element of A such that A31: AD = [:{a},A:] \/ [:A,{a}:] and a in A ; b in {b} by TARSKI:def_1; then [a,b] in [:A,{b}:] by ZFMISC_1:87; then A32: [a,b] in BD by A30, XBOOLE_0:def_3; a in {a} by TARSKI:def_1; then [a,b] in [:{a},A:] by ZFMISC_1:87; then [a,b] in AD by A31, XBOOLE_0:def_3; then AD meets BD by A32, XBOOLE_0:3; hence AD = BD by A27, A28, A29, Th6; ::_thesis: verum end; hence AD = BD ; ::_thesis: verum end; A33: F c= Df .: NAT proof let cAAc be set ; :: according to TARSKI:def_3 ::_thesis: ( not cAAc in F or cAAc in Df .: NAT ) assume A34: cAAc in F ; ::_thesis: cAAc in Df .: NAT then consider k being Element of NAT such that A35: cAAc in f . k by A21, PROB_1:12; S1[k,Df . k] by A25; then A36: cAAc = Df . k by A26, A34, A35; dom Df = NAT by A34, FUNCT_2:def_1; hence cAAc in Df .: NAT by A36, FUNCT_1:def_6; ::_thesis: verum end; A37: not card A c= omega by CARD_3:def_14; then card NAT in card A by CARD_1:4, CARD_1:47; then card NAT c= card F by A11, CARD_1:3; then card NAT c< card F by A11, A37, CARD_1:47, XBOOLE_0:def_8; then A38: card (Df .: NAT) c< card F by CARD_1:67, XBOOLE_1:59; then card (Df .: NAT) c= card F by XBOOLE_0:def_8; then card (Df .: NAT) in card F by A38, CARD_1:3; then F \ (Df .: NAT) <> {} by CARD_1:68; hence contradiction by A33, XBOOLE_1:37; ::_thesis: verum end; hence not F is sigma_discrete ; ::_thesis: verum end; definition let T be non empty TopSpace; let Un be FamilySequence of T; attrUn is Basis_sigma_discrete means :: NAGATA_1:def 5 ( Un is sigma_discrete & Union Un is Basis of T ); end; :: deftheorem defines Basis_sigma_discrete NAGATA_1:def_5_:_ for T being non empty TopSpace for Un being FamilySequence of T holds ( Un is Basis_sigma_discrete iff ( Un is sigma_discrete & Union Un is Basis of T ) ); definition let T be non empty TopSpace; let Un be FamilySequence of T; attrUn is Basis_sigma_locally_finite means :Def6: :: NAGATA_1:def 6 ( Un is sigma_locally_finite & Union Un is Basis of T ); end; :: deftheorem Def6 defines Basis_sigma_locally_finite NAGATA_1:def_6_:_ for T being non empty TopSpace for Un being FamilySequence of T holds ( Un is Basis_sigma_locally_finite iff ( Un is sigma_locally_finite & Union Un is Basis of T ) ); theorem Th14: :: NAGATA_1:14 for r being real number for PM being non empty MetrSpace for x being Element of PM holds ([#] PM) \ (cl_Ball (x,r)) in Family_open_set PM proof let r be real number ; ::_thesis: for PM being non empty MetrSpace for x being Element of PM holds ([#] PM) \ (cl_Ball (x,r)) in Family_open_set PM reconsider r9 = r as Real by XREAL_0:def_1; let PM be non empty MetrSpace; ::_thesis: for x being Element of PM holds ([#] PM) \ (cl_Ball (x,r)) in Family_open_set PM let x be Element of PM; ::_thesis: ([#] PM) \ (cl_Ball (x,r)) in Family_open_set PM now__::_thesis:_for_y_being_Element_of_PM_st_y_in_([#]_PM)_\_(cl_Ball_(x,r))_holds_ ex_r2_being_Real_st_ (_r2_>_0_&_Ball_(y,r2)_c=_([#]_PM)_\_(cl_Ball_(x,r))_) let y be Element of PM; ::_thesis: ( y in ([#] PM) \ (cl_Ball (x,r)) implies ex r2 being Real st ( r2 > 0 & Ball (y,r2) c= ([#] PM) \ (cl_Ball (x,r)) ) ) set r1 = (dist (x,y)) - r9; A1: Ball (y,((dist (x,y)) - r9)) c= ([#] PM) \ (cl_Ball (x,r)) proof assume not Ball (y,((dist (x,y)) - r9)) c= ([#] PM) \ (cl_Ball (x,r)) ; ::_thesis: contradiction then consider z being set such that A2: z in Ball (y,((dist (x,y)) - r9)) and A3: not z in ([#] PM) \ (cl_Ball (x,r)) by TARSKI:def_3; reconsider z = z as Element of PM by A2; ( not z in [#] PM or z in cl_Ball (x,r) ) by A3, XBOOLE_0:def_5; then A4: dist (x,z) <= r9 by METRIC_1:12; dist (y,z) < (dist (x,y)) - r9 by A2, METRIC_1:11; then (dist (y,z)) + (dist (x,z)) < ((dist (x,y)) - r9) + r9 by A4, XREAL_1:8; then (dist (x,z)) + (dist (z,y)) < ((dist (x,y)) - r9) + r9 ; hence contradiction by METRIC_1:4; ::_thesis: verum end; assume y in ([#] PM) \ (cl_Ball (x,r)) ; ::_thesis: ex r2 being Real st ( r2 > 0 & Ball (y,r2) c= ([#] PM) \ (cl_Ball (x,r)) ) then not y in cl_Ball (x,r) by XBOOLE_0:def_5; then r9 + 0 < r9 + ((dist (x,y)) - r9) by METRIC_1:12; then r9 - r9 < ((dist (x,y)) - r9) - 0 by XREAL_1:21; hence ex r2 being Real st ( r2 > 0 & Ball (y,r2) c= ([#] PM) \ (cl_Ball (x,r)) ) by A1; ::_thesis: verum end; hence ([#] PM) \ (cl_Ball (x,r)) in Family_open_set PM by PCOMPS_1:def_4; ::_thesis: verum end; theorem :: NAGATA_1:15 for T being non empty TopSpace st T is metrizable holds ( T is regular & T is T_1 ) proof let T be non empty TopSpace; ::_thesis: ( T is metrizable implies ( T is regular & T is T_1 ) ) assume T is metrizable ; ::_thesis: ( T is regular & T is T_1 ) then consider metr being Function of [: the carrier of T, the carrier of T:],REAL such that A1: metr is_metric_of the carrier of T and A2: Family_open_set (SpaceMetr ( the carrier of T,metr)) = the topology of T by PCOMPS_1:def_8; set PM = SpaceMetr ( the carrier of T,metr); reconsider PM = SpaceMetr ( the carrier of T,metr) as non empty MetrSpace by A1, PCOMPS_1:36; set TPM = TopSpaceMetr PM; A3: for p being Element of T for D being Subset of T st D <> {} & D is closed & p in D ` holds ex A, B being Subset of T st ( A is open & B is open & p in A & D c= B & A misses B ) proof let p be Element of T; ::_thesis: for D being Subset of T st D <> {} & D is closed & p in D ` holds ex A, B being Subset of T st ( A is open & B is open & p in A & D c= B & A misses B ) let D be Subset of T; ::_thesis: ( D <> {} & D is closed & p in D ` implies ex A, B being Subset of T st ( A is open & B is open & p in A & D c= B & A misses B ) ) assume that D <> {} and A4: D is closed and A5: p in D ` ; ::_thesis: ex A, B being Subset of T st ( A is open & B is open & p in A & D c= B & A misses B ) A6: ([#] T) \ D in the topology of T by A4, A5, PRE_TOPC:def_2; reconsider p = p as Element of PM by A1, PCOMPS_2:4; A7: D misses D ` by XBOOLE_1:79; reconsider D = D as Subset of (TopSpaceMetr PM) by A1, PCOMPS_2:4; ([#] (TopSpaceMetr PM)) \ D in Family_open_set PM by A1, A2, A6, PCOMPS_2:4; then ([#] (TopSpaceMetr PM)) \ D is open by PRE_TOPC:def_2; then A8: D is closed by PRE_TOPC:def_3; A9: not p in D by A5, A7, XBOOLE_0:3; ex r1 being Real st ( r1 > 0 & Ball (p,r1) misses D ) proof assume A10: for r1 being Real st r1 > 0 holds Ball (p,r1) meets D ; ::_thesis: contradiction now__::_thesis:_for_A_being_Subset_of_(TopSpaceMetr_PM)_st_A_is_open_&_p_in_A_holds_ A_meets_D let A be Subset of (TopSpaceMetr PM); ::_thesis: ( A is open & p in A implies A meets D ) assume that A11: A is open and A12: p in A ; ::_thesis: A meets D A in Family_open_set PM by A11, PRE_TOPC:def_2; then consider r2 being Real such that A13: r2 > 0 and A14: Ball (p,r2) c= A by A12, PCOMPS_1:def_4; Ball (p,r2) meets D by A10, A13; then ex x being set st ( x in Ball (p,r2) & x in D ) by XBOOLE_0:3; hence A meets D by A14, XBOOLE_0:3; ::_thesis: verum end; then p in Cl D by PRE_TOPC:def_7; hence contradiction by A8, A9, PRE_TOPC:22; ::_thesis: verum end; then consider r1 being Real such that A15: r1 > 0 and A16: Ball (p,r1) misses D ; set r2 = r1 / 2; A17: r1 / 2 < (r1 / 2) + (r1 / 2) by A15, XREAL_1:29; A18: D c= ([#] PM) \ (cl_Ball (p,(r1 / 2))) proof assume not D c= ([#] PM) \ (cl_Ball (p,(r1 / 2))) ; ::_thesis: contradiction then consider x being set such that A19: x in D and A20: not x in ([#] PM) \ (cl_Ball (p,(r1 / 2))) by TARSKI:def_3; reconsider x = x as Element of PM by A19; x in cl_Ball (p,(r1 / 2)) by A20, XBOOLE_0:def_5; then dist (p,x) <= r1 / 2 by METRIC_1:12; then dist (p,x) < r1 by A17, XXREAL_0:2; then x in Ball (p,r1) by METRIC_1:11; hence contradiction by A16, A19, XBOOLE_0:3; ::_thesis: verum end; set r4 = (r1 / 2) / 2; A21: r1 / 2 > 0 by A15, XREAL_1:139; then A22: (r1 / 2) / 2 < ((r1 / 2) / 2) + ((r1 / 2) / 2) by XREAL_1:29; A23: Ball (p,((r1 / 2) / 2)) misses ([#] PM) \ (cl_Ball (p,(r1 / 2))) proof assume Ball (p,((r1 / 2) / 2)) meets ([#] PM) \ (cl_Ball (p,(r1 / 2))) ; ::_thesis: contradiction then consider x being set such that A24: x in Ball (p,((r1 / 2) / 2)) and A25: x in ([#] PM) \ (cl_Ball (p,(r1 / 2))) by XBOOLE_0:3; reconsider x = x as Element of PM by A24; not x in cl_Ball (p,(r1 / 2)) by A25, XBOOLE_0:def_5; then A26: dist (p,x) > r1 / 2 by METRIC_1:12; dist (p,x) < (r1 / 2) / 2 by A24, METRIC_1:11; hence contradiction by A22, A26, XXREAL_0:2; ::_thesis: verum end; set A = Ball (p,((r1 / 2) / 2)); set B = ([#] PM) \ (cl_Ball (p,(r1 / 2))); A27: ( ([#] PM) \ (cl_Ball (p,(r1 / 2))) in Family_open_set PM & Ball (p,((r1 / 2) / 2)) in Family_open_set PM ) by Th14, PCOMPS_1:29; then reconsider A = Ball (p,((r1 / 2) / 2)), B = ([#] PM) \ (cl_Ball (p,(r1 / 2))) as Subset of T by A2; take A ; ::_thesis: ex B being Subset of T st ( A is open & B is open & p in A & D c= B & A misses B ) take B ; ::_thesis: ( A is open & B is open & p in A & D c= B & A misses B ) (r1 / 2) / 2 > 0 by A21, XREAL_1:139; then dist (p,p) < (r1 / 2) / 2 by METRIC_1:1; hence ( A is open & B is open & p in A & D c= B & A misses B ) by A2, A18, A23, A27, METRIC_1:11, PRE_TOPC:def_2; ::_thesis: verum end; for p, q being Point of T st not p = q holds ex A, B being Subset of T st ( A is open & B is open & p in A & not q in A & q in B & not p in B ) proof let p, q be Point of T; ::_thesis: ( not p = q implies ex A, B being Subset of T st ( A is open & B is open & p in A & not q in A & q in B & not p in B ) ) assume A28: not p = q ; ::_thesis: ex A, B being Subset of T st ( A is open & B is open & p in A & not q in A & q in B & not p in B ) reconsider p = p, q = q as Element of (TopSpaceMetr PM) by A1, PCOMPS_2:4; TopSpaceMetr PM is T_2 by PCOMPS_1:34; then consider A, B being Subset of (TopSpaceMetr PM) such that A29: A is open and A30: B is open and A31: ( p in A & q in B ) and A32: A misses B by A28, PRE_TOPC:def_10; reconsider A = A, B = B as Subset of T by A1, PCOMPS_2:4; A in the topology of T by A2, A29, PRE_TOPC:def_2; then A33: A is open by PRE_TOPC:def_2; B in the topology of T by A2, A30, PRE_TOPC:def_2; then A34: B is open by PRE_TOPC:def_2; ( not q in A & not p in B ) by A31, A32, XBOOLE_0:3; hence ex A, B being Subset of T st ( A is open & B is open & p in A & not q in A & q in B & not p in B ) by A31, A33, A34; ::_thesis: verum end; hence ( T is regular & T is T_1 ) by A3, COMPTS_1:def_2, URYSOHN1:def_7; ::_thesis: verum end; theorem :: NAGATA_1:16 for T being non empty TopSpace st T is metrizable holds ex Un being FamilySequence of T st Un is Basis_sigma_locally_finite proof let T be non empty TopSpace; ::_thesis: ( T is metrizable implies ex Un being FamilySequence of T st Un is Basis_sigma_locally_finite ) assume A1: T is metrizable ; ::_thesis: ex Un being FamilySequence of T st Un is Basis_sigma_locally_finite then consider metr being Function of [: the carrier of T, the carrier of T:],REAL such that A2: metr is_metric_of the carrier of T and A3: Family_open_set (SpaceMetr ( the carrier of T,metr)) = the topology of T by PCOMPS_1:def_8; set PM = SpaceMetr ( the carrier of T,metr); reconsider PM = SpaceMetr ( the carrier of T,metr) as non empty MetrSpace by A2, PCOMPS_1:36; deffunc H1( Element of NAT ) -> set = { (Ball (x,(1 / (2 |^ $1)))) where x is Element of PM : x is Element of PM } ; defpred S1[ Element of NAT , set ] means $2 = H1($1); A4: for k being Element of NAT ex y being Subset-Family of T st S1[k,y] proof let k be Element of NAT ; ::_thesis: ex y being Subset-Family of T st S1[k,y] set Ak = H1(k); H1(k) c= bool the carrier of T proof let B be set ; :: according to TARSKI:def_3 ::_thesis: ( not B in H1(k) or B in bool the carrier of T ) assume B in H1(k) ; ::_thesis: B in bool the carrier of T then ex x being Element of PM st ( B = Ball (x,(1 / (2 |^ k))) & x is Element of PM ) ; then B in Family_open_set PM by PCOMPS_1:29; hence B in bool the carrier of T by A3; ::_thesis: verum end; hence ex y being Subset-Family of T st S1[k,y] ; ::_thesis: verum end; consider FB being Function of NAT,(bool (bool the carrier of T)) such that A5: for k being Element of NAT holds S1[k,FB . k] from FUNCT_2:sch_3(A4); defpred S2[ set , set ] means ex W being Subset-Family of T st ( W = $2 & W is open & W is Cover of T & W is_finer_than FB . $1 & W is locally_finite ); set TPM = TopSpaceMetr PM; A6: [#] T = [#] (TopSpaceMetr PM) by A2, PCOMPS_2:4; A7: for n being Element of NAT ex PP being Subset-Family of T st ( PP is_finer_than FB . n & PP is Cover of T & PP is open & PP is locally_finite ) proof let n be Element of NAT ; ::_thesis: ex PP being Subset-Family of T st ( PP is_finer_than FB . n & PP is Cover of T & PP is open & PP is locally_finite ) [#] (TopSpaceMetr PM) c= union (FB . n) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [#] (TopSpaceMetr PM) or x in union (FB . n) ) assume x in [#] (TopSpaceMetr PM) ; ::_thesis: x in union (FB . n) then reconsider x9 = x as Element of PM ; ( dist (x9,x9) = 0 & 2 |^ n > 0 ) by METRIC_1:1, NEWTON:83; then dist (x9,x9) < 1 / (2 |^ n) by XREAL_1:139; then A8: x9 in Ball (x9,(1 / (2 |^ n))) by METRIC_1:11; Ball (x9,(1 / (2 |^ n))) in H1(n) ; then Ball (x9,(1 / (2 |^ n))) in FB . n by A5; hence x in union (FB . n) by A8, TARSKI:def_4; ::_thesis: verum end; then A9: FB . n is Cover of T by A6, SETFAM_1:def_11; for U being Subset of T st U in FB . n holds U is open proof let U be Subset of T; ::_thesis: ( U in FB . n implies U is open ) assume U in FB . n ; ::_thesis: U is open then U in H1(n) by A5; then ex x being Element of PM st ( U = Ball (x,(1 / (2 |^ n))) & x is Element of PM ) ; then U in the topology of T by A3, PCOMPS_1:29; hence U is open by PRE_TOPC:def_2; ::_thesis: verum end; then FB . n is open by TOPS_2:def_1; then ex PP being Subset-Family of T st ( PP is open & PP is Cover of T & PP is_finer_than FB . n & PP is locally_finite ) by A1, A9, PCOMPS_2:6; hence ex PP being Subset-Family of T st ( PP is_finer_than FB . n & PP is Cover of T & PP is open & PP is locally_finite ) ; ::_thesis: verum end; A10: for k being set st k in NAT holds ex y being set st ( y in bool (bool the carrier of T) & S2[k,y] ) proof let k be set ; ::_thesis: ( k in NAT implies ex y being set st ( y in bool (bool the carrier of T) & S2[k,y] ) ) assume k in NAT ; ::_thesis: ex y being set st ( y in bool (bool the carrier of T) & S2[k,y] ) then reconsider k = k as Element of NAT ; ex PP being Subset-Family of T st ( PP is_finer_than FB . k & PP is Cover of T & PP is open & PP is locally_finite ) by A7; hence ex y being set st ( y in bool (bool the carrier of T) & S2[k,y] ) ; ::_thesis: verum end; consider UC being FamilySequence of T such that A11: for x being set st x in NAT holds S2[x,UC . x] from FUNCT_2:sch_1(A10); A12: for A being Subset of T st A is open holds for p being Point of T st p in A holds ex B being Subset of T st ( B in Union UC & p in B & B c= A ) proof let A be Subset of T; ::_thesis: ( A is open implies for p being Point of T st p in A holds ex B being Subset of T st ( B in Union UC & p in B & B c= A ) ) assume A is open ; ::_thesis: for p being Point of T st p in A holds ex B being Subset of T st ( B in Union UC & p in B & B c= A ) then A13: A in Family_open_set PM by A3, PRE_TOPC:def_2; let p be Point of T; ::_thesis: ( p in A implies ex B being Subset of T st ( B in Union UC & p in B & B c= A ) ) assume A14: p in A ; ::_thesis: ex B being Subset of T st ( B in Union UC & p in B & B c= A ) then reconsider p = p as Element of PM by A13; consider r1 being Real such that A15: r1 > 0 and A16: Ball (p,r1) c= A by A14, A13, PCOMPS_1:def_4; consider n being Element of NAT such that A17: 1 / (2 |^ n) <= r1 by A15, PREPOWER:92; A18: S2[n + 1,UC . (n + 1)] by A11; then union (UC . (n + 1)) = the carrier of T by SETFAM_1:45; then consider B being set such that A19: p in B and A20: B in UC . (n + 1) by TARSKI:def_4; reconsider B = B as Subset of PM by A2, A20, PCOMPS_2:4; consider B1 being set such that A21: B1 in FB . (n + 1) and A22: B c= B1 by A18, A20, SETFAM_1:def_2; B1 in H1(n + 1) by A5, A21; then consider q being Element of PM such that A23: B1 = Ball (q,(1 / (2 |^ (n + 1)))) and q is Element of PM ; A24: dist (q,p) < 1 / (2 |^ (n + 1)) by A19, A22, A23, METRIC_1:11; now__::_thesis:_for_r_being_Element_of_PM_st_r_in_B_holds_ r_in_Ball_(p,r1) let r be Element of PM; ::_thesis: ( r in B implies r in Ball (p,r1) ) assume r in B ; ::_thesis: r in Ball (p,r1) then dist (q,r) < 1 / (2 |^ (n + 1)) by A22, A23, METRIC_1:11; then ( dist (p,r) <= (dist (q,p)) + (dist (q,r)) & (dist (q,p)) + (dist (q,r)) < (1 / (2 |^ (n + 1))) + (1 / (2 |^ (n + 1))) ) by A24, METRIC_1:4, XREAL_1:8; then dist (p,r) < 2 * (1 / (2 |^ (n + 1))) by XXREAL_0:2; then dist (p,r) < (1 / ((2 |^ n) * 2)) * 2 by NEWTON:6; then dist (p,r) < 1 / (2 |^ n) by XCMPLX_1:92; then dist (p,r) < r1 by A17, XXREAL_0:2; hence r in Ball (p,r1) by METRIC_1:11; ::_thesis: verum end; then A25: B c= Ball (p,r1) by SUBSET_1:2; B in Union UC by A20, PROB_1:12; hence ex B being Subset of T st ( B in Union UC & p in B & B c= A ) by A16, A19, A25, XBOOLE_1:1; ::_thesis: verum end; for n being Element of NAT holds UC . n is locally_finite proof let n be Element of NAT ; ::_thesis: UC . n is locally_finite S2[n,UC . n] by A11; hence UC . n is locally_finite ; ::_thesis: verum end; then A26: UC is sigma_locally_finite by Def3; Union UC c= the topology of T proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in Union UC or u in the topology of T ) assume u in Union UC ; ::_thesis: u in the topology of T then consider k being Element of NAT such that A27: u in UC . k by PROB_1:12; reconsider u9 = u as Subset of T by A27; S2[k,UC . k] by A11; then u9 is open by A27, TOPS_2:def_1; hence u in the topology of T by PRE_TOPC:def_2; ::_thesis: verum end; then Union UC is Basis of T by A12, YELLOW_9:32; then UC is Basis_sigma_locally_finite by A26, Def6; hence ex Un being FamilySequence of T st Un is Basis_sigma_locally_finite ; ::_thesis: verum end; Lm6: for T being non empty TopSpace for U being open Subset of T for A being Subset of T st A is closed holds U \ A is open proof let T be non empty TopSpace; ::_thesis: for U being open Subset of T for A being Subset of T st A is closed holds U \ A is open let U be open Subset of T; ::_thesis: for A being Subset of T st A is closed holds U \ A is open let A be Subset of T; ::_thesis: ( A is closed implies U \ A is open ) A1: U /\ (([#] T) \ A) = U /\ (A `) ; assume A is closed ; ::_thesis: U \ A is open hence U \ A is open by A1, SUBSET_1:13; ::_thesis: verum end; theorem Th17: :: NAGATA_1:17 for T being non empty TopSpace for U being Function of NAT,(bool the carrier of T) st ( for n being Element of NAT holds U . n is open ) holds Union U is open proof let T be non empty TopSpace; ::_thesis: for U being Function of NAT,(bool the carrier of T) st ( for n being Element of NAT holds U . n is open ) holds Union U is open let U be Function of NAT,(bool the carrier of T); ::_thesis: ( ( for n being Element of NAT holds U . n is open ) implies Union U is open ) assume A1: for n being Element of NAT holds U . n is open ; ::_thesis: Union U is open rng U c= the topology of T proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in rng U or u in the topology of T ) assume u in rng U ; ::_thesis: u in the topology of T then consider k being set such that A2: k in dom U and A3: u = U . k by FUNCT_1:def_3; reconsider k = k as Element of NAT by A2; U . k is open by A1; hence u in the topology of T by A3, PRE_TOPC:def_2; ::_thesis: verum end; then union (rng U) in the topology of T by PRE_TOPC:def_1; then Union U in the topology of T by CARD_3:def_4; hence Union U is open by PRE_TOPC:def_2; ::_thesis: verum end; theorem Th18: :: NAGATA_1:18 for T being non empty TopSpace st ( for A being Subset of T for U being open Subset of T st A is closed & U is open & A c= U holds ex W being Function of NAT,(bool the carrier of T) st ( A c= Union W & Union W c= U & ( for n being Element of NAT holds ( Cl (W . n) c= U & W . n is open ) ) ) ) holds T is normal proof let T be non empty TopSpace; ::_thesis: ( ( for A being Subset of T for U being open Subset of T st A is closed & U is open & A c= U holds ex W being Function of NAT,(bool the carrier of T) st ( A c= Union W & Union W c= U & ( for n being Element of NAT holds ( Cl (W . n) c= U & W . n is open ) ) ) ) implies T is normal ) assume A1: for A being Subset of T for U being open Subset of T st A is closed & U is open & A c= U holds ex W being Function of NAT,(bool the carrier of T) st ( A c= Union W & Union W c= U & ( for n being Element of NAT holds ( Cl (W . n) c= U & W . n is open ) ) ) ; ::_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 UA, WB being Subset of T st ( UA is open & WB is open & A c= UA & B c= WB & UA misses WB ) proof let A, B be Subset of T; ::_thesis: ( A <> {} & B <> {} & A is closed & B is closed & A misses B implies ex UA, WB being Subset of T st ( UA is open & WB is open & A c= UA & B c= WB & UA misses WB ) ) assume that A <> {} and B <> {} and A2: ( A is closed & B is closed ) and A3: A misses B ; ::_thesis: ex UA, WB being Subset of T st ( UA is open & WB is open & A c= UA & B c= WB & UA misses WB ) set W = ([#] T) \ B; A c= B ` by A3, SUBSET_1:23; then consider Wn being Function of NAT,(bool the carrier of T) such that A4: A c= Union Wn and Union Wn c= ([#] T) \ B and A5: for n being Element of NAT holds ( Cl (Wn . n) c= ([#] T) \ B & Wn . n is open ) by A1, A2; set U = ([#] T) \ A; B c= A ` by A3, SUBSET_1:23; then consider Un being Function of NAT,(bool the carrier of T) such that A6: B c= Union Un and Union Un c= ([#] T) \ A and A7: for n being Element of NAT holds ( Cl (Un . n) c= ([#] T) \ A & Un . n is open ) by A1, A2; deffunc H1( Element of NAT ) -> Element of bool the carrier of T = (Un . $1) \ (union { (Cl (Wn . k)) where k is Element of NAT : k in (Seg $1) \/ {0} } ); defpred S1[ Element of NAT , set ] means $2 = H1($1); A8: for k being Element of NAT ex y being Subset of T st S1[k,y] ; consider FUW being Function of NAT,(bool the carrier of T) such that A9: for k being Element of NAT holds S1[k,FUW . k] from FUNCT_2:sch_3(A8); for n being Element of NAT holds FUW . n is open proof let n be Element of NAT ; ::_thesis: FUW . n is open set CLn = { (Cl (Wn . k)) where k is Element of NAT : k in (Seg n) \/ {0} } ; now__::_thesis:_for_C_being_set_st_C_in__{__(Cl_(Wn_._k))_where_k_is_Element_of_NAT_:_k_in_(Seg_n)_\/_{0}__}__holds_ C_in_bool_the_carrier_of_T let C be set ; ::_thesis: ( C in { (Cl (Wn . k)) where k is Element of NAT : k in (Seg n) \/ {0} } implies C in bool the carrier of T ) assume C in { (Cl (Wn . k)) where k is Element of NAT : k in (Seg n) \/ {0} } ; ::_thesis: C in bool the carrier of T then ex k being Element of NAT st ( C = Cl (Wn . k) & k in (Seg n) \/ {0} ) ; hence C in bool the carrier of T ; ::_thesis: verum end; then reconsider CLn = { (Cl (Wn . k)) where k is Element of NAT : k in (Seg n) \/ {0} } as Subset-Family of T by TARSKI:def_3; deffunc H2( Element of NAT ) -> Element of bool the carrier of T = Cl (Wn . $1); A10: (Seg n) \/ {0} is finite ; A11: { H2(k) where k is Element of NAT : k in (Seg n) \/ {0} } is finite from FRAENKEL:sch_21(A10); now__::_thesis:_for_A_being_Subset_of_T_st_A_in_CLn_holds_ A_is_closed let A be Subset of T; ::_thesis: ( A in CLn implies A is closed ) assume A in CLn ; ::_thesis: A is closed then ex k being Element of NAT st ( A = Cl (Wn . k) & k in (Seg n) \/ {0} ) ; hence A is closed ; ::_thesis: verum end; then A12: CLn is closed by TOPS_2:def_2; Un . n is open by A7; then (Un . n) \ (union CLn) is open by A11, A12, Lm6, TOPS_2:21; hence FUW . n is open by A9; ::_thesis: verum end; then A13: Union FUW is open by Th17; A14: for n being Element of NAT holds B misses Cl (Wn . n) proof let n be Element of NAT ; ::_thesis: B misses Cl (Wn . n) Cl (Wn . n) c= ([#] T) \ B by A5; hence B misses Cl (Wn . n) by XBOOLE_1:63, XBOOLE_1:79; ::_thesis: verum end; now__::_thesis:_for_b_being_set_st_b_in_B_holds_ b_in_Union_FUW let b be set ; ::_thesis: ( b in B implies b in Union FUW ) assume that A15: b in B and A16: not b in Union FUW ; ::_thesis: contradiction consider k being Element of NAT such that A17: b in Un . k by A6, A15, PROB_1:12; not b in union { (Cl (Wn . m)) where m is Element of NAT : m in (Seg k) \/ {0} } proof assume b in union { (Cl (Wn . m)) where m is Element of NAT : m in (Seg k) \/ {0} } ; ::_thesis: contradiction then consider CL being set such that A18: b in CL and A19: CL in { (Cl (Wn . m)) where m is Element of NAT : m in (Seg k) \/ {0} } by TARSKI:def_4; consider m being Element of NAT such that A20: CL = Cl (Wn . m) and m in (Seg k) \/ {0} by A19; B meets Cl (Wn . m) by A15, A18, A20, XBOOLE_0:3; hence contradiction by A14; ::_thesis: verum end; then b in H1(k) by A17, XBOOLE_0:def_5; then b in FUW . k by A9; hence contradiction by A16, PROB_1:12; ::_thesis: verum end; then A21: B c= Union FUW by TARSKI:def_3; deffunc H2( Element of NAT ) -> Element of bool the carrier of T = (Wn . $1) \ (union { (Cl (Un . k)) where k is Element of NAT : k in (Seg $1) \/ {0} } ); defpred S2[ Element of NAT , set ] means $2 = H2($1); A22: for k being Element of NAT ex y being Subset of T st S2[k,y] ; consider FWU being Function of NAT,(bool the carrier of T) such that A23: for k being Element of NAT holds S2[k,FWU . k] from FUNCT_2:sch_3(A22); A24: Union FUW misses Union FWU proof assume Union FUW meets Union FWU ; ::_thesis: contradiction then consider f being set such that A25: f in Union FUW and A26: f in Union FWU by XBOOLE_0:3; consider n being Element of NAT such that A27: f in FUW . n by A25, PROB_1:12; consider k being Element of NAT such that A28: f in FWU . k by A26, PROB_1:12; A29: ( n >= k implies FUW . n misses FWU . k ) proof assume that A30: n >= k and A31: FUW . n meets FWU . k ; ::_thesis: contradiction consider w being set such that A32: w in FUW . n and A33: w in FWU . k by A31, XBOOLE_0:3; w in (Wn . k) \ (union { (Cl (Un . l)) where l is Element of NAT : l in (Seg k) \/ {0} } ) by A23, A33; then A34: w in Wn . k by XBOOLE_0:def_5; ( k = 0 or k in Seg k ) by FINSEQ_1:3; then ( k in {0} or ( k in Seg k & Seg k c= Seg n ) ) by A30, FINSEQ_1:5, TARSKI:def_1; then k in (Seg n) \/ {0} by XBOOLE_0:def_3; then A35: ( Wn . k c= Cl (Wn . k) & Cl (Wn . k) in { (Cl (Wn . l)) where l is Element of NAT : l in (Seg n) \/ {0} } ) by PRE_TOPC:18; w in (Un . n) \ (union { (Cl (Wn . l)) where l is Element of NAT : l in (Seg n) \/ {0} } ) by A9, A32; then not w in union { (Cl (Wn . l)) where l is Element of NAT : l in (Seg n) \/ {0} } by XBOOLE_0:def_5; hence contradiction by A34, A35, TARSKI:def_4; ::_thesis: verum end; ( n <= k implies FUW . n misses FWU . k ) proof assume that A36: n <= k and A37: FUW . n meets FWU . k ; ::_thesis: contradiction consider u being set such that A38: u in FUW . n and A39: u in FWU . k by A37, XBOOLE_0:3; u in (Un . n) \ (union { (Cl (Wn . l)) where l is Element of NAT : l in (Seg n) \/ {0} } ) by A9, A38; then A40: u in Un . n by XBOOLE_0:def_5; ( n = 0 or n in Seg n ) by FINSEQ_1:3; then ( n in {0} or ( n in Seg n & Seg n c= Seg k ) ) by A36, FINSEQ_1:5, TARSKI:def_1; then n in (Seg k) \/ {0} by XBOOLE_0:def_3; then A41: ( Un . n c= Cl (Un . n) & Cl (Un . n) in { (Cl (Un . l)) where l is Element of NAT : l in (Seg k) \/ {0} } ) by PRE_TOPC:18; u in (Wn . k) \ (union { (Cl (Un . l)) where l is Element of NAT : l in (Seg k) \/ {0} } ) by A23, A39; then not u in union { (Cl (Un . l)) where l is Element of NAT : l in (Seg k) \/ {0} } by XBOOLE_0:def_5; hence contradiction by A40, A41, TARSKI:def_4; ::_thesis: verum end; hence contradiction by A27, A28, A29, XBOOLE_0:3; ::_thesis: verum end; for n being Element of NAT holds FWU . n is open proof let n be Element of NAT ; ::_thesis: FWU . n is open set CLn = { (Cl (Un . k)) where k is Element of NAT : k in (Seg n) \/ {0} } ; now__::_thesis:_for_C_being_set_st_C_in__{__(Cl_(Un_._k))_where_k_is_Element_of_NAT_:_k_in_(Seg_n)_\/_{0}__}__holds_ C_in_bool_the_carrier_of_T let C be set ; ::_thesis: ( C in { (Cl (Un . k)) where k is Element of NAT : k in (Seg n) \/ {0} } implies C in bool the carrier of T ) assume C in { (Cl (Un . k)) where k is Element of NAT : k in (Seg n) \/ {0} } ; ::_thesis: C in bool the carrier of T then ex k being Element of NAT st ( C = Cl (Un . k) & k in (Seg n) \/ {0} ) ; hence C in bool the carrier of T ; ::_thesis: verum end; then reconsider CLn = { (Cl (Un . k)) where k is Element of NAT : k in (Seg n) \/ {0} } as Subset-Family of T by TARSKI:def_3; deffunc H3( Element of NAT ) -> Element of bool the carrier of T = Cl (Un . $1); A42: (Seg n) \/ {0} is finite ; A43: { H3(k) where k is Element of NAT : k in (Seg n) \/ {0} } is finite from FRAENKEL:sch_21(A42); now__::_thesis:_for_A_being_Subset_of_T_st_A_in_CLn_holds_ A_is_closed let A be Subset of T; ::_thesis: ( A in CLn implies A is closed ) assume A in CLn ; ::_thesis: A is closed then ex k being Element of NAT st ( A = Cl (Un . k) & k in (Seg n) \/ {0} ) ; hence A is closed ; ::_thesis: verum end; then A44: CLn is closed by TOPS_2:def_2; Wn . n is open by A5; then (Wn . n) \ (union CLn) is open by A43, A44, Lm6, TOPS_2:21; hence FWU . n is open by A23; ::_thesis: verum end; then A45: Union FWU is open by Th17; A46: for n being Element of NAT holds A misses Cl (Un . n) proof let n be Element of NAT ; ::_thesis: A misses Cl (Un . n) Cl (Un . n) c= ([#] T) \ A by A7; hence A misses Cl (Un . n) by XBOOLE_1:63, XBOOLE_1:79; ::_thesis: verum end; now__::_thesis:_for_a_being_set_st_a_in_A_holds_ a_in_Union_FWU let a be set ; ::_thesis: ( a in A implies a in Union FWU ) assume that A47: a in A and A48: not a in Union FWU ; ::_thesis: contradiction consider k being Element of NAT such that A49: a in Wn . k by A4, A47, PROB_1:12; not a in union { (Cl (Un . m)) where m is Element of NAT : m in (Seg k) \/ {0} } proof assume a in union { (Cl (Un . m)) where m is Element of NAT : m in (Seg k) \/ {0} } ; ::_thesis: contradiction then consider CL being set such that A50: a in CL and A51: CL in { (Cl (Un . m)) where m is Element of NAT : m in (Seg k) \/ {0} } by TARSKI:def_4; consider m being Element of NAT such that A52: CL = Cl (Un . m) and m in (Seg k) \/ {0} by A51; A meets Cl (Un . m) by A47, A50, A52, XBOOLE_0:3; hence contradiction by A46; ::_thesis: verum end; then a in H2(k) by A49, XBOOLE_0:def_5; then a in FWU . k by A23; hence contradiction by A48, PROB_1:12; ::_thesis: verum end; then A c= Union FWU by TARSKI:def_3; hence ex UA, WB being Subset of T st ( UA is open & WB is open & A c= UA & B c= WB & UA misses WB ) by A21, A24, A13, A45; ::_thesis: verum end; hence T is normal by COMPTS_1:def_3; ::_thesis: verum end; theorem Th19: :: NAGATA_1:19 for T being non empty TopSpace st T is regular holds for Bn being FamilySequence of T st Union Bn is Basis of T holds for U being Subset of T for p being Point of T st U is open & p in U holds ex O being Subset of T st ( p in O & Cl O c= U & O in Union Bn ) proof let T be non empty TopSpace; ::_thesis: ( T is regular implies for Bn being FamilySequence of T st Union Bn is Basis of T holds for U being Subset of T for p being Point of T st U is open & p in U holds ex O being Subset of T st ( p in O & Cl O c= U & O in Union Bn ) ) assume A1: T is regular ; ::_thesis: for Bn being FamilySequence of T st Union Bn is Basis of T holds for U being Subset of T for p being Point of T st U is open & p in U holds ex O being Subset of T st ( p in O & Cl O c= U & O in Union Bn ) let Bn be FamilySequence of T; ::_thesis: ( Union Bn is Basis of T implies for U being Subset of T for p being Point of T st U is open & p in U holds ex O being Subset of T st ( p in O & Cl O c= U & O in Union Bn ) ) assume A2: Union Bn is Basis of T ; ::_thesis: for U being Subset of T for p being Point of T st U is open & p in U holds ex O being Subset of T st ( p in O & Cl O c= U & O in Union Bn ) for U being open Subset of T for p being Point of T st U is open & p in U holds ex O being Subset of T st ( p in O & Cl O c= U & O in Union Bn ) proof let U be open Subset of T; ::_thesis: for p being Point of T st U is open & p in U holds ex O being Subset of T st ( p in O & Cl O c= U & O in Union Bn ) let p be Point of T; ::_thesis: ( U is open & p in U implies ex O being Subset of T st ( p in O & Cl O c= U & O in Union Bn ) ) assume that U is open and A3: p in U ; ::_thesis: ex O being Subset of T st ( p in O & Cl O c= U & O in Union Bn ) now__::_thesis:_ex_O,_O_being_Subset_of_T_st_ (_p_in_O_&_Cl_O_c=_U_&_O_in_Union_Bn_) percases ( U = the carrier of T or U <> the carrier of T ) ; supposeA4: U = the carrier of T ; ::_thesis: ex O, O being Subset of T st ( p in O & Cl O c= U & O in Union Bn ) consider O being Subset of T such that A5: ( O in Union Bn & p in O ) and O c= U by A2, A3, YELLOW_9:31; take O = O; ::_thesis: ex O being Subset of T st ( p in O & Cl O c= U & O in Union Bn ) Cl O c= U by A4; hence ex O being Subset of T st ( p in O & Cl O c= U & O in Union Bn ) by A5; ::_thesis: verum end; suppose U <> the carrier of T ; ::_thesis: ex O, O being Subset of T st ( p in O & Cl O c= U & O in Union Bn ) then U c< the carrier of T by XBOOLE_0:def_8; then A6: U ` <> {} by XBOOLE_1:105; p in (U `) ` by A3; then consider W, V being Subset of T such that A7: W is open and A8: V is open and A9: p in W and A10: U ` c= V and A11: W misses V by A1, A6, COMPTS_1:def_2; consider O being Subset of T such that A12: ( O in Union Bn & p in O ) and A13: O c= W by A2, A7, A9, YELLOW_9:31; W c= V ` by A11, SUBSET_1:23; then O c= V ` by A13, XBOOLE_1:1; then Cl O c= Cl (V `) by PRE_TOPC:19; then A14: Cl O c= V ` by A8, PRE_TOPC:22; take O = O; ::_thesis: ex O being Subset of T st ( p in O & Cl O c= U & O in Union Bn ) V ` c= U by A10, SUBSET_1:17; hence ex O being Subset of T st ( p in O & Cl O c= U & O in Union Bn ) by A12, A14, XBOOLE_1:1; ::_thesis: verum end; end; end; hence ex O being Subset of T st ( p in O & Cl O c= U & O in Union Bn ) ; ::_thesis: verum end; hence for U being Subset of T for p being Point of T st U is open & p in U holds ex O being Subset of T st ( p in O & Cl O c= U & O in Union Bn ) ; ::_thesis: verum end; theorem :: NAGATA_1:20 for T being non empty TopSpace st T is regular & ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite holds T is normal proof let T be non empty TopSpace; ::_thesis: ( T is regular & ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite implies T is normal ) assume that A1: T is regular and A2: ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite ; ::_thesis: T is normal consider Bn being FamilySequence of T such that A3: Bn is Basis_sigma_locally_finite by A2; A4: Union Bn is Basis of T by A3, Def6; A5: Bn is sigma_locally_finite by A3, Def6; for A being Subset of T for U being open Subset of T st A is closed & U is open & A c= U holds ex W being Function of NAT,(bool the carrier of T) st ( A c= Union W & Union W c= U & ( for n being Element of NAT holds ( Cl (W . n) c= U & W . n is open ) ) ) proof let A be Subset of T; ::_thesis: for U being open Subset of T st A is closed & U is open & A c= U holds ex W being Function of NAT,(bool the carrier of T) st ( A c= Union W & Union W c= U & ( for n being Element of NAT holds ( Cl (W . n) c= U & W . n is open ) ) ) let U be open Subset of T; ::_thesis: ( A is closed & U is open & A c= U implies ex W being Function of NAT,(bool the carrier of T) st ( A c= Union W & Union W c= U & ( for n being Element of NAT holds ( Cl (W . n) c= U & W . n is open ) ) ) ) assume that A is closed and U is open and A6: A c= U ; ::_thesis: ex W being Function of NAT,(bool the carrier of T) st ( A c= Union W & Union W c= U & ( for n being Element of NAT holds ( Cl (W . n) c= U & W . n is open ) ) ) deffunc H1( set ) -> set = union { O where O is Subset of T : ( O in Bn . $1 & Cl O c= U ) } ; A7: for k being set st k in NAT holds H1(k) in bool the carrier of T proof let k be set ; ::_thesis: ( k in NAT implies H1(k) in bool the carrier of T ) assume k in NAT ; ::_thesis: H1(k) in bool the carrier of T then reconsider k = k as Element of NAT ; now__::_thesis:_for_bu_being_set_st_bu_in_H1(k)_holds_ bu_in_the_carrier_of_T let bu be set ; ::_thesis: ( bu in H1(k) implies bu in the carrier of T ) assume bu in H1(k) ; ::_thesis: bu in the carrier of T then consider b being set such that A8: bu in b and A9: b in { O where O is Subset of T : ( O in Bn . k & Cl O c= U ) } by TARSKI:def_4; ex O being Subset of T st ( b = O & O in Bn . k & Cl O c= U ) by A9; hence bu in the carrier of T by A8; ::_thesis: verum end; then H1(k) c= the carrier of T by TARSKI:def_3; hence H1(k) in bool the carrier of T ; ::_thesis: verum end; consider BU being Function of NAT,(bool the carrier of T) such that A10: for k being set st k in NAT holds BU . k = H1(k) from FUNCT_2:sch_2(A7); A11: now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_BU_._n_is_open_&_Cl_(BU_._n)_c=_U_) let n be Element of NAT ; ::_thesis: ( BU . n is open & Cl (BU . n) c= U ) set BUn = { O where O is Subset of T : ( O in Bn . n & Cl O c= U ) } ; { O where O is Subset of T : ( O in Bn . n & Cl O c= U ) } c= bool the carrier of T proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in { O where O is Subset of T : ( O in Bn . n & Cl O c= U ) } or b in bool the carrier of T ) assume b in { O where O is Subset of T : ( O in Bn . n & Cl O c= U ) } ; ::_thesis: b in bool the carrier of T then ex O being Subset of T st ( b = O & O in Bn . n & Cl O c= U ) ; hence b in bool the carrier of T ; ::_thesis: verum end; then reconsider BUn = { O where O is Subset of T : ( O in Bn . n & Cl O c= U ) } as Subset-Family of T ; A12: BUn c= Bn . n proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in BUn or b in Bn . n ) assume b in BUn ; ::_thesis: b in Bn . n then ex O being Subset of T st ( b = O & O in Bn . n & Cl O c= U ) ; hence b in Bn . n ; ::_thesis: verum end; Bn . n is locally_finite by A5, Def3; then A13: Cl (union BUn) = union (clf BUn) by A12, PCOMPS_1:9, PCOMPS_1:20; A14: Cl (union BUn) c= U proof let ClBu be set ; :: according to TARSKI:def_3 ::_thesis: ( not ClBu in Cl (union BUn) or ClBu in U ) assume ClBu in Cl (union BUn) ; ::_thesis: ClBu in U then consider ClB being set such that A15: ClBu in ClB and A16: ClB in clf BUn by A13, TARSKI:def_4; reconsider ClB = ClB as Subset of T by A16; consider B being Subset of T such that A17: Cl B = ClB and A18: B in BUn by A16, PCOMPS_1:def_2; ex Q being Subset of T st ( B = Q & Q in Bn . n & Cl Q c= U ) by A18; hence ClBu in U by A15, A17; ::_thesis: verum end; BUn c= the topology of T proof let B be set ; :: according to TARSKI:def_3 ::_thesis: ( not B in BUn or B in the topology of T ) assume B in BUn ; ::_thesis: B in the topology of T then consider Q being Subset of T such that A19: B = Q and A20: Q in Bn . n and Cl Q c= U ; A21: Union Bn c= the topology of T by A4, TOPS_2:64; Q in Union Bn by A20, PROB_1:12; hence B in the topology of T by A19, A21; ::_thesis: verum end; then union BUn in the topology of T by PRE_TOPC:def_1; then union BUn is open by PRE_TOPC:def_2; hence ( BU . n is open & Cl (BU . n) c= U ) by A10, A14; ::_thesis: verum end; A22: Union BU c= U proof let bu be set ; :: according to TARSKI:def_3 ::_thesis: ( not bu in Union BU or bu in U ) assume bu in Union BU ; ::_thesis: bu in U then consider k being Element of NAT such that A23: bu in BU . k by PROB_1:12; bu in union { O where O is Subset of T : ( O in Bn . k & Cl O c= U ) } by A10, A23; then consider b being set such that A24: bu in b and A25: b in { O where O is Subset of T : ( O in Bn . k & Cl O c= U ) } by TARSKI:def_4; consider O being Subset of T such that A26: b = O and O in Bn . k and A27: Cl O c= U by A25; O c= Cl O by PRE_TOPC:18; then b c= U by A26, A27, XBOOLE_1:1; hence bu in U by A24; ::_thesis: verum end; for a being set st a in A holds a in Union BU proof let a be set ; ::_thesis: ( a in A implies a in Union BU ) assume a in A ; ::_thesis: a in Union BU then consider Q being Subset of T such that A28: a in Q and A29: Cl Q c= U and A30: Q in Union Bn by A1, A4, A6, Th19; consider k being Element of NAT such that A31: Q in Bn . k by A30, PROB_1:12; Q in { O where O is Subset of T : ( O in Bn . k & Cl O c= U ) } by A29, A31; then a in H1(k) by A28, TARSKI:def_4; then a in BU . k by A10; hence a in Union BU by PROB_1:12; ::_thesis: verum end; then A c= Union BU by TARSKI:def_3; hence ex W being Function of NAT,(bool the carrier of T) st ( A c= Union W & Union W c= U & ( for n being Element of NAT holds ( Cl (W . n) c= U & W . n is open ) ) ) by A22, A11; ::_thesis: verum end; hence T is normal by Th18; ::_thesis: verum end; Lm7: for r being Real for A being Point of RealSpace st r > 0 holds A in Ball (A,r) proof let r be Real; ::_thesis: for A being Point of RealSpace st r > 0 holds A in Ball (A,r) let A be Point of RealSpace; ::_thesis: ( r > 0 implies A in Ball (A,r) ) reconsider A9 = A as Real by METRIC_1:def_13; A1: abs (A9 - A9) = 0 by ABSVALUE:2; assume r > 0 ; ::_thesis: A in Ball (A,r) then dist (A,A) < r by A1, TOPMETR:11; hence A in Ball (A,r) by METRIC_1:11; ::_thesis: verum end; definition let T be non empty TopSpace; let F, G be RealMap of T; :: original: + redefine funcF + G -> RealMap of T means :Def7: :: NAGATA_1:def 7 for t being Element of T holds it . t = (F . t) + (G . t); coherence F + G is RealMap of T proof F + G is Function of the carrier of T,REAL ; hence F + G is RealMap of T ; ::_thesis: verum end; compatibility for b1 being RealMap of T holds ( b1 = F + G iff for t being Element of T holds b1 . t = (F . t) + (G . t) ) proof let m be RealMap of T; ::_thesis: ( m = F + G iff for t being Element of T holds m . t = (F . t) + (G . t) ) thus ( m = F + G implies for p being Element of T holds m . p = (F . p) + (G . p) ) by VALUED_1:1; ::_thesis: ( ( for t being Element of T holds m . t = (F . t) + (G . t) ) implies m = F + G ) A1: dom (F + G) = (dom F) /\ (dom G) by VALUED_1:def_1 .= the carrier of T /\ (dom G) by FUNCT_2:def_1 .= the carrier of T /\ the carrier of T by FUNCT_2:def_1 ; assume A2: for p being Element of T holds m . p = (F . p) + (G . p) ; ::_thesis: m = F + G A3: now__::_thesis:_for_x_being_set_st_x_in_dom_m_holds_ m_._x_=_(F_+_G)_._x let x be set ; ::_thesis: ( x in dom m implies m . x = (F + G) . x ) assume A4: x in dom m ; ::_thesis: m . x = (F + G) . x hence m . x = (F . x) + (G . x) by A2 .= (F + G) . x by A1, A4, VALUED_1:def_1 ; ::_thesis: verum end; dom m = the carrier of T by FUNCT_2:def_1; hence m = F + G by A1, A3, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def7 defines + NAGATA_1:def_7_:_ for T being non empty TopSpace for F, G, b4 being RealMap of T holds ( b4 = F + G iff for t being Element of T holds b4 . t = (F . t) + (G . t) ); theorem :: NAGATA_1:21 for T being non empty TopSpace for f being RealMap of T st f is continuous holds for F being RealMap of [:T,T:] st ( for x, y being Element of T holds F . (x,y) = abs ((f . x) - (f . y)) ) holds F is continuous proof let T be non empty TopSpace; ::_thesis: for f being RealMap of T st f is continuous holds for F being RealMap of [:T,T:] st ( for x, y being Element of T holds F . (x,y) = abs ((f . x) - (f . y)) ) holds F is continuous let f be RealMap of T; ::_thesis: ( f is continuous implies for F being RealMap of [:T,T:] st ( for x, y being Element of T holds F . (x,y) = abs ((f . x) - (f . y)) ) holds F is continuous ) assume A1: f is continuous ; ::_thesis: for F being RealMap of [:T,T:] st ( for x, y being Element of T holds F . (x,y) = abs ((f . x) - (f . y)) ) holds F is continuous set TT = [:T,T:]; set cT = the carrier of T; reconsider f9 = f as Function of T,R^1 by TOPMETR:17; let F be RealMap of [:T,T:]; ::_thesis: ( ( for x, y being Element of T holds F . (x,y) = abs ((f . x) - (f . y)) ) implies F is continuous ) assume A2: for x, y being Element of T holds F . (x,y) = abs ((f . x) - (f . y)) ; ::_thesis: F is continuous reconsider F9 = F as Function of [:T,T:],R^1 by TOPMETR:17; A3: f9 is continuous by A1, JORDAN5A:27; now__::_thesis:_for_tt_being_Point_of_[:T,T:]_holds_F9_is_continuous_at_tt let tt be Point of [:T,T:]; ::_thesis: F9 is_continuous_at tt tt in the carrier of [:T,T:] ; then tt in [: the carrier of T, the carrier of T:] by BORSUK_1:def_2; then consider t1, t2 being set such that A4: ( t1 in the carrier of T & t2 in the carrier of T ) and A5: [t1,t2] = tt by ZFMISC_1:def_2; reconsider t1 = t1, t2 = t2 as Point of T by A4; for R being Subset of R^1 st R is open & F9 . tt in R holds ex H being Subset of [:T,T:] st ( H is open & tt in H & F9 .: H c= R ) proof reconsider ft1 = f . t1, ft2 = f . t2 as Point of RealSpace by METRIC_1:def_13; reconsider Ftt = F . tt as Point of RealSpace by METRIC_1:def_13; let R be Subset of R^1; ::_thesis: ( R is open & F9 . tt in R implies ex H being Subset of [:T,T:] st ( H is open & tt in H & F9 .: H c= R ) ) assume ( R is open & F9 . tt in R ) ; ::_thesis: ex H being Subset of [:T,T:] st ( H is open & tt in H & F9 .: H c= R ) then consider r being real number such that A6: r > 0 and A7: Ball (Ftt,r) c= R by TOPMETR:15, TOPMETR:def_6; reconsider r9 = r as Real by XREAL_0:def_1; reconsider A = Ball (ft1,(r9 / 2)), B = Ball (ft2,(r9 / 2)) as Subset of R^1 by METRIC_1:def_13, TOPMETR:17; A8: ( A is open & f9 is_continuous_at t1 ) by A3, TMAP_1:50, TOPMETR:14, TOPMETR:def_6; f . t1 in A by A6, Lm7, XREAL_1:139; then consider T1 being Subset of T such that A9: T1 is open and A10: t1 in T1 and A11: f9 .: T1 c= A by A8, TMAP_1:43; A12: ( B is open & f9 is_continuous_at t2 ) by A3, TMAP_1:50, TOPMETR:14, TOPMETR:def_6; f . t2 in B by A6, Lm7, XREAL_1:139; then consider T2 being Subset of T such that A13: T2 is open and A14: t2 in T2 and A15: f9 .: T2 c= B by A12, TMAP_1:43; F . tt = F . (t1,t2) by A5; then A16: abs ((f9 . t1) - (f9 . t2)) = F . tt by A2; A17: F .: [:T1,T2:] c= R proof let Fxy be set ; :: according to TARSKI:def_3 ::_thesis: ( not Fxy in F .: [:T1,T2:] or Fxy in R ) assume Fxy in F .: [:T1,T2:] ; ::_thesis: Fxy in R then consider xy being set such that xy in dom F and A18: xy in [:T1,T2:] and A19: Fxy = F . xy by FUNCT_1:def_6; consider x, y being set such that A20: x in T1 and A21: y in T2 and A22: xy = [x,y] by A18, ZFMISC_1:def_2; reconsider x = x, y = y as Point of T by A20, A21; reconsider fx = f . x, fy = f . y as Point of RealSpace by METRIC_1:def_13; y in the carrier of T ; then y in dom f by FUNCT_2:def_1; then f . y in f .: T2 by A21, FUNCT_1:def_6; then A23: dist (fy,ft2) < r9 / 2 by A15, METRIC_1:11; reconsider Fxy1 = F . [x,y] as Point of RealSpace by METRIC_1:def_13; A24: abs ((f . x) - (f . y)) = F . (x,y) by A2; then F . [x,y] <= ((abs ((f . x) - (f . t1))) + (F . tt)) + (abs ((f . t2) - (f . y))) by A16, Lm2; then F . [x,y] <= ((abs ((f . x) - (f . t1))) + (F . tt)) + (dist (ft2,fy)) by TOPMETR:11; then A25: (F . [x,y]) + 0 <= ((F . tt) + (dist (fx,ft1))) + (dist (ft2,fy)) by TOPMETR:11; F . tt <= ((abs ((f . t1) - (f . x))) + (F . [x,y])) + (abs ((f . y) - (f . t2))) by A16, A24, Lm2; then F . tt <= ((dist (fx,ft1)) + (F . [x,y])) + (abs ((f . y) - (f . t2))) by TOPMETR:11; then A26: F . tt <= ((F . [x,y]) + (dist (fx,ft1))) + (dist (fy,ft2)) by TOPMETR:11; x in the carrier of T ; then x in dom f by FUNCT_2:def_1; then f . x in f .: T1 by A20, FUNCT_1:def_6; then dist (fx,ft1) < r9 / 2 by A11, METRIC_1:11; then A27: (dist (fx,ft1)) + (dist (fy,ft2)) < (r9 / 2) + (r9 / 2) by A23, XREAL_1:8; then (F . [x,y]) + ((dist (fx,ft1)) + (dist (fy,ft2))) < (F . [x,y]) + r9 by XREAL_1:8; then F . tt < - ((- (F . [x,y])) - r9) by A26, XXREAL_0:2; then (- (F . tt)) - 0 > (- r9) - (F . [x,y]) by XREAL_1:26; then A28: (- (F . tt)) + (F . [x,y]) > (- r9) + 0 by XREAL_1:21; (F . tt) + ((dist (fx,ft1)) + (dist (ft2,fy))) < (F . tt) + r9 by A27, XREAL_1:8; then (F . [x,y]) + 0 < (F . tt) + r9 by A25, XXREAL_0:2; then (F . [x,y]) - (F . tt) < r9 - 0 by XREAL_1:21; then abs ((F . [x,y]) - (F . tt)) < r9 by A28, SEQ_2:1; then dist (Ftt,Fxy1) < r9 by TOPMETR:11; then Fxy1 in Ball (Ftt,r) by METRIC_1:11; hence Fxy in R by A7, A19, A22; ::_thesis: verum end; tt in [:T1,T2:] by A5, A10, A14, ZFMISC_1:def_2; hence ex H being Subset of [:T,T:] st ( H is open & tt in H & F9 .: H c= R ) by A9, A13, A17, BORSUK_1:6; ::_thesis: verum end; hence F9 is_continuous_at tt by TMAP_1:43; ::_thesis: verum end; then F9 is continuous by TMAP_1:50; hence F is continuous by JORDAN5A:27; ::_thesis: verum end; theorem Th22: :: NAGATA_1:22 for T being non empty TopSpace for F, G being RealMap of T st F is continuous & G is continuous holds F + G is continuous proof let T be non empty TopSpace; ::_thesis: for F, G being RealMap of T st F is continuous & G is continuous holds F + G is continuous let F, G be RealMap of T; ::_thesis: ( F is continuous & G is continuous implies F + G is continuous ) assume that A1: F is continuous and A2: G is continuous ; ::_thesis: F + G is continuous reconsider F9 = F, G9 = G, FG9 = F + G as Function of T,R^1 by TOPMETR:17; A3: G9 is continuous by A2, JORDAN5A:27; A4: F9 is continuous by A1, JORDAN5A:27; now__::_thesis:_for_t_being_Point_of_T_holds_FG9_is_continuous_at_t let t be Point of T; ::_thesis: FG9 is_continuous_at t for R being Subset of R^1 st R is open & FG9 . t in R holds ex H being Subset of T st ( H is open & t in H & FG9 .: H c= R ) proof reconsider Ft = F . t, Gt = G . t, FGt = (F + G) . t as Point of RealSpace by METRIC_1:def_13; let R be Subset of R^1; ::_thesis: ( R is open & FG9 . t in R implies ex H being Subset of T st ( H is open & t in H & FG9 .: H c= R ) ) assume ( R is open & FG9 . t in R ) ; ::_thesis: ex H being Subset of T st ( H is open & t in H & FG9 .: H c= R ) then consider r being real number such that A5: r > 0 and A6: Ball (FGt,r) c= R by TOPMETR:15, TOPMETR:def_6; reconsider r9 = r as Real by XREAL_0:def_1; reconsider A = Ball (Ft,(r9 / 2)), B = Ball (Gt,(r9 / 2)) as Subset of R^1 by METRIC_1:def_13, TOPMETR:17; A7: ( A is open & F9 is_continuous_at t ) by A4, TMAP_1:50, TOPMETR:14, TOPMETR:def_6; F9 . t in A by A5, Lm7, XREAL_1:139; then consider AT being Subset of T such that A8: AT is open and A9: t in AT and A10: F9 .: AT c= A by A7, TMAP_1:43; A11: ( B is open & G9 is_continuous_at t ) by A3, TMAP_1:50, TOPMETR:14, TOPMETR:def_6; G . t in B by A5, Lm7, XREAL_1:139; then consider BT being Subset of T such that A12: BT is open and A13: t in BT and A14: G9 .: BT c= B by A11, TMAP_1:43; A15: (F + G) .: (AT /\ BT) c= R proof let FGx be set ; :: according to TARSKI:def_3 ::_thesis: ( not FGx in (F + G) .: (AT /\ BT) or FGx in R ) assume FGx in (F + G) .: (AT /\ BT) ; ::_thesis: FGx in R then consider x being set such that A16: x in dom (F + G) and A17: x in AT /\ BT and A18: FGx = (F + G) . x by FUNCT_1:def_6; reconsider x = x as Point of T by A16; reconsider Fx = F . x, Gx = G . x, FGx9 = (F + G) . x as Point of RealSpace by METRIC_1:def_13; ( dom G = the carrier of T & x in BT ) by A17, FUNCT_2:def_1, XBOOLE_0:def_4; then G . x in G .: BT by FUNCT_1:def_6; then dist (Gx,Gt) < r9 / 2 by A14, METRIC_1:11; then A19: abs ((G . x) - (G . t)) < r9 / 2 by TOPMETR:11; then A20: - (r9 / 2) < (G . x) - (G . t) by SEQ_2:1; ( dom F = the carrier of T & x in AT ) by A17, FUNCT_2:def_1, XBOOLE_0:def_4; then F . x in F .: AT by FUNCT_1:def_6; then dist (Fx,Ft) < r9 / 2 by A10, METRIC_1:11; then A21: abs ((F . x) - (F . t)) < r9 / 2 by TOPMETR:11; then - (r9 / 2) < (F . x) - (F . t) by SEQ_2:1; then (- (r9 / 2)) + (- (r9 / 2)) < ((F . x) - (F . t)) + ((G . x) - (G . t)) by A20, XREAL_1:8; then A22: - r9 < ((F . x) + (G . x)) - ((F . t) + (G . t)) ; A23: (G . x) - (G . t) < r9 / 2 by A19, SEQ_2:1; (F . x) - (F . t) < r9 / 2 by A21, SEQ_2:1; then ((F . x) - (F . t)) + ((G . x) - (G . t)) < (r9 / 2) + (r9 / 2) by A23, XREAL_1:8; then abs (((F . x) + (G . x)) - ((F . t) + (G . t))) < r9 by A22, SEQ_2:1; then abs (((F + G) . x) - ((F . t) + (G . t))) < r9 by Def7; then abs (((F + G) . x) - ((F + G) . t)) < r9 by Def7; then dist (FGt,FGx9) < r9 by TOPMETR:11; then FGx9 in Ball (FGt,r) by METRIC_1:11; hence FGx in R by A6, A18; ::_thesis: verum end; t in AT /\ BT by A9, A13, XBOOLE_0:def_4; hence ex H being Subset of T st ( H is open & t in H & FG9 .: H c= R ) by A8, A12, A15; ::_thesis: verum end; hence FG9 is_continuous_at t by TMAP_1:43; ::_thesis: verum end; then FG9 is continuous by TMAP_1:50; hence F + G is continuous by JORDAN5A:27; ::_thesis: verum end; theorem Th23: :: NAGATA_1:23 for T being non empty TopSpace for ADD being BinOp of (Funcs ( the carrier of T,REAL)) st ( for f1, f2 being RealMap of T holds ADD . (f1,f2) = f1 + f2 ) holds ( ADD is having_a_unity & ADD is commutative & ADD is associative ) proof let T be non empty TopSpace; ::_thesis: for ADD being BinOp of (Funcs ( the carrier of T,REAL)) st ( for f1, f2 being RealMap of T holds ADD . (f1,f2) = f1 + f2 ) holds ( ADD is having_a_unity & ADD is commutative & ADD is associative ) set F = Funcs ( the carrier of T,REAL); let ADD be BinOp of (Funcs ( the carrier of T,REAL)); ::_thesis: ( ( for f1, f2 being RealMap of T holds ADD . (f1,f2) = f1 + f2 ) implies ( ADD is having_a_unity & ADD is commutative & ADD is associative ) ) assume A1: for f1, f2 being RealMap of T holds ADD . (f1,f2) = f1 + f2 ; ::_thesis: ( ADD is having_a_unity & ADD is commutative & ADD is associative ) ex map9 being Element of Funcs ( the carrier of T,REAL) st map9 is_a_unity_wrt ADD proof reconsider map0 = the carrier of T --> 0 as RealMap of T by FUNCOP_1:45; reconsider map09 = map0 as Element of Funcs ( the carrier of T,REAL) by FUNCT_2:8; take map09 ; ::_thesis: map09 is_a_unity_wrt ADD now__::_thesis:_for_f_being_Element_of_Funcs_(_the_carrier_of_T,REAL)_holds_ (_ADD_._(map0,f)_=_f_&_ADD_._(f,map0)_=_f_) let f be Element of Funcs ( the carrier of T,REAL); ::_thesis: ( ADD . (map0,f) = f & ADD . (f,map0) = f ) now__::_thesis:_for_x_being_Element_of_T_holds_(f_+_map09)_._x_=_f_._x let x be Element of T; ::_thesis: (f + map09) . x = f . x (f + map09) . x = (f . x) + (map09 . x) by Def7; then (f + map09) . x = (f . x) + 0 by FUNCOP_1:7; hence (f + map09) . x = f . x ; ::_thesis: verum end; then f + map09 = f by FUNCT_2:63; hence ( ADD . (map0,f) = f & ADD . (f,map0) = f ) by A1; ::_thesis: verum end; hence map09 is_a_unity_wrt ADD by BINOP_1:3; ::_thesis: verum end; hence ADD is having_a_unity by SETWISEO:def_2; ::_thesis: ( ADD is commutative & ADD is associative ) thus ADD is commutative ::_thesis: ADD is associative proof let f1, f2 be Element of Funcs ( the carrier of T,REAL); :: according to BINOP_1:def_2 ::_thesis: ADD . (f1,f2) = ADD . (f2,f1) ADD . (f1,f2) = f1 + f2 by A1; hence ADD . (f1,f2) = ADD . (f2,f1) by A1; ::_thesis: verum end; thus ADD is associative ::_thesis: verum proof let f1, f2, f3 be Element of Funcs ( the carrier of T,REAL); :: according to BINOP_1:def_3 ::_thesis: ADD . (f1,(ADD . (f2,f3))) = ADD . ((ADD . (f1,f2)),f3) reconsider ADD12 = ADD . (f1,f2), ADD23 = ADD . (f2,f3) as RealMap of T by FUNCT_2:66; A2: ADD12 + f3 = ADD . (ADD12,f3) by A1; now__::_thesis:_for_t_being_Element_of_T_holds_(f1_+_(f2_+_f3))_._t_=_((f1_+_f2)_+_f3)_._t let t be Element of T; ::_thesis: (f1 + (f2 + f3)) . t = ((f1 + f2) + f3) . t ( (f1 + (f2 + f3)) . t = (f1 . t) + ((f2 + f3) . t) & (f2 + f3) . t = (f2 . t) + (f3 . t) ) by Def7; then (f1 + (f2 + f3)) . t = ((f1 . t) + (f2 . t)) + (f3 . t) ; then (f1 + (f2 + f3)) . t = ((f1 + f2) . t) + (f3 . t) by Def7; hence (f1 + (f2 + f3)) . t = ((f1 + f2) + f3) . t by Def7; ::_thesis: verum end; then A3: f1 + (f2 + f3) = (f1 + f2) + f3 by FUNCT_2:63; f1 + (f2 + f3) = f1 + ADD23 by A1; then f1 + ADD23 = ADD12 + f3 by A1, A3; hence ADD . (f1,(ADD . (f2,f3))) = ADD . ((ADD . (f1,f2)),f3) by A1, A2; ::_thesis: verum end; end; theorem Th24: :: NAGATA_1:24 for T being non empty TopSpace for ADD being BinOp of (Funcs ( the carrier of T,REAL)) st ( for f1, f2 being RealMap of T holds ADD . (f1,f2) = f1 + f2 ) holds for map9 being Element of Funcs ( the carrier of T,REAL) st map9 is_a_unity_wrt ADD holds map9 is continuous proof let T be non empty TopSpace; ::_thesis: for ADD being BinOp of (Funcs ( the carrier of T,REAL)) st ( for f1, f2 being RealMap of T holds ADD . (f1,f2) = f1 + f2 ) holds for map9 being Element of Funcs ( the carrier of T,REAL) st map9 is_a_unity_wrt ADD holds map9 is continuous let ADD be BinOp of (Funcs ( the carrier of T,REAL)); ::_thesis: ( ( for f1, f2 being RealMap of T holds ADD . (f1,f2) = f1 + f2 ) implies for map9 being Element of Funcs ( the carrier of T,REAL) st map9 is_a_unity_wrt ADD holds map9 is continuous ) assume A1: for f1, f2 being RealMap of T holds ADD . (f1,f2) = f1 + f2 ; ::_thesis: for map9 being Element of Funcs ( the carrier of T,REAL) st map9 is_a_unity_wrt ADD holds map9 is continuous set F = Funcs ( the carrier of T,REAL); let map9 be Element of Funcs ( the carrier of T,REAL); ::_thesis: ( map9 is_a_unity_wrt ADD implies map9 is continuous ) assume A2: map9 is_a_unity_wrt ADD ; ::_thesis: map9 is continuous A3: for x being Point of T holds map9 . x = 0 proof assume ex x being Point of T st map9 . x <> 0 ; ::_thesis: contradiction then consider x being Point of T such that A4: map9 . x <> 0 ; ADD . (map9,map9) = map9 by A2, BINOP_1:3; then map9 + map9 = map9 by A1; then (map9 . x) + (map9 . x) = map9 . x by Def7; hence contradiction by A4; ::_thesis: verum end; reconsider map99 = map9 as Function of T,R^1 by TOPMETR:17; for A being Subset of T holds map99 .: (Cl A) c= Cl (map99 .: A) proof let A be Subset of T; ::_thesis: map99 .: (Cl A) c= Cl (map99 .: A) let mCla be set ; :: according to TARSKI:def_3 ::_thesis: ( not mCla in map99 .: (Cl A) or mCla in Cl (map99 .: A) ) assume mCla in map99 .: (Cl A) ; ::_thesis: mCla in Cl (map99 .: A) then A5: ex Cla being set st ( Cla in dom map9 & Cla in Cl A & mCla = map99 . Cla ) by FUNCT_1:def_6; then A <> {} T by PRE_TOPC:22; then consider a being set such that A6: a in A by XBOOLE_0:def_1; reconsider a = a as Element of T by A6; ( dom map9 = the carrier of T & map9 . a = 0 ) by A3, FUNCT_2:def_1; then 0 in map9 .: A by A6, FUNCT_1:def_6; then A7: mCla in map9 .: A by A3, A5; map99 .: A c= Cl (map99 .: A) by PRE_TOPC:18; hence mCla in Cl (map99 .: A) by A7; ::_thesis: verum end; then map99 is continuous by TOPS_2:45; hence map9 is continuous by JORDAN5A:27; ::_thesis: verum end; definition let A, B be non empty set ; let F be Function of A,(Funcs (A,B)); funcF Toler -> Function of A,B means :Def8: :: NAGATA_1:def 8 for p being Element of A holds it . p = (F . p) . p; existence ex b1 being Function of A,B st for p being Element of A holds b1 . p = (F . p) . p proof deffunc H1( Element of A) -> set = (F . $1) . $1; defpred S1[ Element of A, set ] means $2 = H1($1); A1: for x being Element of A ex y being Element of B st S1[x,y] proof let x be Element of A; ::_thesis: ex y being Element of B st S1[x,y] reconsider Funx = F . x as Function of A,B by FUNCT_2:66; Funx . x in B ; hence ex y being Element of B st S1[x,y] ; ::_thesis: verum end; consider F being Function of A,B such that A2: for x being Element of A holds S1[x,F . x] from FUNCT_2:sch_3(A1); take F ; ::_thesis: for p being Element of A holds F . p = (F . p) . p thus for p being Element of A holds F . p = (F . p) . p by A2; ::_thesis: verum end; uniqueness for b1, b2 being Function of A,B st ( for p being Element of A holds b1 . p = (F . p) . p ) & ( for p being Element of A holds b2 . p = (F . p) . p ) holds b1 = b2 proof now__::_thesis:_for_IT1,_IT2_being_Function_of_A,B_st_(_for_x_being_Element_of_A_holds_ (_IT1_._x_=_(F_._x)_._x_&_(_for_x_being_Element_of_A_holds_IT2_._x_=_(F_._x)_._x_)_)_)_holds_ IT1_=_IT2 let IT1, IT2 be Function of A,B; ::_thesis: ( ( for x being Element of A holds ( IT1 . x = (F . x) . x & ( for x being Element of A holds IT2 . x = (F . x) . x ) ) ) implies IT1 = IT2 ) assume A3: for x being Element of A holds ( IT1 . x = (F . x) . x & ( for x being Element of A holds IT2 . x = (F . x) . x ) ) ; ::_thesis: IT1 = IT2 now__::_thesis:_for_x_being_Element_of_A_holds_IT1_._x_=_IT2_._x let x be Element of A; ::_thesis: IT1 . x = IT2 . x IT1 . x = (F . x) . x by A3; hence IT1 . x = IT2 . x by A3; ::_thesis: verum end; hence IT1 = IT2 by FUNCT_2:63; ::_thesis: verum end; hence for b1, b2 being Function of A,B st ( for p being Element of A holds b1 . p = (F . p) . p ) & ( for p being Element of A holds b2 . p = (F . p) . p ) holds b1 = b2 ; ::_thesis: verum end; end; :: deftheorem Def8 defines Toler NAGATA_1:def_8_:_ for A, B being non empty set for F being Function of A,(Funcs (A,B)) for b4 being Function of A,B holds ( b4 = F Toler iff for p being Element of A holds b4 . p = (F . p) . p ); theorem :: NAGATA_1:25 for T being non empty TopSpace for ADD being BinOp of (Funcs ( the carrier of T,REAL)) st ( for f1, f2 being RealMap of T holds ADD . (f1,f2) = f1 + f2 ) holds for F being FinSequence of Funcs ( the carrier of T,REAL) st ( for n being Element of NAT st 0 <> n & n <= len F holds F . n is continuous RealMap of T ) holds ADD "**" F is continuous RealMap of T proof let T be non empty TopSpace; ::_thesis: for ADD being BinOp of (Funcs ( the carrier of T,REAL)) st ( for f1, f2 being RealMap of T holds ADD . (f1,f2) = f1 + f2 ) holds for F being FinSequence of Funcs ( the carrier of T,REAL) st ( for n being Element of NAT st 0 <> n & n <= len F holds F . n is continuous RealMap of T ) holds ADD "**" F is continuous RealMap of T let ADD be BinOp of (Funcs ( the carrier of T,REAL)); ::_thesis: ( ( for f1, f2 being RealMap of T holds ADD . (f1,f2) = f1 + f2 ) implies for F being FinSequence of Funcs ( the carrier of T,REAL) st ( for n being Element of NAT st 0 <> n & n <= len F holds F . n is continuous RealMap of T ) holds ADD "**" F is continuous RealMap of T ) assume A1: for f1, f2 being RealMap of T holds ADD . (f1,f2) = f1 + f2 ; ::_thesis: for F being FinSequence of Funcs ( the carrier of T,REAL) st ( for n being Element of NAT st 0 <> n & n <= len F holds F . n is continuous RealMap of T ) holds ADD "**" F is continuous RealMap of T set Fu = Funcs ( the carrier of T,REAL); let F be FinSequence of Funcs ( the carrier of T,REAL); ::_thesis: ( ( for n being Element of NAT st 0 <> n & n <= len F holds F . n is continuous RealMap of T ) implies ADD "**" F is continuous RealMap of T ) assume A2: for n being Element of NAT st 0 <> n & n <= len F holds F . n is continuous RealMap of T ; ::_thesis: ADD "**" F is continuous RealMap of T reconsider ADDF = ADD "**" F as RealMap of T by FUNCT_2:66; now__::_thesis:_ADD_"**"_F_is_continuous_RealMap_of_T percases ( len F = 0 or len F <> 0 ) ; supposeA3: len F = 0 ; ::_thesis: ADD "**" F is continuous RealMap of T A4: ADD is having_a_unity by A1, Th23; then ex x being Element of Funcs ( the carrier of T,REAL) st x is_a_unity_wrt ADD by SETWISEO:def_2; then A5: the_unity_wrt ADD is_a_unity_wrt ADD by BINOP_1:def_8; ADDF = the_unity_wrt ADD by A3, A4, FINSOP_1:def_1; hence ADD "**" F is continuous RealMap of T by A1, A5, Th24; ::_thesis: verum end; supposeA6: len F <> 0 ; ::_thesis: ADD "**" F is continuous RealMap of T A7: len F >= 1 proof assume len F < 1 ; ::_thesis: contradiction then len F < 1 + 0 ; hence contradiction by A6, NAT_1:13; ::_thesis: verum end; then consider f being Function of NAT,(Funcs ( the carrier of T,REAL)) such that A8: f . 1 = F . 1 and A9: for n being Element of NAT st 0 <> n & n < len F holds f . (n + 1) = ADD . ((f . n),(F . (n + 1))) and A10: ADD "**" F = f . (len F) by FINSOP_1:1; defpred S1[ Nat] means ( $1 <= len F implies f . $1 is continuous RealMap of T ); A11: for n being Nat st n >= 1 & S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] ) assume that A12: n >= 1 and A13: S1[n] ; ::_thesis: S1[n + 1] assume A14: n + 1 <= len F ; ::_thesis: f . (n + 1) is continuous RealMap of T reconsider n = n as Element of NAT by ORDINAL1:def_12; A15: n + 0 < n + 1 by XREAL_1:8; then n < len F by A14, XXREAL_0:2; then A16: f . (n + 1) = ADD . ((f . n),(F . (n + 1))) by A9, A12; 1 + 0 <= n + 1 by A12, XREAL_1:8; then n + 1 in Seg (len F) by A14, FINSEQ_1:1; then n + 1 in dom F by FINSEQ_1:def_3; then F . (n + 1) in rng F by FUNCT_1:def_3; then reconsider fn = f . n, Fn1 = F . (n + 1) as RealMap of T by FUNCT_2:66; Fn1 is continuous by A2, A14; then fn + Fn1 is continuous by A13, A14, A15, Th22, XXREAL_0:2; hence f . (n + 1) is continuous RealMap of T by A1, A16; ::_thesis: verum end; A17: S1[1] by A2, A8; for n being Nat st n >= 1 holds S1[n] from NAT_1:sch_8(A17, A11); hence ADD "**" F is continuous RealMap of T by A7, A10; ::_thesis: verum end; end; end; hence ADD "**" F is continuous RealMap of T ; ::_thesis: verum end; theorem :: NAGATA_1:26 for T, T1 being non empty TopSpace for F being Function of the carrier of T,(Funcs ( the carrier of T, the carrier of T1)) st ( for p being Point of T holds F . p is continuous Function of T,T1 ) holds for S being Function of the carrier of T,(bool the carrier of T) st ( for p being Point of T holds ( p in S . p & S . p is open & ( for p, q being Point of T st p in S . q holds (F . p) . p = (F . q) . p ) ) ) holds F Toler is continuous proof let T, T1 be non empty TopSpace; ::_thesis: for F being Function of the carrier of T,(Funcs ( the carrier of T, the carrier of T1)) st ( for p being Point of T holds F . p is continuous Function of T,T1 ) holds for S being Function of the carrier of T,(bool the carrier of T) st ( for p being Point of T holds ( p in S . p & S . p is open & ( for p, q being Point of T st p in S . q holds (F . p) . p = (F . q) . p ) ) ) holds F Toler is continuous let F be Function of the carrier of T,(Funcs ( the carrier of T, the carrier of T1)); ::_thesis: ( ( for p being Point of T holds F . p is continuous Function of T,T1 ) implies for S being Function of the carrier of T,(bool the carrier of T) st ( for p being Point of T holds ( p in S . p & S . p is open & ( for p, q being Point of T st p in S . q holds (F . p) . p = (F . q) . p ) ) ) holds F Toler is continuous ) assume A1: for p being Point of T holds F . p is continuous Function of T,T1 ; ::_thesis: for S being Function of the carrier of T,(bool the carrier of T) st ( for p being Point of T holds ( p in S . p & S . p is open & ( for p, q being Point of T st p in S . q holds (F . p) . p = (F . q) . p ) ) ) holds F Toler is continuous let S be Function of the carrier of T,(bool the carrier of T); ::_thesis: ( ( for p being Point of T holds ( p in S . p & S . p is open & ( for p, q being Point of T st p in S . q holds (F . p) . p = (F . q) . p ) ) ) implies F Toler is continuous ) assume A2: for p being Point of T holds ( p in S . p & S . p is open & ( for p, q being Point of T st p in S . q holds (F . p) . p = (F . q) . p ) ) ; ::_thesis: F Toler is continuous now__::_thesis:_for_t_being_Point_of_T_holds_F_Toler_is_continuous_at_t let t be Point of T; ::_thesis: F Toler is_continuous_at t for R being Subset of T1 st R is open & (F Toler) . t in R holds ex H being Subset of T st ( H is open & t in H & (F Toler) .: H c= R ) proof reconsider Ft = F . t as Function of T,T1 by A1; let R be Subset of T1; ::_thesis: ( R is open & (F Toler) . t in R implies ex H being Subset of T st ( H is open & t in H & (F Toler) .: H c= R ) ) assume that A3: R is open and A4: (F Toler) . t in R ; ::_thesis: ex H being Subset of T st ( H is open & t in H & (F Toler) .: H c= R ) Ft is continuous by A1; then A5: Ft is_continuous_at t by TMAP_1:50; Ft . t in R by A4, Def8; then consider A being Subset of T such that A6: ( A is open & t in A ) and A7: Ft .: A c= R by A3, A5, TMAP_1:43; set H = A /\ (S . t); A8: (F Toler) .: (A /\ (S . t)) c= R proof let FSh be set ; :: according to TARSKI:def_3 ::_thesis: ( not FSh in (F Toler) .: (A /\ (S . t)) or FSh in R ) assume FSh in (F Toler) .: (A /\ (S . t)) ; ::_thesis: FSh in R then consider h being set such that A9: h in dom (F Toler) and A10: h in A /\ (S . t) and A11: FSh = (F Toler) . h by FUNCT_1:def_6; reconsider h9 = h as Point of T by A9; ( h9 in S . t & FSh = (F . h9) . h9 ) by A10, A11, Def8, XBOOLE_0:def_4; then A12: FSh = Ft . h9 by A2; A13: the carrier of T = dom Ft by FUNCT_2:def_1; h9 in A by A10, XBOOLE_0:def_4; then FSh in Ft .: A by A12, A13, FUNCT_1:def_6; hence FSh in R by A7; ::_thesis: verum end; take A /\ (S . t) ; ::_thesis: ( A /\ (S . t) is open & t in A /\ (S . t) & (F Toler) .: (A /\ (S . t)) c= R ) ( S . t is open & t in S . t ) by A2; hence ( A /\ (S . t) is open & t in A /\ (S . t) & (F Toler) .: (A /\ (S . t)) c= R ) by A6, A8, XBOOLE_0:def_4; ::_thesis: verum end; hence F Toler is_continuous_at t by TMAP_1:43; ::_thesis: verum end; hence F Toler is continuous by TMAP_1:50; ::_thesis: verum end; definition let X be set ; let r be Real; let f be Function of X,REAL; deffunc H1( Element of X) -> set = min (r,(f . $1)); func min (r,f) -> Function of X,REAL means :Def9: :: NAGATA_1:def 9 for x being set st x in X holds it . x = min (r,(f . x)); existence ex b1 being Function of X,REAL st for x being set st x in X holds b1 . x = min (r,(f . x)) proof defpred S1[ set , set ] means ex a being Element of X st ( a = $1 & $2 = H1(a) ); A1: for x being set st x in X holds ex y being set st ( y in REAL & S1[x,y] ) proof let x be set ; ::_thesis: ( x in X implies ex y being set st ( y in REAL & S1[x,y] ) ) assume x in X ; ::_thesis: ex y being set st ( y in REAL & S1[x,y] ) then reconsider x = x as Element of X ; min (r,(f . x)) is Element of REAL by XREAL_0:def_1; hence ex y being set st ( y in REAL & S1[x,y] ) ; ::_thesis: verum end; consider Min being Function of X,REAL such that A2: for x being set st x in X holds S1[x,Min . x] from FUNCT_2:sch_1(A1); take Min ; ::_thesis: for x being set st x in X holds Min . x = min (r,(f . x)) let x be set ; ::_thesis: ( x in X implies Min . x = min (r,(f . x)) ) assume x in X ; ::_thesis: Min . x = min (r,(f . x)) then S1[x,Min . x] by A2; hence Min . x = min (r,(f . x)) ; ::_thesis: verum end; uniqueness for b1, b2 being Function of X,REAL st ( for x being set st x in X holds b1 . x = min (r,(f . x)) ) & ( for x being set st x in X holds b2 . x = min (r,(f . x)) ) holds b1 = b2 proof let M1, M2 be Function of X,REAL; ::_thesis: ( ( for x being set st x in X holds M1 . x = min (r,(f . x)) ) & ( for x being set st x in X holds M2 . x = min (r,(f . x)) ) implies M1 = M2 ) assume that A3: for x being set st x in X holds M1 . x = min (r,(f . x)) and A4: for x being set st x in X holds M2 . x = min (r,(f . x)) ; ::_thesis: M1 = M2 now__::_thesis:_for_x_being_set_st_x_in_X_holds_ M1_._x_=_M2_._x let x be set ; ::_thesis: ( x in X implies M1 . x = M2 . x ) assume A5: x in X ; ::_thesis: M1 . x = M2 . x reconsider y = x as Element of X by A5; M1 . x = H1(y) by A3, A5; hence M1 . x = M2 . x by A4, A5; ::_thesis: verum end; hence M1 = M2 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def9 defines min NAGATA_1:def_9_:_ for X being set for r being Real for f, b4 being Function of X,REAL holds ( b4 = min (r,f) iff for x being set st x in X holds b4 . x = min (r,(f . x)) ); theorem :: NAGATA_1:27 for T being non empty TopSpace for r being Real for f being RealMap of T st f is continuous holds min (r,f) is continuous proof let T be non empty TopSpace; ::_thesis: for r being Real for f being RealMap of T st f is continuous holds min (r,f) is continuous let r be Real; ::_thesis: for f being RealMap of T st f is continuous holds min (r,f) is continuous let f be RealMap of T; ::_thesis: ( f is continuous implies min (r,f) is continuous ) assume A1: f is continuous ; ::_thesis: min (r,f) is continuous reconsider f9 = f, mf9 = min (r,f) as Function of T,R^1 by TOPMETR:17; A2: f9 is continuous by A1, JORDAN5A:27; now__::_thesis:_for_t_being_Point_of_T_holds_mf9_is_continuous_at_t let t be Point of T; ::_thesis: mf9 is_continuous_at t for R being Subset of R^1 st R is open & mf9 . t in R holds ex U being Subset of T st ( U is open & t in U & mf9 .: U c= R ) proof reconsider ft = f . t as Point of RealSpace by METRIC_1:def_13; let R be Subset of R^1; ::_thesis: ( R is open & mf9 . t in R implies ex U being Subset of T st ( U is open & t in U & mf9 .: U c= R ) ) assume that A3: R is open and A4: mf9 . t in R ; ::_thesis: ex U being Subset of T st ( U is open & t in U & mf9 .: U c= R ) now__::_thesis:_ex_U_being_Subset_of_T_st_ (_U_is_open_&_t_in_U_&_(min_(r,f))_.:_U_c=_R_) percases ( f . t <= r or f . t > r ) ; supposeA5: f . t <= r ; ::_thesis: ex U being Subset of T st ( U is open & t in U & (min (r,f)) .: U c= R ) then f . t = min (r,(f . t)) by XXREAL_0:def_9; then ft in R by A4, Def9; then consider s being real number such that A6: s > 0 and A7: Ball (ft,s) c= R by A3, TOPMETR:15, TOPMETR:def_6; reconsider s9 = s as Real by XREAL_0:def_1; reconsider B = Ball (ft,s9) as Subset of R^1 by METRIC_1:def_13, TOPMETR:17; dist (ft,ft) < s9 by A6, METRIC_1:1; then A8: ft in B by METRIC_1:11; ( B is open & f9 is_continuous_at t ) by A2, TMAP_1:50, TOPMETR:14, TOPMETR:def_6; then consider U being Subset of T such that A9: ( U is open & t in U ) and A10: f9 .: U c= B by A8, TMAP_1:43; (min (r,f)) .: U c= R proof let mfx be set ; :: according to TARSKI:def_3 ::_thesis: ( not mfx in (min (r,f)) .: U or mfx in R ) assume mfx in (min (r,f)) .: U ; ::_thesis: mfx in R then consider x being set such that A11: x in dom (min (r,f)) and A12: x in U and A13: mfx = (min (r,f)) . x by FUNCT_1:def_6; reconsider x = x as Point of T by A11; reconsider fx = f . x, r9 = r as Point of RealSpace by METRIC_1:def_13; dom (min (r,f)) = the carrier of T by FUNCT_2:def_1; then x in dom f by A11, FUNCT_2:def_1; then A14: f . x in f .: U by A12, FUNCT_1:def_6; then A15: f . x in B by A10; now__::_thesis:_mfx_in_R percases ( f . x <= r or f . x > r ) ; suppose f . x <= r ; ::_thesis: mfx in R then min (r,(f . x)) = f . x by XXREAL_0:def_9; then mfx = f . x by A13, Def9; hence mfx in R by A7, A15; ::_thesis: verum end; supposeA16: f . x > r ; ::_thesis: mfx in R dist (fx,ft) < s by A10, A14, METRIC_1:11; then A17: abs ((f . x) - (f . t)) < s by TOPMETR:11; A18: r - (f . t) <= (f . x) - (f . t) by A16, XREAL_1:9; f . x >= f . t by A5, A16, XXREAL_0:2; then (f . x) - (f . t) >= 0 by XREAL_1:48; then (f . x) - (f . t) < s by A17, ABSVALUE:def_1; then A19: r - (f . t) < s by A18, XXREAL_0:2; r - (f . t) >= 0 by A5, XREAL_1:48; then abs (r - (f . t)) < s by A19, ABSVALUE:def_1; then dist (ft,r9) < s by TOPMETR:11; then A20: r in B by METRIC_1:11; min (r,(f . x)) = r by A16, XXREAL_0:def_9; then mfx = r by A13, Def9; hence mfx in R by A7, A20; ::_thesis: verum end; end; end; hence mfx in R ; ::_thesis: verum end; hence ex U being Subset of T st ( U is open & t in U & (min (r,f)) .: U c= R ) by A9; ::_thesis: verum end; supposeA21: f . t > r ; ::_thesis: ex U being Subset of T st ( U is open & t in U & (min (r,f)) .: U c= R ) set s = (f . t) - r; reconsider B = Ball (ft,((f . t) - r)) as Subset of R^1 by METRIC_1:def_13, TOPMETR:17; (f . t) - r > 0 by A21, XREAL_1:50; then dist (ft,ft) < (f . t) - r by METRIC_1:1; then A22: ft in B by METRIC_1:11; ( B is open & f9 is_continuous_at t ) by A2, TMAP_1:50, TOPMETR:14, TOPMETR:def_6; then consider U being Subset of T such that A23: ( U is open & t in U ) and A24: f9 .: U c= B by A22, TMAP_1:43; (min (r,f)) .: U c= R proof let mfx be set ; :: according to TARSKI:def_3 ::_thesis: ( not mfx in (min (r,f)) .: U or mfx in R ) assume mfx in (min (r,f)) .: U ; ::_thesis: mfx in R then consider x being set such that A25: x in dom (min (r,f)) and A26: x in U and A27: mfx = (min (r,f)) . x by FUNCT_1:def_6; reconsider x = x as Point of T by A25; reconsider fx = f . x as Point of RealSpace by METRIC_1:def_13; dom (min (r,f)) = the carrier of T by FUNCT_2:def_1; then x in dom f by A25, FUNCT_2:def_1; then f . x in f .: U by A26, FUNCT_1:def_6; then dist (ft,fx) < (f . t) - r by A24, METRIC_1:11; then abs ((f . t) - (f . x)) < (f . t) - r by TOPMETR:11; then (f . t) + (- (f . x)) <= (f . t) + (- r) by ABSVALUE:5; then - (f . x) <= - r by XREAL_1:6; then r <= f . x by XREAL_1:24; then A28: min (r,(f . x)) = r by XXREAL_0:def_9; min (r,(f . t)) = r by A21, XXREAL_0:def_9; then (min (r,f)) . t = r by Def9; hence mfx in R by A4, A27, A28, Def9; ::_thesis: verum end; hence ex U being Subset of T st ( U is open & t in U & (min (r,f)) .: U c= R ) by A23; ::_thesis: verum end; end; end; hence ex U being Subset of T st ( U is open & t in U & mf9 .: U c= R ) ; ::_thesis: verum end; hence mf9 is_continuous_at t by TMAP_1:43; ::_thesis: verum end; then mf9 is continuous by TMAP_1:50; hence min (r,f) is continuous by JORDAN5A:27; ::_thesis: verum end; definition let X be set ; let f be Function of [:X,X:],REAL; predf is_a_pseudometric_of X means :Def10: :: NAGATA_1:def 10 ( f is Reflexive & f is symmetric & f is triangle ); end; :: deftheorem Def10 defines is_a_pseudometric_of NAGATA_1:def_10_:_ for X being set for f being Function of [:X,X:],REAL holds ( f is_a_pseudometric_of X iff ( f is Reflexive & f is symmetric & f is triangle ) ); Lm8: for X being set for f being Function of [:X,X:],REAL holds ( f is_a_pseudometric_of X iff for a, b, c being Element of X holds ( f . (a,a) = 0 & f . (a,b) = f . (b,a) & f . (a,c) <= (f . (a,b)) + (f . (b,c)) ) ) proof let X be set ; ::_thesis: for f being Function of [:X,X:],REAL holds ( f is_a_pseudometric_of X iff for a, b, c being Element of X holds ( f . (a,a) = 0 & f . (a,b) = f . (b,a) & f . (a,c) <= (f . (a,b)) + (f . (b,c)) ) ) let f be Function of [:X,X:],REAL; ::_thesis: ( f is_a_pseudometric_of X iff for a, b, c being Element of X holds ( f . (a,a) = 0 & f . (a,b) = f . (b,a) & f . (a,c) <= (f . (a,b)) + (f . (b,c)) ) ) ( f is_a_pseudometric_of X iff ( f is Reflexive & f is symmetric & f is triangle ) ) by Def10; hence ( f is_a_pseudometric_of X iff for a, b, c being Element of X holds ( f . (a,a) = 0 & f . (a,b) = f . (b,a) & f . (a,c) <= (f . (a,b)) + (f . (b,c)) ) ) by METRIC_1:def_2, METRIC_1:def_4, METRIC_1:def_5; ::_thesis: verum end; theorem Th28: :: NAGATA_1:28 for X being set for f being Function of [:X,X:],REAL holds ( f is_a_pseudometric_of X iff for a, b, c being Element of X holds ( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) ) proof let X be set ; ::_thesis: for f being Function of [:X,X:],REAL holds ( f is_a_pseudometric_of X iff for a, b, c being Element of X holds ( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) ) let f be Function of [:X,X:],REAL; ::_thesis: ( f is_a_pseudometric_of X iff for a, b, c being Element of X holds ( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) ) thus ( f is_a_pseudometric_of X implies for a, b, c being Element of X holds ( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) ) ::_thesis: ( ( for a, b, c being Element of X holds ( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) ) implies f is_a_pseudometric_of X ) proof assume A1: f is_a_pseudometric_of X ; ::_thesis: for a, b, c being Element of X holds ( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) let a, b, c be Element of X; ::_thesis: ( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) f . (a,c) <= (f . (a,b)) + (f . (b,c)) by A1, Lm8; hence ( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) by A1, Lm8; ::_thesis: verum end; thus ( ( for a, b, c being Element of X holds ( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) ) implies f is_a_pseudometric_of X ) ::_thesis: verum proof assume A2: for a, b, c being Element of X holds ( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) ; ::_thesis: f is_a_pseudometric_of X A3: for a, b being Element of X holds f . (a,b) = f . (b,a) proof let a, b be Element of X; ::_thesis: f . (a,b) = f . (b,a) A4: ( f . (b,a) <= (f . (b,b)) + (f . (a,b)) & f . (b,b) = 0 ) by A2; ( f . (a,b) <= (f . (a,a)) + (f . (b,a)) & f . (a,a) = 0 ) by A2; hence f . (a,b) = f . (b,a) by A4, XXREAL_0:1; ::_thesis: verum end; for a, b, c being Element of X holds f . (a,c) <= (f . (a,b)) + (f . (b,c)) proof let x, y, z be Element of X; ::_thesis: f . (x,z) <= (f . (x,y)) + (f . (y,z)) f . (x,z) <= (f . (x,y)) + (f . (z,y)) by A2; hence f . (x,z) <= (f . (x,y)) + (f . (y,z)) by A3; ::_thesis: verum end; then ( f is Reflexive & f is symmetric & f is triangle ) by A2, A3, METRIC_1:def_2, METRIC_1:def_4, METRIC_1:def_5; hence f is_a_pseudometric_of X by Def10; ::_thesis: verum end; end; Lm9: for r being Real for X being non empty set for f being Function of [:X,X:],REAL for x, y being Element of X holds (min (r,f)) . (x,y) = min (r,(f . (x,y))) proof let r be Real; ::_thesis: for X being non empty set for f being Function of [:X,X:],REAL for x, y being Element of X holds (min (r,f)) . (x,y) = min (r,(f . (x,y))) let X be non empty set ; ::_thesis: for f being Function of [:X,X:],REAL for x, y being Element of X holds (min (r,f)) . (x,y) = min (r,(f . (x,y))) let f be Function of [:X,X:],REAL; ::_thesis: for x, y being Element of X holds (min (r,f)) . (x,y) = min (r,(f . (x,y))) let x, y be Element of X; ::_thesis: (min (r,f)) . (x,y) = min (r,(f . (x,y))) (min (r,f)) . (x,y) = min (r,(f . [x,y])) by Def9; hence (min (r,f)) . (x,y) = min (r,(f . (x,y))) ; ::_thesis: verum end; theorem Th29: :: NAGATA_1:29 for X being set for f being Function of [:X,X:],REAL st f is_a_pseudometric_of X holds for x, y being Element of X holds f . (x,y) >= 0 proof let X be set ; ::_thesis: for f being Function of [:X,X:],REAL st f is_a_pseudometric_of X holds for x, y being Element of X holds f . (x,y) >= 0 let f be Function of [:X,X:],REAL; ::_thesis: ( f is_a_pseudometric_of X implies for x, y being Element of X holds f . (x,y) >= 0 ) assume A1: f is_a_pseudometric_of X ; ::_thesis: for x, y being Element of X holds f . (x,y) >= 0 let x, y be Element of X; ::_thesis: f . (x,y) >= 0 ( f . (x,x) <= (f . (x,y)) + (f . (y,x)) & f . (x,x) = 0 ) by A1, Lm8; then 0 <= ((f . (x,y)) + (f . (x,y))) / 2 by A1, Lm8; hence f . (x,y) >= 0 ; ::_thesis: verum end; theorem Th30: :: NAGATA_1:30 for T being non empty TopSpace for r being Real for m being Function of [: the carrier of T, the carrier of T:],REAL st r > 0 & m is_a_pseudometric_of the carrier of T holds min (r,m) is_a_pseudometric_of the carrier of T proof let T be non empty TopSpace; ::_thesis: for r being Real for m being Function of [: the carrier of T, the carrier of T:],REAL st r > 0 & m is_a_pseudometric_of the carrier of T holds min (r,m) is_a_pseudometric_of the carrier of T let r be Real; ::_thesis: for m being Function of [: the carrier of T, the carrier of T:],REAL st r > 0 & m is_a_pseudometric_of the carrier of T holds min (r,m) is_a_pseudometric_of the carrier of T let m be Function of [: the carrier of T, the carrier of T:],REAL; ::_thesis: ( r > 0 & m is_a_pseudometric_of the carrier of T implies min (r,m) is_a_pseudometric_of the carrier of T ) assume that A1: r > 0 and A2: m is_a_pseudometric_of the carrier of T ; ::_thesis: min (r,m) is_a_pseudometric_of the carrier of T now__::_thesis:_for_a,_b,_c_being_Element_of_T_holds_ (_(min_(r,m))_._(a,a)_=_0_&_(min_(r,m))_._(a,c)_<=_((min_(r,m))_._(a,b))_+_((min_(r,m))_._(c,b))_) let a, b, c be Element of T; ::_thesis: ( (min (r,m)) . (a,a) = 0 & (min (r,m)) . (a,c) <= ((min (r,m)) . (a,b)) + ((min (r,m)) . (c,b)) ) m . (a,a) = 0 by A2, Th28; then min (r,(m . (a,a))) = 0 by A1, XXREAL_0:def_9; hence (min (r,m)) . (a,a) = 0 by Lm9; ::_thesis: (min (r,m)) . (a,c) <= ((min (r,m)) . (a,b)) + ((min (r,m)) . (c,b)) thus (min (r,m)) . (a,c) <= ((min (r,m)) . (a,b)) + ((min (r,m)) . (c,b)) ::_thesis: verum proof now__::_thesis:_(min_(r,m))_._(a,c)_<=_((min_(r,m))_._(a,b))_+_((min_(r,m))_._(c,b)) percases ( ((min (r,m)) . (a,b)) + ((min (r,m)) . (c,b)) >= r or ((min (r,m)) . (a,b)) + ((min (r,m)) . (c,b)) < r ) ; supposeA3: ((min (r,m)) . (a,b)) + ((min (r,m)) . (c,b)) >= r ; ::_thesis: (min (r,m)) . (a,c) <= ((min (r,m)) . (a,b)) + ((min (r,m)) . (c,b)) min (r,(m . (a,c))) <= r by XXREAL_0:17; then (min (r,m)) . (a,c) <= r by Lm9; hence (min (r,m)) . (a,c) <= ((min (r,m)) . (a,b)) + ((min (r,m)) . (c,b)) by A3, XXREAL_0:2; ::_thesis: verum end; supposeA4: ((min (r,m)) . (a,b)) + ((min (r,m)) . (c,b)) < r ; ::_thesis: (min (r,m)) . (a,c) <= ((min (r,m)) . (a,b)) + ((min (r,m)) . (c,b)) m . (c,b) >= 0 by A2, Th29; then 0 <= min (r,(m . (c,b))) by A1, XXREAL_0:20; then A5: 0 <= (min (r,m)) . (c,b) by Lm9; m . (a,b) >= 0 by A2, Th29; then 0 <= min (r,(m . (a,b))) by A1, XXREAL_0:20; then A6: 0 <= (min (r,m)) . (a,b) by Lm9; then (min (r,m)) . (a,b) < r by A4, A5, Lm1; then min (r,(m . (a,b))) < r by Lm9; then min (r,(m . (a,b))) = m . (a,b) by XXREAL_0:def_9; then A7: (min (r,m)) . (a,b) = m . (a,b) by Lm9; (min (r,m)) . (c,b) < r by A4, A6, A5, Lm1; then min (r,(m . (c,b))) < r by Lm9; then min (r,(m . (c,b))) = m . (c,b) by XXREAL_0:def_9; then A8: (min (r,m)) . (c,b) = m . (c,b) by Lm9; ( min (r,(m . (a,c))) <= m . (a,c) & m . (a,c) <= (m . (a,b)) + (m . (c,b)) ) by A2, Th28, XXREAL_0:17; then min (r,(m . (a,c))) <= (m . (a,b)) + (m . (c,b)) by XXREAL_0:2; hence (min (r,m)) . (a,c) <= ((min (r,m)) . (a,b)) + ((min (r,m)) . (c,b)) by A7, A8, Lm9; ::_thesis: verum end; end; end; hence (min (r,m)) . (a,c) <= ((min (r,m)) . (a,b)) + ((min (r,m)) . (c,b)) ; ::_thesis: verum end; end; hence min (r,m) is_a_pseudometric_of the carrier of T by Th28; ::_thesis: verum end; theorem :: NAGATA_1:31 for T being non empty TopSpace for r being Real for m being Function of [: the carrier of T, the carrier of T:],REAL st r > 0 & m is_metric_of the carrier of T holds min (r,m) is_metric_of the carrier of T proof let T be non empty TopSpace; ::_thesis: for r being Real for m being Function of [: the carrier of T, the carrier of T:],REAL st r > 0 & m is_metric_of the carrier of T holds min (r,m) is_metric_of the carrier of T let r be Real; ::_thesis: for m being Function of [: the carrier of T, the carrier of T:],REAL st r > 0 & m is_metric_of the carrier of T holds min (r,m) is_metric_of the carrier of T let m be Function of [: the carrier of T, the carrier of T:],REAL; ::_thesis: ( r > 0 & m is_metric_of the carrier of T implies min (r,m) is_metric_of the carrier of T ) assume that A1: r > 0 and A2: m is_metric_of the carrier of T ; ::_thesis: min (r,m) is_metric_of the carrier of T let a, b, c be Element of T; :: according to PCOMPS_1:def_6 ::_thesis: ( ( not (min (r,m)) . (a,b) = 0 or a = b ) & ( not a = b or (min (r,m)) . (a,b) = 0 ) & (min (r,m)) . (a,b) = (min (r,m)) . (b,a) & (min (r,m)) . (a,c) <= ((min (r,m)) . (a,b)) + ((min (r,m)) . (b,c)) ) for a, b, c being Element of T holds ( m . (a,a) = 0 & m . (a,b) = m . (b,a) & m . (a,c) <= (m . (a,b)) + (m . (b,c)) ) by A2, PCOMPS_1:def_6; then m is_a_pseudometric_of the carrier of T by Lm8; then A3: min (r,m) is_a_pseudometric_of the carrier of T by A1, Th30; ( (min (r,m)) . (a,b) = 0 implies a = b ) proof assume (min (r,m)) . (a,b) = 0 ; ::_thesis: a = b then min (r,(m . (a,b))) = 0 by Lm9; then m . (a,b) = 0 by A1, XXREAL_0:def_9; hence a = b by A2, PCOMPS_1:def_6; ::_thesis: verum end; hence ( (min (r,m)) . (a,b) = 0 iff a = b ) by A3, Lm8; ::_thesis: ( (min (r,m)) . (a,b) = (min (r,m)) . (b,a) & (min (r,m)) . (a,c) <= ((min (r,m)) . (a,b)) + ((min (r,m)) . (b,c)) ) thus ( (min (r,m)) . (a,b) = (min (r,m)) . (b,a) & (min (r,m)) . (a,c) <= ((min (r,m)) . (a,b)) + ((min (r,m)) . (b,c)) ) by A3, Lm8; ::_thesis: verum end;