:: Miscellaneous { I } :: by Andrzej Trybulec :: :: Received August 28, 2000 :: Copyright (c) 2000-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, XBOOLE_0, SUBSET_1, XXREAL_1, ARYTM_3, REAL_1, XXREAL_0, COMPLEX1, ARYTM_1, CARD_1, FUNCT_1, MCART_1, ZFMISC_1, PRE_TOPC, RCOMP_1, TARSKI, STRUCT_0, SETFAM_1, SEQ_1, RELAT_1, VALUED_0, SEQ_2, ORDINAL2, RELAT_2, PSCOMP_1, LIMFUNC1, CONNSP_1, METRIC_1, SEQ_4, XXREAL_2, TOPMETR, NAT_1, VALUED_1, EUCLID, MEASURE5; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XTUPLE_0, MCART_1, FUNCT_1, COMPLEX1, RELSET_1, FUNCT_2, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, XXREAL_1, XXREAL_2, NAT_1, VALUED_1, SEQ_1, SEQ_2, SEQ_4, STRUCT_0, PRE_TOPC, COMPTS_1, BORSUK_1, MEASURE5, MEASURE6, PSCOMP_1, VALUED_0, METRIC_1, TBSP_1, TOPMETR, LIMFUNC1, CONNSP_1, RLTOPSP1, EUCLID, RECDEF_1, RCOMP_1; constructors REAL_1, COMPLEX1, PROB_1, LIMFUNC1, BINARITH, CONNSP_1, COMPTS_1, TBSP_1, TOPMETR, MEASURE6, INTEGRA1, RECDEF_1, SEQ_4, PSCOMP_1, COMSEQ_2, XTUPLE_0; registrations SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, STRUCT_0, PRE_TOPC, COMPTS_1, BORSUK_1, EUCLID, TOPMETR, TOPREAL1, MEASURE6, JORDAN2C, BORSUK_3, INTEGRA1, VALUED_1, FUNCT_2, XXREAL_2, VALUED_0, FCONT_3, PSCOMP_1, MEASURE5, JORDAN5A, XTUPLE_0, NAT_1; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; begin :: Preliminaries scheme :: JCT_MISC:sch 1 NonEmpty{ A()-> non empty set, F(object)-> set}: the set of all F(a) where a is Element of A() is non empty; reserve r,s,r0,s0,t for Real; theorem :: JCT_MISC:1 for a,b being Real st r in [.a,b.] & s in [.a,b.] holds (r + s)/2 in [.a,b.]; theorem :: JCT_MISC:2 |.|.r0-s0.|-|.r-s.|.| <= |.r0-r.| + |.s0-s.|; theorem :: JCT_MISC:3 t in ].r,s.[ implies |.t.| < max(|.r.|,|.s.|); scheme :: JCT_MISC:sch 2 DoubleChoice{ A,B,C() -> non empty set, P[object,object,object]}: ex a being Function of A(), B(), b being Function of A(), C() st for i being Element of A() holds P [i,a.i,b.i] provided for i being Element of A() ex ai being Element of B(), bi being Element of C() st P[i,ai,bi]; theorem :: JCT_MISC:4 for S,T being non empty TopSpace, G being Subset of [:S,T:] st for x being Point of [:S,T:] st x in G ex GS being Subset of S, GT being Subset of T st GS is open & GT is open & x in [:GS,GT:] & [:GS,GT:] c= G holds G is open; begin :: topological properties of sets of real numbers theorem :: JCT_MISC:5 for A,B being compact Subset of REAL holds A /\ B is compact; theorem :: JCT_MISC:6 for T being non empty TopSpace for f being continuous RealMap of T for A being Subset of T st A is connected holds f.:A is interval; definition let A,B be Subset of REAL; func dist(A,B) -> Real means :: JCT_MISC:def 1 ex X being Subset of REAL st X = {|.r-s.| where r, s is Real : r in A & s in B} & it = lower_bound X; commutativity; end; theorem :: JCT_MISC:7 for A,B being Subset of REAL, r, s st r in A & s in B holds |.r-s.| >= dist(A,B); theorem :: JCT_MISC:8 for A,B being Subset of REAL, C,D being non empty Subset of REAL st C c= A & D c= B holds dist(A,B) <= dist(C,D); theorem :: JCT_MISC:9 for A, B being non empty compact Subset of REAL ex r,s being Real st r in A & s in B & dist(A,B) = |.r-s.|; theorem :: JCT_MISC:10 for A, B being non empty compact Subset of REAL holds dist(A,B) >= 0; theorem :: JCT_MISC:11 for A,B being non empty compact Subset of REAL st A misses B holds dist(A,B) > 0; theorem :: JCT_MISC:12 for e,f being Real, A,B being compact Subset of REAL st A misses B & A c= [.e,f.] & B c= [.e,f.] for S being sequence of bool REAL st for i being Nat holds S.i is interval & S.i meets A & S.i meets B ex r being Real st r in [.e,f.] & not r in A \/ B & for i being Nat ex k being Nat st i <= k & r in S.k; :: Moved from JORDAN1A, AK, 23.02.2006 theorem :: JCT_MISC:13 for S being closed Subset of TOP-REAL 2 st S is bounded holds proj2.:S is closed; theorem :: JCT_MISC:14 for S being Subset of TOP-REAL 2 st S is bounded holds proj2.:S is real-bounded; theorem :: JCT_MISC:15 for S being compact Subset of TOP-REAL 2 holds proj2.:S is compact;