:: Bounded Domains and Unbounded Domains
:: by Yatsuka Nakamura , Andrzej Trybulec and Czeslaw Bylinski
::
:: Received January 7, 1999
:: Copyright (c) 1999-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, SUBSET_1, REAL_1, XXREAL_0, CARD_1, COMPLEX1, ARYTM_1,
ARYTM_3, FINSEQ_1, RELAT_1, FUNCT_1, ORDINAL2, PRE_TOPC, EUCLID, RVSUM_1,
SQUARE_1, XBOOLE_0, RELAT_2, TARSKI, STRUCT_0, NAT_1, XXREAL_2, CONNSP_1,
METRIC_1, CONVEX1, CONNSP_3, ZFMISC_1, SETFAM_1, RLTOPSP1, FINSEQ_2,
SUPINF_2, BORSUK_1, XXREAL_1, BORSUK_2, GRAPH_1, TOPMETR, TREAL_1,
VALUED_1, FUNCT_4, RCOMP_1, TOPREAL1, TOPS_2, PCOMPS_1, WEIERSTR, SEQ_4,
PARTFUN1, FUNCOP_1, BINOP_2, ORDINAL4, JORDAN3, TBSP_1, CONNSP_2,
RUSUB_4, SPPOL_1, GOBOARD2, SPRECT_1, TREES_1, PSCOMP_1, GOBOARD1,
MCART_1, MATRIX_1, GOBOARD9, GOBOARD5, TOPS_1, JORDAN1, SPRECT_2,
JORDAN2C;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
RVSUM_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, ORDINAL1, CARD_1, NUMBERS,
XCMPLX_0, XREAL_0, XXREAL_2, COMPLEX1, SEQM_3, PRE_TOPC, TOPS_1, TOPS_2,
COMPTS_1, METRIC_1, BINOP_2, PCOMPS_1, CONNSP_1, CONNSP_2, TBSP_1,
CONNSP_3, TOPMETR, RCOMP_1, FINSEQ_1, FINSEQ_2, DOMAIN_1, STRUCT_0,
SQUARE_1, BORSUK_2, XXREAL_0, SEQ_4, FINSEQ_6, FUNCOP_1, FUNCT_3,
TREAL_1, FUNCT_4, RLVECT_1, RUSUB_4, RLTOPSP1, CONVEX1, EUCLID, SPPOL_1,
PSCOMP_1, SPRECT_1, SPRECT_2, TOPREAL1, MATRIX_0, GOBOARD1, GOBOARD2,
GOBOARD5, GOBOARD9, JORDAN2B, REAL_1, NAT_1, NAT_D, WEIERSTR, FINSOP_1;
constructors REAL_1, SQUARE_1, FINSEQOP, RCOMP_1, FINSOP_1, TOPS_1, CONNSP_1,
TOPS_2, COMPTS_1, TBSP_1, MONOID_0, TREAL_1, GOBOARD2, SPPOL_1, JORDAN1,
PSCOMP_1, WEIERSTR, BORSUK_2, GOBOARD9, CONNSP_3, JORDAN2B, SPRECT_1,
SPRECT_2, BINOP_2, GOBOARD1, NAT_D, SEQ_4, FUNCSDOM, CONVEX1, RUSUB_4,
SETWISEO, NUMBERS;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1,
NUMBERS, XXREAL_0, XREAL_0, MEMBERED, FINSEQ_1, STRUCT_0, PRE_TOPC,
TOPS_1, METRIC_1, BORSUK_1, TBSP_1, EUCLID, TOPMETR, GOBOARD2, JORDAN1,
BORSUK_2, SPRECT_1, SPRECT_3, VALUED_0, RLTOPSP1, JORDAN2B, MONOID_0,
SEQ_4, SPPOL_1, CARD_1, NAT_1, SQUARE_1, ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: from, RLAFFIN2, 2011.08.01, A.T.
registration
let n be Nat;
cluster TOP-REAL n -> add-continuous Mult-continuous;
end;
begin :: Definitions of Bounded Domain and Unbounded Domain
reserve m,n,i,i2,j for Nat,
r,r1,r2,s,t for Real,
x,y,z for object;
::$CT 5
theorem :: JORDAN2C:6
for f being increasing FinSequence of REAL st rng f={r,s} & len f
=2 & r<=s holds f.1=r & f.2=s;
reserve p,p1,p2,p3,q,q1,q2,q3,q4 for Point of TOP-REAL n;
::$CT
theorem :: JORDAN2C:8
|.|.q.|.|=|.q.|;
theorem :: JORDAN2C:9
|.|.q1.|- |.q2.|.|<=|.q1-q2.|;
theorem :: JORDAN2C:10
|.|[r]|.|=|.r.|;
theorem :: JORDAN2C:11
for n being Nat, A be Subset of TOP-REAL n
holds A is bounded iff A is bounded Subset of Euclid n;
theorem :: JORDAN2C:12
for A,B being Subset of TOP-REAL n st B is bounded & A c= B
holds A is bounded;
definition
::$CD
let n be Nat;
let A, B be Subset of TOP-REAL n;
pred B is_inside_component_of A means
:: JORDAN2C:def 2
B is_a_component_of A` & B is bounded;
end;
registration
let M be non empty MetrStruct;
cluster bounded for Subset of M;
end;
theorem :: JORDAN2C:13
for A being Subset of TOP-REAL n, B being Subset of TOP-REAL n
holds B is_inside_component_of A iff ex C being Subset of
((TOP-REAL n) | (A`))
st C=B & C is a_component & C is bounded Subset of Euclid n;
definition
let n be Nat;
let A, B be Subset of TOP-REAL n;
pred B is_outside_component_of A means
:: JORDAN2C:def 3
B is_a_component_of A` & B is not bounded;
end;
theorem :: JORDAN2C:14
for A being Subset of TOP-REAL n, B being Subset of TOP-REAL n
holds B is_outside_component_of A iff
ex C being Subset of ((TOP-REAL n) | (A`))
st C=B & C is a_component &
C is not bounded Subset of Euclid n;
theorem :: JORDAN2C:15
for A,B being Subset of TOP-REAL n st B is_inside_component_of A holds
B c= A`;
theorem :: JORDAN2C:16
for A,B being Subset of TOP-REAL n st B is_outside_component_of A
holds B c= A`;
definition
let n be Nat;
let A be Subset of TOP-REAL n;
func BDD A -> Subset of TOP-REAL n equals
:: JORDAN2C:def 4
union{B where B is Subset of
TOP-REAL n: B is_inside_component_of A};
end;
definition
let n be Nat;
let A be Subset of TOP-REAL n;
func UBD A -> Subset of TOP-REAL n equals
:: JORDAN2C:def 5
union{B where B is Subset of
TOP-REAL n: B is_outside_component_of A};
end;
registration
let n be Nat;
cluster [#](TOP-REAL n) -> convex;
end;
registration
let n;
cluster [#](TOP-REAL n) -> a_component;
end;
::$CT 3
theorem :: JORDAN2C:20
for A being Subset of TOP-REAL n holds BDD A is
a_union_of_components of (TOP-REAL n) | A`;
theorem :: JORDAN2C:21
for A being Subset of TOP-REAL n holds UBD A is
a_union_of_components of (TOP-REAL n) | A`;
theorem :: JORDAN2C:22
for A being Subset of TOP-REAL n, B being Subset of TOP-REAL n
st B is_inside_component_of A holds B c= BDD A;
theorem :: JORDAN2C:23
for A being Subset of TOP-REAL n, B being Subset of TOP-REAL n
st B is_outside_component_of A holds B c= UBD A;
theorem :: JORDAN2C:24
for A being Subset of TOP-REAL n holds BDD A misses UBD A;
theorem :: JORDAN2C:25
for A being Subset of TOP-REAL n holds BDD A c= A`;
theorem :: JORDAN2C:26
for A being Subset of TOP-REAL n holds UBD A c= A`;
theorem :: JORDAN2C:27
for A being Subset of TOP-REAL n holds (BDD A) \/ (UBD A) = A`;
reserve u for Point of Euclid n;
theorem :: JORDAN2C:28
for P being Subset of TOP-REAL n st P=REAL n holds P is connected;
::$CT 4
theorem :: JORDAN2C:33
for W being Subset of Euclid n st n>=1 & W=REAL n holds W is not bounded;
theorem :: JORDAN2C:34
for A being Subset of TOP-REAL n holds A is bounded iff
ex r being Real st
for q being Point of TOP-REAL n st q in A holds |.q.|=1 implies not [#](TOP-REAL n) is bounded;
theorem :: JORDAN2C:36
n>=1 implies UBD {}(TOP-REAL n)=REAL n;
theorem :: JORDAN2C:37
for w1,w2,w3 being Point of TOP-REAL n, P being non empty Subset
of TOP-REAL n, h1,h2 being Function of I[01],(TOP-REAL n) |P st
h1 is continuous
& w1=h1.0 & w2=h1.1 & h2 is continuous & w2=h2.0 & w3=h2.1 holds ex h3 being
Function of I[01],(TOP-REAL n) |P st h3 is continuous & w1=h3.0 & w3=h3.1;
theorem :: JORDAN2C:38
for P being Subset of TOP-REAL n, w1,w2,w3 being Point of
TOP-REAL n st w1 in P & w2 in P & w3 in P & LSeg(w1,w2) c= P & LSeg(w2,w3) c= P
ex h being Function of I[01],(TOP-REAL n) |P st h is continuous & w1=h.0 &
w3=h.1;
theorem :: JORDAN2C:39
for P being Subset of TOP-REAL n, w1,w2,w3,w4 being Point of
TOP-REAL n st w1 in P & w2 in P & w3 in P & w4 in P & LSeg(w1,w2) c= P & LSeg(
w2,w3) c= P & LSeg(w3,w4) c= P ex h being Function of I[01],(TOP-REAL n) |P
st h is continuous & w1=h.0 & w4=h.1;
theorem :: JORDAN2C:40
for P being Subset of TOP-REAL n, w1,w2,w3,w4,w5,w6,w7 being
Point of TOP-REAL n st w1 in P & w2 in P & w3 in P & w4 in P & w5 in P & w6 in
P & w7 in P & LSeg(w1,w2) c= P & LSeg(w2,w3) c= P & LSeg(w3,w4) c= P & LSeg(w4,
w5) c= P & LSeg(w5,w6) c= P & LSeg(w6,w7) c= P ex h being Function of I[01],(
TOP-REAL n) |P st h is continuous & w1=h.0 & w7=h.1;
theorem :: JORDAN2C:41
for w1,w2 being Point of TOP-REAL n,P being Subset of
TopSpaceMetr(Euclid n) st P=LSeg(w1,w2)& not (0.TOP-REAL n) in LSeg(w1,w2)
holds ex w0 being Point of TOP-REAL n st w0 in LSeg(w1,w2) & |.w0.|>0 & |.w0.|=
(dist_min(P)).(0.TOP-REAL n);
theorem :: JORDAN2C:42
for a being Real, Q being Subset of TOP-REAL n, w1,w4 being
Point of TOP-REAL n st Q={q : (|.q.|) > a } & w1 in Q & w4 in Q & not
(ex r being Real
st w1=r*w4 or w4=r*w1) holds ex w2,w3 being Point of TOP-REAL n st
w2 in Q & w3 in Q & LSeg(w1,w2) c=Q & LSeg(w2,w3) c= Q & LSeg(w3,w4) c= Q;
theorem :: JORDAN2C:43
for a being Real, Q being Subset of TOP-REAL n, w1,w4 being
Point of TOP-REAL n st Q=(REAL n)\ {q : (|.q.|) < a } & w1 in Q & w4 in Q & not
(ex r being Real st w1=r*w4 or w4=r*w1)
holds ex w2,w3 being Point of TOP-REAL
n st w2 in Q & w3 in Q & LSeg(w1,w2) c=Q & LSeg(w2,w3) c= Q & LSeg(w3,w4) c= Q;
theorem :: JORDAN2C:44
for f being FinSequence of REAL holds f is Element of REAL (len
f) & f is Point of TOP-REAL (len f);
theorem :: JORDAN2C:45
for x being Element of REAL n,f,g being FinSequence of REAL,
r being Real st f=x & g=r*x
holds len f=len g & for i being Element of NAT st 1<=
i & i<=len f holds g/.i=r*f/.i;
theorem :: JORDAN2C:46
for x being Element of REAL n,f being FinSequence st x<> 0*n & x
=f holds ex i being Element of NAT st 1<=i & i<=n & f.i<>0;
theorem :: JORDAN2C:47
for x being Element of REAL n st n>=2 & x<> 0*n holds ex y being
Element of REAL n st not ex r being Real st y=r*x or x=r*y;
theorem :: JORDAN2C:48
for a being Real, Q being Subset of TOP-REAL n, w1,w7 being
Point of TOP-REAL n st n>=2 & Q={q : (|.q.|) > a } & w1 in Q & w7 in Q &
(ex r being Real
st w1=r*w7 or w7=r*w1) holds ex w2,w3,w4,w5,w6 being Point of
TOP-REAL n st w2 in Q & w3 in Q & w4 in Q & w5 in Q & w6 in Q & LSeg(w1,w2) c=Q
& LSeg(w2,w3) c= Q & LSeg(w3,w4) c= Q & LSeg(w4,w5) c= Q & LSeg(w5,w6) c=Q &
LSeg(w6,w7) c= Q;
theorem :: JORDAN2C:49
for a being Real, Q being Subset of TOP-REAL n, w1,w7 being
Point of TOP-REAL n st n>=2 & Q=(REAL n)\ {q : (|.q.|) < a } & w1 in Q & w7 in
Q &
(ex r being Real st w1=r*w7 or w7=r*w1)
holds ex w2,w3,w4,w5,w6 being Point
of TOP-REAL n st w2 in Q & w3 in Q & w4 in Q & w5 in Q & w6 in Q & LSeg(w1,w2)
c=Q & LSeg(w2,w3) c= Q & LSeg(w3,w4) c= Q & LSeg(w4,w5) c= Q & LSeg(w5,w6) c=Q
& LSeg(w6,w7) c= Q;
theorem :: JORDAN2C:50
for a being Real st n>=1 holds {q: |.q.| >a} <>{};
theorem :: JORDAN2C:51
for a being Real, P being Subset of TOP-REAL n st n>=2 & P={q :
|.q.| > a } holds P is connected;
theorem :: JORDAN2C:52
for a being Real st n>=1 holds (REAL n) \ {q: |.q.| < a} <> {};
theorem :: JORDAN2C:53
for a being Real,P being Subset of TOP-REAL n st n>=2 & P=(REAL
n)\ {q : |.q.| < a } holds P is connected;
theorem :: JORDAN2C:54
for a being Real,n being Nat, P being Subset of
TOP-REAL n st n>=1 & P=(REAL n)\ {q where q is Point of TOP-REAL n: |.q.| < a }
holds not P is bounded;
theorem :: JORDAN2C:55
for a being Real,P being Subset of TOP-REAL 1 st P={q where q is
Point of TOP-REAL 1: ex r st q=<*r*> & r > a } holds P is convex;
theorem :: JORDAN2C:56
for a being Real,P being Subset of TOP-REAL 1 st P={q where q is
Point of TOP-REAL 1 : ex r st q=<*r*> & r < -a } holds P is convex;
::$CT 2
theorem :: JORDAN2C:59
for W being Subset of Euclid 1,a being Real
st W={q where q is Point of TOP-REAL 1 : ex r st q=<*r*> & r > a }
holds W is not bounded;
theorem :: JORDAN2C:60
for W being Subset of Euclid 1,a being Real
st W={q where q is Point of TOP-REAL 1 : ex r st q=<*r*> & r < -a }
holds W is not bounded;
theorem :: JORDAN2C:61
for W being Subset of Euclid n,a being Real
st n>=2 & W={q : |.q.| > a } holds W is not bounded;
theorem :: JORDAN2C:62
for W being Subset of Euclid n,a being Real
st n>=2 & W=(REAL n)\ {q : (|.q.|) < a } holds W is not bounded;
theorem :: JORDAN2C:63
for P, P1 being Subset of TOP-REAL n, Q being Subset of TOP-REAL
n, W being Subset of Euclid n st P=W & P is connected & W is not bounded & P1=
Component_of (Down(P,Q`)) & W misses Q holds P1 is_outside_component_of Q;
theorem :: JORDAN2C:64
for A being Subset of Euclid n, B being non empty Subset of
Euclid n, C being Subset of (Euclid n) | B st A=C & C is bounded holds A is
bounded;
theorem :: JORDAN2C:65
for A being Subset of TOP-REAL n st A is compact holds A is bounded;
registration
let n be Element of NAT;
cluster compact -> bounded for Subset of TOP-REAL n;
end;
theorem :: JORDAN2C:66
for A being Subset of TOP-REAL n st 1<=n & A is bounded holds A` <> {};
theorem :: JORDAN2C:67
for r being Real holds (ex B being Subset of Euclid n st B={q :
(|.q.|) < r }) & for A being Subset of Euclid n st A={q1 : (|.q1.|) < r } holds
A is bounded;
theorem :: JORDAN2C:68
for A being Subset of TOP-REAL n st n>=2 & A is bounded holds
UBD A is_outside_component_of A;
theorem :: JORDAN2C:69
for a being Real, P being Subset of TOP-REAL n st P={q : (|.q.|)
< a } holds P is convex;
theorem :: JORDAN2C:70
for a being Real,P being Subset of TOP-REAL n st P=Ball(u,a)
holds P is convex;
reserve R for Subset of TOP-REAL n;
reserve P,Q for Subset of TOP-REAL n;
::$CT
theorem :: JORDAN2C:72 :: uogolnic na wypukle !!!
p <> q & p in Ball(u,r) & q in Ball(u,r) implies ex h being
Function of I[01],TOP-REAL n st h is continuous & h.0=p & h.1=q & rng h c= Ball
(u,r);
theorem :: JORDAN2C:73
for f being Function of I[01],TOP-REAL n st f is continuous & f.
0=p1 & f.1=p2 & p in Ball(u,r) & p2 in Ball(u,r) ex h being Function of I[01],
TOP-REAL n st h is continuous & h.0=p1 & h.1=p & rng h c= rng f \/ Ball(u,r);
theorem :: JORDAN2C:74
for f being Function of I[01],TOP-REAL n st f is continuous &
rng f c=P & f.0=p1 & f.1=p2 & p in Ball(u,r) & p2 in Ball(u,r) & Ball(u,r) c= P
ex f1 being Function of I[01],TOP-REAL n st f1 is continuous & rng f1 c= P & f1
.0=p1 & f1.1=p;
theorem :: JORDAN2C:75
for p for P being Subset of TOP-REAL n st R is connected & R is
open & P = {q: q<>p & q in R & not ex f being Function of I[01],TOP-REAL n st f
is continuous & rng f c= R & f.0=p & f.1=q} holds P is open;
theorem :: JORDAN2C:76
for P being Subset of TOP-REAL n st R is connected & R is open &
p in R & P = {q: q=p or ex f being Function of I[01],TOP-REAL n st f is
continuous & rng f c= R & f.0=p & f.1=q} holds P is open;
theorem :: JORDAN2C:77
for R being Subset of TOP-REAL n holds p in R & P={q: q=p or ex
f being Function of I[01],TOP-REAL n st f is continuous & rng f c= R & f.0=p &
f.1=q} implies P c= R;
theorem :: JORDAN2C:78
for R being Subset of TOP-REAL n, p being Point of TOP-REAL n st
R is connected & R is open & p in R & P={q: q=p or ex f being Function of I[01]
,TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q} holds R c= P;
theorem :: JORDAN2C:79
for R being Subset of TOP-REAL n, p,q being Point of TOP-REAL n
st R is connected & R is open & p in R & q in R & p<>q holds ex f being
Function of I[01],TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q;
theorem :: JORDAN2C:80
for A being Subset of TOP-REAL n, a being Real st A={q:
|.q.|=a} holds A` is open & A is closed;
theorem :: JORDAN2C:81
for B being non empty Subset of TOP-REAL n st B is open holds
(TOP-REAL n) | B is locally_connected;
theorem :: JORDAN2C:82
for B being non empty Subset of TOP-REAL n, A being Subset of
TOP-REAL n,a being Real st A={q: |.q.|=a} & A`=B holds
(TOP-REAL n) | B is locally_connected;
theorem :: JORDAN2C:83
for f being Function of TOP-REAL n,R^1 st (for q holds f.q=|.q.|
) holds f is continuous;
theorem :: JORDAN2C:84
ex f being Function of TOP-REAL n,R^1 st (for q holds f.q=|.q.|)
& f is continuous;
theorem :: JORDAN2C:85
for g being Function of I[01],TOP-REAL n st g is continuous
holds ex f being Function of I[01],R^1 st (for t being Point of I[01] holds f.t
=|.g.t.|) & f is continuous;
theorem :: JORDAN2C:86
for g being Function of I[01],TOP-REAL n,a being Real st g is
continuous & |.g/.0 .|<=a & a<=|.g/.1 .| holds ex s being Point of I[01] st
|.g/.s.|=a;
theorem :: JORDAN2C:87
q=<*r*> implies |.q.|=|.r.|;
theorem :: JORDAN2C:88
for A being Subset of TOP-REAL n,a being Real st n>=1 & a>0 & A={q: |.
q.|=a} holds BDD A is_inside_component_of A;
begin ::bounded and Unbounded Domains of Rectangles
reserve D for non vertical non horizontal non empty compact Subset of TOP-REAL
2;
theorem :: JORDAN2C:89
len (GoB SpStSeq D)=2 & width (GoB SpStSeq D)=2 & (SpStSeq D)/.1
=(GoB SpStSeq D)*(1,2) & (SpStSeq D)/.2=(GoB SpStSeq D)*(2,2) & (SpStSeq D)/.3=
(GoB SpStSeq D)*(2,1) & (SpStSeq D)/.4=(GoB SpStSeq D)*(1,1) & (SpStSeq D)/.5=(
GoB SpStSeq D)*(1,2);
theorem :: JORDAN2C:90
LeftComp SpStSeq D is non bounded;
theorem :: JORDAN2C:91
LeftComp SpStSeq D c= UBD (L~SpStSeq D);
theorem :: JORDAN2C:92
for G being TopSpace,A,B,C being Subset of G st
A is a_component & B is a_component & C is connected & A meets C & B
meets C holds A=B;
theorem :: JORDAN2C:93
for B being Subset of TOP-REAL 2 st B is_a_component_of (L~
SpStSeq D)` & not B is bounded holds B=LeftComp SpStSeq D;
theorem :: JORDAN2C:94
RightComp SpStSeq D c= BDD (L~SpStSeq D) & RightComp SpStSeq D is bounded;
theorem :: JORDAN2C:95
LeftComp SpStSeq D = UBD (L~SpStSeq D) & RightComp SpStSeq D =
BDD (L~SpStSeq D);
theorem :: JORDAN2C:96
UBD (L~SpStSeq D)<>{} & UBD (L~SpStSeq D)
is_outside_component_of (L~SpStSeq D) & BDD (L~SpStSeq D)<>{} & BDD (L~SpStSeq
D) is_inside_component_of (L~SpStSeq D);
begin :: Jordan property and boundary property
theorem :: JORDAN2C:97
for G being non empty TopSpace, A being Subset of G st A`<>{}
holds A is boundary iff for x being set,V being Subset of G st x in A & x in V
& V is open ex B being Subset of G st B is_a_component_of A` & V meets B;
theorem :: JORDAN2C:98
for A being Subset of TOP-REAL 2 st A`<>{} holds A is boundary
& A is Jordan iff ex A1,A2 being Subset of TOP-REAL 2 st A` = A1 \/ A2 & A1
misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A=(Cl A1) \ A1 & for C1,C2 being
Subset of (TOP-REAL 2) | A` st C1 = A1 & C2 = A2 holds C1 is a_component
& C2 is a_component;
theorem :: JORDAN2C:99
for p being Point of TOP-REAL n, P being Subset of TOP-REAL n
st n>=1 & P={p} holds P is boundary;
theorem :: JORDAN2C:100
for p,q being Point of TOP-REAL 2,r st p`1=q`2 & -p`2=q`1 & p=r
*q holds p`1=0 & p`2=0 & p=0.TOP-REAL 2;
theorem :: JORDAN2C:101
for q1,q2 being Point of TOP-REAL 2 holds LSeg(q1,q2) is boundary;
registration
let q1,q2 be Point of TOP-REAL 2;
cluster LSeg(q1,q2) -> boundary;
end;
theorem :: JORDAN2C:102
for f being FinSequence of TOP-REAL 2 holds L~f is boundary;
registration
let f be FinSequence of TOP-REAL 2;
cluster L~f -> boundary;
end;
theorem :: JORDAN2C:103
for ep being Point of Euclid n,p,q being Point of TOP-REAL n st
p=ep & q in Ball(ep,r) holds |.p-q.|0 & p in L~SpStSeq D
holds ex q being Point of TOP-REAL 2 st q in UBD (L~SpStSeq D) & |.p-q.|0 & p in (L~SpStSeq
D) holds ex q being Point of TOP-REAL 2 st q in BDD (L~SpStSeq D) & |.p-q.| E-bound (
L~f) holds p in LeftComp f;
theorem :: JORDAN2C:112
for p being Point of TOP-REAL 2 st f/.1 = N-min L~f & p`2 < S-bound (
L~f) holds p in LeftComp f;
theorem :: JORDAN2C:113
for p being Point of TOP-REAL 2 st f/.1 = N-min L~f & p`2 > N-bound (
L~f) holds p in LeftComp f;
:: Moved from GOBRD14, AK, 22.02.2006
theorem :: JORDAN2C:114
for T being TopSpace, A being Subset of T, B being Subset of T st B
is_a_component_of A holds B is connected;
theorem :: JORDAN2C:115
for A being Subset of TOP-REAL n, B being Subset of TOP-REAL n st B
is_inside_component_of A holds B is connected;
theorem :: JORDAN2C:116
for A being Subset of TOP-REAL n, B being Subset of TOP-REAL n
st B is_outside_component_of A holds B is connected;
theorem :: JORDAN2C:117
for A being Subset of TOP-REAL n, B being Subset of TOP-REAL n st B
is_a_component_of A` holds A misses B;
theorem :: JORDAN2C:118
P is_outside_component_of Q & R is_inside_component_of Q implies P misses R;
theorem :: JORDAN2C:119
2 <= n implies for A, B, P being Subset of TOP-REAL n st P is bounded
& A is_outside_component_of P & B is_outside_component_of P holds A = B;
registration
let C be closed Subset of TOP-REAL 2;
cluster BDD C -> open;
cluster UBD C -> open;
end;
registration
let C be compact Subset of TOP-REAL 2;
cluster UBD C -> connected;
end;
:: Moved from JORDAN1C, AK, 22.02.2006
reserve p for Point of TOP-REAL 2;
theorem :: JORDAN2C:120
west_halfline p is non bounded;
theorem :: JORDAN2C:121
east_halfline p is non bounded;
theorem :: JORDAN2C:122
north_halfline p is non bounded;
theorem :: JORDAN2C:123
south_halfline p is non bounded;
registration
let C be compact Subset of TOP-REAL 2;
cluster UBD C -> non empty;
end;
theorem :: JORDAN2C:124
for C being compact Subset of TOP-REAL 2 holds UBD C is_a_component_of C`;
theorem :: JORDAN2C:125
for C being compact Subset of TOP-REAL 2 for WH being connected
Subset of TOP-REAL 2 st WH is non bounded & WH misses C holds WH c= UBD C;
theorem :: JORDAN2C:126
for C being compact Subset of TOP-REAL 2 for p being Point of TOP-REAL
2 st west_halfline p misses C holds west_halfline p c= UBD C;
theorem :: JORDAN2C:127
for C being compact Subset of TOP-REAL 2 for p being Point of TOP-REAL
2 st east_halfline p misses C holds east_halfline p c= UBD C;
theorem :: JORDAN2C:128
for C being compact Subset of TOP-REAL 2 for p being Point of TOP-REAL
2 st south_halfline p misses C holds south_halfline p c= UBD C;
theorem :: JORDAN2C:129
for C being compact Subset of TOP-REAL 2 for p being Point of TOP-REAL
2 st north_halfline p misses C holds north_halfline p c= UBD C;
theorem :: JORDAN2C:130
for n being Nat, r being Real st r > 0
for x,y,z being Element of Euclid n st x = 0*n
for p being Element of TOP-REAL n st p = y & r*p = z
holds r*dist(x,y) = dist(x,z);
theorem :: JORDAN2C:131
for n being Nat, r,s being Real st r > 0
for x being Element of Euclid n st x = 0*n
for A being Subset of TOP-REAL n st A = Ball(x,s)
holds r*A = Ball(x,r*s);
theorem :: JORDAN2C:132
for n being Nat, r,s,t be Real st 0 < s & s <= t
for x being Element of Euclid n st x = 0*n
for BA being Subset of TOP-REAL n st BA = Ball(x,r)
holds s*BA c= t*BA;