:: Topological Properties of Subsets in Real Numbers :: by Konrad Raczkowski and Pawe{\l} Sadowski :: :: Received June 18, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin definition let g, s be real number ; :: original:[. redefine func[.g,s.] -> Subset of REAL equals :: RCOMP_1:def 1 { r where r is Real : ( g <= r & r <= s ) } ; coherence [.g,s.] is Subset of REAL proofend; compatibility for b1 being Subset of REAL holds ( b1 = [.g,s.] iff b1 = { r where r is Real : ( g <= r & r <= s ) } ) proofend; end; :: deftheorem defines [. RCOMP_1:def_1_:_ for g, s being real number holds [.g,s.] = { r where r is Real : ( g <= r & r <= s ) } ; definition let g, s be ext-real number ; :: original:]. redefine func].g,s.[ -> Subset of REAL equals :: RCOMP_1:def 2 { r where r is Real : ( g < r & r < s ) } ; coherence ].g,s.[ is Subset of REAL proofend; compatibility for b1 being Subset of REAL holds ( b1 = ].g,s.[ iff b1 = { r where r is Real : ( g < r & r < s ) } ) proofend; end; :: deftheorem defines ]. RCOMP_1:def_2_:_ for g, s being ext-real number holds ].g,s.[ = { r where r is Real : ( g < r & r < s ) } ; theorem Th1: :: RCOMP_1:1 for r, p, g being real number holds ( r in ].(p - g),(p + g).[ iff abs (r - p) < g ) proofend; theorem :: RCOMP_1:2 for r, p, g being real number holds ( r in [.p,g.] iff abs ((p + g) - (2 * r)) <= g - p ) proofend; theorem :: RCOMP_1:3 for r, p, g being real number holds ( r in ].p,g.[ iff abs ((p + g) - (2 * r)) < g - p ) proofend; definition let X be Subset of REAL; attrX is compact means :Def3: :: RCOMP_1:def 3 for s1 being Real_Sequence st rng s1 c= X holds ex s2 being Real_Sequence st ( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ); end; :: deftheorem Def3 defines compact RCOMP_1:def_3_:_ for X being Subset of REAL holds ( X is compact iff for s1 being Real_Sequence st rng s1 c= X holds ex s2 being Real_Sequence st ( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) ); definition let X be Subset of REAL; attrX is closed means :Def4: :: RCOMP_1:def 4 for s1 being Real_Sequence st rng s1 c= X & s1 is convergent holds lim s1 in X; end; :: deftheorem Def4 defines closed RCOMP_1:def_4_:_ for X being Subset of REAL holds ( X is closed iff for s1 being Real_Sequence st rng s1 c= X & s1 is convergent holds lim s1 in X ); definition let X be Subset of REAL; attrX is open means :Def5: :: RCOMP_1:def 5 X ` is closed ; end; :: deftheorem Def5 defines open RCOMP_1:def_5_:_ for X being Subset of REAL holds ( X is open iff X ` is closed ); theorem Th4: :: RCOMP_1:4 for s, g being real number for s1 being Real_Sequence st rng s1 c= [.s,g.] holds s1 is bounded proofend; theorem Th5: :: RCOMP_1:5 for s, g being real number holds [.s,g.] is closed proofend; theorem :: RCOMP_1:6 for s, g being real number holds [.s,g.] is compact proofend; theorem Th7: :: RCOMP_1:7 for p, q being real number holds ].p,q.[ is open proofend; registration let p, q be real number ; cluster].p,q.[ -> open for Subset of REAL; coherence for b1 being Subset of REAL st b1 = ].p,q.[ holds b1 is open by Th7; cluster[.p,q.] -> closed for Subset of REAL; coherence for b1 being Subset of REAL st b1 = [.p,q.] holds b1 is closed by Th5; end; theorem Th8: :: RCOMP_1:8 for X being Subset of REAL st X is compact holds X is closed proofend; registration cluster compact -> closed for Element of K19(REAL); coherence for b1 being Subset of REAL st b1 is compact holds b1 is closed by Th8; end; theorem Th9: :: RCOMP_1:9 for s1 being Real_Sequence for X being Subset of REAL st ( for p being real number st p in X holds ex r being real number ex n being Element of NAT st ( 0 < r & ( for m being Element of NAT st n < m holds r < abs ((s1 . m) - p) ) ) ) holds for s2 being Real_Sequence st s2 is subsequence of s1 & s2 is convergent holds not lim s2 in X proofend; theorem Th10: :: RCOMP_1:10 for X being Subset of REAL st X is compact holds X is real-bounded proofend; theorem :: RCOMP_1:11 for X being Subset of REAL st X is real-bounded & X is closed holds X is compact proofend; theorem Th12: :: RCOMP_1:12 for X being Subset of REAL st X <> {} & X is closed & X is bounded_above holds upper_bound X in X proofend; theorem Th13: :: RCOMP_1:13 for X being Subset of REAL st X <> {} & X is closed & X is bounded_below holds lower_bound X in X proofend; theorem :: RCOMP_1:14 for X being Subset of REAL st X <> {} & X is compact holds ( upper_bound X in X & lower_bound X in X ) proofend; theorem :: RCOMP_1:15 for X being Subset of REAL st X is compact & ( for g1, g2 being real number st g1 in X & g2 in X holds [.g1,g2.] c= X ) holds ex p, g being real number st X = [.p,g.] proofend; registration clusterV50() V51() V52() open for Element of K19(REAL); existence ex b1 being Subset of REAL st b1 is open proofend; end; definition let r be real number ; mode Neighbourhood of r -> Subset of REAL means :Def6: :: RCOMP_1:def 6 ex g being real number st ( 0 < g & it = ].(r - g),(r + g).[ ); existence ex b1 being Subset of REAL ex g being real number st ( 0 < g & b1 = ].(r - g),(r + g).[ ) proofend; end; :: deftheorem Def6 defines Neighbourhood RCOMP_1:def_6_:_ for r being real number for b2 being Subset of REAL holds ( b2 is Neighbourhood of r iff ex g being real number st ( 0 < g & b2 = ].(r - g),(r + g).[ ) ); registration let r be real number ; cluster -> open for Neighbourhood of r; coherence for b1 being Neighbourhood of r holds b1 is open proofend; end; theorem :: RCOMP_1:16 for r being real number for N being Neighbourhood of r holds r in N proofend; theorem :: RCOMP_1:17 for r being real number for N1, N2 being Neighbourhood of r ex N being Neighbourhood of r st ( N c= N1 & N c= N2 ) proofend; theorem Th18: :: RCOMP_1:18 for X being open Subset of REAL for r being real number st r in X holds ex N being Neighbourhood of r st N c= X proofend; theorem :: RCOMP_1:19 for X being open Subset of REAL for r being real number st r in X holds ex g being real number st ( 0 < g & ].(r - g),(r + g).[ c= X ) proofend; theorem :: RCOMP_1:20 for X being Subset of REAL st ( for r being real number st r in X holds ex N being Neighbourhood of r st N c= X ) holds X is open proofend; theorem Th21: :: RCOMP_1:21 for X being Subset of REAL st X is open & X is bounded_above holds not upper_bound X in X proofend; theorem Th22: :: RCOMP_1:22 for X being Subset of REAL st X is open & X is bounded_below holds not lower_bound X in X proofend; theorem :: RCOMP_1:23 for X being Subset of REAL st X is open & X is real-bounded & ( for g1, g2 being real number st g1 in X & g2 in X holds [.g1,g2.] c= X ) holds ex p, g being real number st X = ].p,g.[ proofend; :: From RCOMP_2, AG 19.12.2008 definition let g be real number ; let s be ext-real number ; :: original:[. redefine func[.g,s.[ -> Subset of REAL equals :: RCOMP_1:def 7 { r where r is Real : ( g <= r & r < s ) } ; coherence [.g,s.[ is Subset of REAL proofend; compatibility for b1 being Subset of REAL holds ( b1 = [.g,s.[ iff b1 = { r where r is Real : ( g <= r & r < s ) } ) proofend; end; :: deftheorem defines [. RCOMP_1:def_7_:_ for g being real number for s being ext-real number holds [.g,s.[ = { r where r is Real : ( g <= r & r < s ) } ; definition let g be ext-real number ; let s be real number ; :: original:]. redefine func].g,s.] -> Subset of REAL equals :: RCOMP_1:def 8 { r where r is Real : ( g < r & r <= s ) } ; coherence ].g,s.] is Subset of REAL proofend; compatibility for b1 being Subset of REAL holds ( b1 = ].g,s.] iff b1 = { r where r is Real : ( g < r & r <= s ) } ) proofend; end; :: deftheorem defines ]. RCOMP_1:def_8_:_ for g being ext-real number for s being real number holds ].g,s.] = { r where r is Real : ( g < r & r <= s ) } ;