:: Topological Properties of Subsets in Real Numbers :: by Konrad Raczkowski and Pawe{\l} Sadowski :: :: Received June 18, 1990 :: Copyright (c) 1990-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, SEQ_1, ORDINAL2, NAT_1, XXREAL_1, REAL_1, XXREAL_0, TARSKI, ARYTM_3, ARYTM_1, COMPLEX1, RELAT_1, VALUED_0, SEQ_2, XXREAL_2, FUNCT_1, CARD_1, XBOOLE_0, SEQ_4, RCOMP_1, ASYMPT_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, SEQ_1, SEQ_2, COMSEQ_2, VALUED_0, SEQ_4, XXREAL_0, XXREAL_1, XXREAL_2, RECDEF_1; constructors FUNCOP_1, REAL_1, NAT_1, XXREAL_1, COMPLEX1, PARTFUN1, SEQ_2, SEQM_3, SEQ_4, RECDEF_1, XXREAL_2, MEMBERED, RELSET_1, RVSUM_1, BINOP_2, COMSEQ_2, SEQ_1; registrations ORDINAL1, RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, VALUED_0, XXREAL_2, FUNCT_2, SEQ_1, SEQ_2; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve n,n1,m,k for Nat; reserve x,y for set; reserve s,g,g1,g2,r,p,p2,q,t for Real; reserve s1,s2,s3 for Real_Sequence; reserve Nseq for increasing sequence of NAT; reserve X for Subset of REAL; definition let g,s be Real; redefine func [. g,s .] -> Subset of REAL equals :: RCOMP_1:def 1 {r: g<=r & r<=s }; end; definition let g,s be ExtReal; redefine func ]. g,s .[ -> Subset of REAL equals :: RCOMP_1:def 2 {r : g open for Subset of REAL; cluster [.p,q.] -> closed for Subset of REAL; end; theorem :: RCOMP_1:8 X is compact implies X is closed; registration cluster compact -> closed for Subset of REAL; end; theorem :: RCOMP_1:9 (for p st p in X ex r,n st 0{} & X is closed & X is bounded_above holds upper_bound X in X; theorem :: RCOMP_1:13 for X st X<>{} & X is closed & X is bounded_below holds lower_bound X in X; theorem :: RCOMP_1:14 for X st X<>{} & X is compact holds upper_bound X in X & lower_bound X in X; theorem :: RCOMP_1:15 X is compact & (for g1,g2 st g1 in X & g2 in X holds [.g1,g2.] c= X) implies ex p,g st X = [.p,g.]; registration cluster open for Subset of REAL; end; definition let r be Real; mode Neighbourhood of r -> Subset of REAL means :: RCOMP_1:def 6 ex g st 0 open for Neighbourhood of r; end; theorem :: RCOMP_1:16 for N being Neighbourhood of r holds r in N; theorem :: RCOMP_1:17 for r for N1,N2 being Neighbourhood of r ex N being Neighbourhood of r st N c= N1 & N c= N2; theorem :: RCOMP_1:18 for X being open Subset of REAL, r st r in X ex N being Neighbourhood of r st N c= X; theorem :: RCOMP_1:19 for X being open Subset of REAL, r st r in X ex g st 0 Subset of REAL equals :: RCOMP_1:def 7 { r : g<=r & r Subset of REAL equals :: RCOMP_1:def 8 { r: g