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