:: Topological Properties of Subsets in Real Numbers
:: by Konrad Raczkowski and Pawe{\l} Sadowski
::
:: Received June 18, 1990
:: Copyright (c) 1990-2018 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~~