:: Miscellaneous { I }
:: by Andrzej Trybulec
::
:: Received August 28, 2000
:: Copyright (c) 2000-2017 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;