The Mizar abstract of JORDAN2C

Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999 Association of Mizar Users
The abstract of the Mizar article:: Bounded Domains and Unbounded Domains
by
Yatsuka Nakamura,
Andrzej Trybulec, and
Czeslaw Bylinski
Received January 7, 1999
MML identifier: JORDAN2C
[ Mizar article, MML identifier index ]
environ

 vocabulary ABSVALUE, ARYTM_1, FINSEQ_1, RELAT_1, FUNCT_1, ORDINAL2, PRE_TOPC,
      EUCLID, COMPLEX1, SQUARE_1, RLVECT_1, RVSUM_1, TOPREAL1, RELAT_2,
      BORSUK_1, TOPS_2, SUBSET_1, RCOMP_1, BOOLE, LATTICES, CONNSP_1, TARSKI,
      CONNSP_3, SETFAM_1, GRAPH_1, ARYTM_3, TREAL_1, SEQ_1, FUNCT_4, TOPMETR,
      COMPTS_1, FINSEQ_2, METRIC_1, PCOMPS_1, WEIERSTR, SEQ_4, SEQ_2, VECTSP_1,
      FUNCOP_1, PARTFUN1, JORDAN3, TBSP_1, CONNSP_2, SPPOL_1, GOBOARD2,
      SPRECT_1, TREES_1, PSCOMP_1, GOBOARD1, MCART_1, CARD_1, MATRIX_1,
      GOBOARD9, SEQM_3, GOBOARD5, TOPS_1, JORDAN1, SPRECT_2, JORDAN2C,
      FINSEQ_4, CARD_3, ARYTM;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
      FUNCT_2, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, CARD_1,
      PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, METRIC_1, STRUCT_0, PCOMPS_1,
      CONNSP_1, CONNSP_2, TBSP_1, CONNSP_3, TOPRNS_1, TOPMETR, RCOMP_1,
      FINSEQ_1, FINSEQ_2, FINSEQ_4, SQUARE_1, ABSVALUE, BORSUK_2, WEIERSTR,
      SEQ_4, JORDAN3, BINARITH, FUNCOP_1, FUNCT_3, VECTSP_1, TREAL_1, FUNCT_4,
      RVSUM_1, EUCLID, SPPOL_1, PSCOMP_1, SPRECT_1, SPRECT_2, TOPREAL1,
      MATRIX_1, GOBOARD1, JORDAN1, GOBOARD2, GOBOARD5, GOBOARD9, JORDAN2B;
 constructors WEIERSTR, REAL_1, TOPS_1, TOPS_2, COMPTS_1, REALSET1, CONNSP_1,
      TBSP_1, CONNSP_3, FINSEQ_4, JORDAN1, RCOMP_1, GOBOARD2, GOBOARD9,
      FINSEQOP, SQUARE_1, ABSVALUE, BORSUK_2, JORDAN3, TREAL_1, FUNCT_4,
      SPPOL_1, SPRECT_1, TOPREAL2, SPRECT_2, PSCOMP_1, BINARITH, JORDAN2B,
      PARTFUN1, TOPRNS_1, DOMAIN_1, MEMBERED, XCMPLX_0;
 clusters SUBSET_1, RELSET_1, STRUCT_0, PRE_TOPC, METRIC_1, PCOMPS_1, SPRECT_1,
      TOPMETR, TOPREAL1, BORSUK_1, FUNCT_1, FUNCOP_1, FINSEQ_1, XREAL_0,
      FINSET_1, SPRECT_3, EUCLID, GOBOARD1, GOBOARD2, ARYTM_3, MEMBERED,
      ZFMISC_1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin ::Definitions of Bounded Domain and Unbounded Domain

reserve m,n,i,i2,j for Nat,
        r,r1,r2,s for Real,
        x,y,z,y1,y2 for set;

theorem :: JORDAN2C:1
r<=0 implies abs(r)=-r;

theorem :: JORDAN2C:2
for n,m st n<=m & m<=n+2 holds m=n or m=n+1 or m=n+2;

theorem :: JORDAN2C:3
for n,m st n<=m & m<=n+3 holds m=n or m=n+1 or m=n+2 or m=n+3;

theorem :: JORDAN2C:4
for n,m st n<=m & m<=n+4 holds
m=n or m=n+1 or m=n+2 or m=n+3 or m=n+4;

theorem :: JORDAN2C:5
for a,b being real number st a>=0 & b>=0 holds a+b>=0;

theorem :: JORDAN2C:6
for a,b being real number st a>0 & b>=0 holds a+b>0;

theorem :: JORDAN2C:7
for f being FinSequence st rng f={x,y} & len f=2
holds f.1=x & f.2=y or f.1=y & f.2=x;

theorem :: JORDAN2C:8
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;

theorem :: JORDAN2C:9
p1+p2-p3=p1-p3+p2;

theorem :: JORDAN2C:10
abs(|.q.|)=|.q.|;

theorem :: JORDAN2C:11
abs(|.q1.|- |.q2.|)<=|.q1-q2.|;

theorem :: JORDAN2C:12
|.|[r]|.|=abs(r);

theorem :: JORDAN2C:13
q-0.REAL n=q & (0.REAL n)-q = -q;

theorem :: JORDAN2C:14
for P being Subset of TOP-REAL n st P is convex
 holds P is connected;

theorem :: JORDAN2C:15
for G being non empty TopSpace,
P being Subset of G,A being Subset of G,
Q being Subset of G|A st P=Q & P is connected
holds Q is connected;

definition let n;let A be Subset of TOP-REAL n;
  canceled;
attr A is Bounded means
:: JORDAN2C:def 2
ex C being Subset of Euclid n st C=A & C is bounded;
end;

theorem :: JORDAN2C:16
for A,B being Subset of TOP-REAL n st B is Bounded &
A c= B holds A is Bounded;

definition let n;let A be Subset of TOP-REAL n;
  let B be Subset of TOP-REAL n;
pred B is_inside_component_of A means
:: JORDAN2C:def 3
 B is_a_component_of A` & B is Bounded;
end;

definition let M be non empty MetrStruct;
cluster bounded Subset of M;
end;

theorem :: JORDAN2C:17
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_of ((TOP-REAL n)|(A`)) &
 C is bounded Subset of Euclid n;

definition let n;let A be Subset of TOP-REAL n;
   let B be Subset of TOP-REAL n;
pred B is_outside_component_of A means
:: JORDAN2C:def 4
 B is_a_component_of A` & B is not Bounded;
end;

theorem :: JORDAN2C:18
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_of ((TOP-REAL n)|(A`)) &
  C is not bounded Subset of Euclid n;

theorem :: JORDAN2C:19
for A,B being Subset of TOP-REAL n st
B is_inside_component_of A holds B c= A`;

theorem :: JORDAN2C:20
for A,B being Subset of TOP-REAL n st
B is_outside_component_of A holds B c= A`;

definition let n;let A be Subset of TOP-REAL n;
func BDD A -> Subset of TOP-REAL n equals
:: JORDAN2C:def 5
 union{B where B is Subset of TOP-REAL n: B is_inside_component_of A};
end;

definition let n;let A be Subset of TOP-REAL n;
func UBD A -> Subset of TOP-REAL n equals
:: JORDAN2C:def 6
 union{B where B is Subset of TOP-REAL n: B is_outside_component_of A};
end;

theorem :: JORDAN2C:21
[#](TOP-REAL n) is convex;

theorem :: JORDAN2C:22
[#](TOP-REAL n) is connected;

definition let n;
 cluster [#](TOP-REAL n) -> connected;
end;

theorem :: JORDAN2C:23
[#](TOP-REAL n) is_a_component_of TOP-REAL n;

theorem :: JORDAN2C:24
for A being Subset of TOP-REAL n holds
BDD A is a_union_of_components of (TOP-REAL n)|A`;

theorem :: JORDAN2C:25
for A being Subset of TOP-REAL n holds
UBD A is a_union_of_components of (TOP-REAL n)|A`;

theorem :: JORDAN2C:26
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:27
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:28
for A being Subset of TOP-REAL n holds
 BDD A misses UBD A;

theorem :: JORDAN2C:29
for A being Subset of TOP-REAL n holds
BDD A c= A`;

theorem :: JORDAN2C:30
for A being Subset of TOP-REAL n holds
UBD A c= A`;

theorem :: JORDAN2C:31
for A being Subset of TOP-REAL n holds
(BDD A) \/ (UBD A) = A`;

reserve u for Point of Euclid n;

theorem :: JORDAN2C:32
 for G being non empty TopSpace,
   w1,w2,w3 being Point of G,
   h1,h2 being map of I[01],G
   st h1 is continuous & w1=h1.0 & w2=h1.1 &
  h2 is continuous & w2=h2.0 & w3=h2.1 holds
  ex h3 being map of I[01],G st h3 is continuous & w1=h3.0 & w3=h3.1 &
  rng h3 c= (rng h1) \/ (rng h2);

theorem :: JORDAN2C:33
for P being Subset of TOP-REAL n
 st P=REAL n holds P is connected;

definition let n;
   func 1*n -> FinSequence of REAL equals
:: JORDAN2C:def 7
   n |-> (1 qua Real);
end;

definition let n;
  redefine func 1*n -> Element of REAL n;
end;

definition let n;
  func 1.REAL n -> Point of TOP-REAL n equals
:: JORDAN2C:def 8
     1*n;
end;

theorem :: JORDAN2C:34
abs 1*n = n |-> (1 qua Real);

theorem :: JORDAN2C:35
|.1*n.| = sqrt n;

theorem :: JORDAN2C:36
1.REAL 1 = <* 1 qua Real *>;

theorem :: JORDAN2C:37
|. (1.REAL n) .| = sqrt n;

theorem :: JORDAN2C:38
1<=n implies 1<=|. (1.REAL n) .|;

theorem :: JORDAN2C:39
for W being Subset of Euclid n
 st n>=1 & W=REAL n holds W is not bounded;

theorem :: JORDAN2C:40
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.|<r;

theorem :: JORDAN2C:41
n>=1 implies not [#](TOP-REAL n) is Bounded;

theorem :: JORDAN2C:42
n>=1 implies UBD {}(TOP-REAL n)=REAL n;

theorem :: JORDAN2C:43
for w1,w2,w3 being Point of TOP-REAL n,
 P being non empty Subset of TOP-REAL n,
 h1,h2 being map 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 map of I[01],(TOP-REAL n)|P st
 h3 is continuous & w1=h3.0 & w3=h3.1;

theorem :: JORDAN2C:44
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 map of I[01],(TOP-REAL n)|P st h is continuous
                        & w1=h.0 & w3=h.1;

theorem :: JORDAN2C:45
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 map of I[01],(TOP-REAL n)|P st h is continuous
                        & w1=h.0 & w4=h.1;

theorem :: JORDAN2C:46
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 map of I[01],(TOP-REAL n)|P st h is continuous
                        & w1=h.0 & w7=h.1;

reserve s2 for Real;

theorem :: JORDAN2C:47
for w1,w2 being Point of TOP-REAL n st
not (ex r being Real st w1=r*w2 or w2=r*w1)
holds not (0.REAL n) in LSeg(w1,w2);

theorem :: JORDAN2C:48
for w1,w2 being Point of TOP-REAL n,P being Subset of
 TopSpaceMetr(Euclid n) st P=LSeg(w1,w2)&
 not (0.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.REAL n);

theorem :: JORDAN2C:49
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:50
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;

canceled;

theorem :: JORDAN2C:52
for f being FinSequence of REAL holds f is Element of REAL (len f)
 & f is Point of TOP-REAL (len f);

theorem :: JORDAN2C:53
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 Nat st 1<=i & i<=len f holds g/.i=r*f/.i;

theorem :: JORDAN2C:54
for x being Element of REAL n,f being FinSequence
 st x<> 0*n & x=f holds ex i being Nat st 1<=i & i<=n & f.i<>0;

theorem :: JORDAN2C:55
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:56
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:57
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:58
for a being Real st n>=1 holds {q: |.q.| >a} <>{};

theorem :: JORDAN2C:59
for a being Real,
P being Subset of TOP-REAL n st n>=2 & P={q : |.q.| > a }
 holds P is connected;

theorem :: JORDAN2C:60
for a being Real st n>=1 holds
  (REAL n) \ {q: |.q.| < a} <> {};

theorem :: JORDAN2C:61
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:62
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:63
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:64
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:65
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 connected;

theorem :: JORDAN2C:66
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 connected;

theorem :: JORDAN2C:67
for W being Subset of Euclid 1,a being Real,
P being Subset of TOP-REAL 1
 st W={q where q is Point of TOP-REAL 1 : ex r st q=<*r*> & r > a }
    & P=W holds P is connected & W is not bounded;

theorem :: JORDAN2C:68
for W being Subset of Euclid 1,a being Real,
P being Subset of TOP-REAL 1
 st W={q where q is Point of TOP-REAL 1 : ex r st q=<*r*> & r < -a }
    & P=W holds P is connected & W is not bounded;

theorem :: JORDAN2C:69
for W being Subset of Euclid n,a being Real,
P being Subset of TOP-REAL n st n>=2 & W={q : |.q.| > a }
    & P=W holds P is connected & W is not bounded;

theorem :: JORDAN2C:70
for W being Subset of Euclid n,a being Real,
P being Subset of TOP-REAL n st n>=2 & W=(REAL n)\ {q : (|.q.|) < a }
    & P=W holds P is connected & W is not bounded;

theorem :: JORDAN2C:71
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=skl (Down(P,Q`)) & W misses Q holds
P1 is_outside_component_of Q;

theorem :: JORDAN2C:72
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= B & A=C & C is bounded holds A is bounded;

theorem :: JORDAN2C:73
for A being Subset of TOP-REAL n st
A is compact holds A is Bounded;

theorem :: JORDAN2C:74
for A being Subset of TOP-REAL n st 1<=n & A is Bounded holds
 A` <> {};

theorem :: JORDAN2C:75
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:76
for A being Subset of TOP-REAL n st n>=2 & A is Bounded
 ex B being Subset of TOP-REAL n st B is_outside_component_of A & B=UBD A;

theorem :: JORDAN2C:77
for a being Real, P being Subset of TOP-REAL n st
 P={q : (|.q.|) < a } holds P is convex;

theorem :: JORDAN2C:78
for a being Real,P being Subset of TOP-REAL n st P=Ball(u,a)
 holds P is convex;

theorem :: JORDAN2C:79
for a being Real,P being Subset of TOP-REAL n
 st P={q : |.q.| < a } holds P is connected;

reserve R for Subset of TOP-REAL n;
reserve P for Subset of TOP-REAL n;

theorem :: JORDAN2C:80
p <> q & p in Ball(u,r) & q in Ball(u,r) implies
ex h being map of I[01],TOP-REAL n st h is continuous & h.0=p & h.1=q &
      rng h c= Ball(u,r);

theorem :: JORDAN2C:81
for f being map 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 map 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:82
for f being map 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 map of I[01],TOP-REAL n st
      f1 is continuous & rng f1 c= P & f1.0=p1 & f1.1=p;

theorem :: JORDAN2C:83
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 map 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:84
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 map 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:85
for R being Subset of TOP-REAL n holds
p in R & P={q: q=p or
      ex f being map 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:86
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 map 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:87
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 map of I[01],TOP-REAL n st f is continuous & rng f c= R &
f.0=p & f.1=q;

theorem :: JORDAN2C:88
for A being Subset of TOP-REAL n, a being real number
st A={q: |.q.|=a} holds A` is open & A is closed;

theorem :: JORDAN2C:89
for B being non empty Subset of TOP-REAL n
st B is open holds (TOP-REAL n)|B is locally_connected;

theorem :: JORDAN2C:90
for B being non empty Subset of TOP-REAL n,
A being Subset of TOP-REAL n,a being real number st
A={q: |.q.|=a} & A`=B holds (TOP-REAL n)|B is locally_connected;

theorem :: JORDAN2C:91
for f being map of TOP-REAL n,R^1 st
 (for q holds f.q=|.q.|) holds f is continuous;

theorem :: JORDAN2C:92
ex f being map of TOP-REAL n,R^1 st
 (for q holds f.q=|.q.|) & f is continuous;

definition
  canceled;
  let X, Y be non empty 1-sorted, f be map of X,Y, x be set;
  assume x is Point of X;
 func pi(f,x) -> Point of Y equals
:: JORDAN2C:def 10
 f.x;
end;

theorem :: JORDAN2C:93
for g being map of I[01],TOP-REAL n st
 g is continuous holds ex f being map of I[01],R^1 st
 (for t being Point of I[01] holds f.t=|.g.t.|)
 & f is continuous;

theorem :: JORDAN2C:94
for g being map of I[01],TOP-REAL n,a being Real st
 g is continuous & |.pi(g,0).|<=a & a<=|.pi(g,1).| holds
 ex s being Point of I[01] st |.pi(g,s).|=a;

theorem :: JORDAN2C:95
q=<*r*> implies |.q.|=abs(r);

theorem :: JORDAN2C:96
for A being Subset of TOP-REAL n,a being Real
st n>=1 & a>0 & A={q: |.q.|=a}
holds ex B being Subset of TOP-REAL n st
B is_inside_component_of A & B=BDD 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:97
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:98
 LeftComp SpStSeq D is non Bounded;

theorem :: JORDAN2C:99
LeftComp SpStSeq D c= UBD (L~SpStSeq D);

theorem :: JORDAN2C:100
for G being TopSpace,A,B,C being Subset of G st
A is_a_component_of G & B is_a_component_of G & C is connected
& A meets C & B meets C holds A=B;

theorem :: JORDAN2C:101
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:102
RightComp SpStSeq D c= BDD (L~SpStSeq D) & RightComp SpStSeq D is Bounded;

theorem :: JORDAN2C:103
 LeftComp SpStSeq D = UBD (L~SpStSeq D) &
 RightComp SpStSeq D = BDD (L~SpStSeq D);

theorem :: JORDAN2C:104
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:105
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:106
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_of (TOP-REAL 2)|A` &
      C2 is_a_component_of (TOP-REAL 2)|A`;

theorem :: JORDAN2C:107
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:108
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.REAL 2;

theorem :: JORDAN2C:109
for q1,q2 being Point of TOP-REAL 2 holds
LSeg(q1,q2) is boundary;

definition let q1,q2 be Point of TOP-REAL 2;
 cluster LSeg(q1,q2) -> boundary;
end;

theorem :: JORDAN2C:110
for f being FinSequence of TOP-REAL 2 holds L~f is boundary;

definition let f be FinSequence of TOP-REAL 2;
 cluster L~f -> boundary;
end;

theorem :: JORDAN2C:111
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.|<r & |.q-p.|<r;

theorem :: JORDAN2C:112
for a being Real,p being Point of TOP-REAL 2
st a>0 & p in L~SpStSeq D holds ex q being Point of TOP-REAL 2 st
q in UBD (L~SpStSeq D) & |.p-q.|<a;

theorem :: JORDAN2C:113
REAL 0 = {0.REAL 0};

theorem :: JORDAN2C:114
for A being Subset of TOP-REAL n st
A is Bounded holds BDD A is Bounded;

theorem :: JORDAN2C:115
for G being non empty TopSpace,A,B,C,D being Subset of G st
A is_a_component_of G & B is_a_component_of G & C is_a_component_of G
& A \/ B=the carrier of G & C misses A holds C=B;

theorem :: JORDAN2C:116
for A being Subset of TOP-REAL 2 st
A is Bounded & A is Jordan holds BDD A is_inside_component_of A;

theorem :: JORDAN2C:117
for a being Real,p being Point of TOP-REAL 2
st a>0 & p in (L~SpStSeq D) holds ex q being Point of TOP-REAL 2 st
q in BDD (L~SpStSeq D) & |.p-q.|<a;

begin :: Points in LeftComp

reserve f for
   clockwise_oriented (non constant standard special_circular_sequence);

theorem :: JORDAN2C:118
for p being Point of TOP-REAL 2 st f/.1 = N-min L~f &
 p`1 < W-bound (L~f) holds p in LeftComp f;

theorem :: JORDAN2C:119
for p being Point of TOP-REAL 2 st f/.1 = N-min L~f &
 p`1 > E-bound (L~f) holds p in LeftComp f;

theorem :: JORDAN2C:120
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:121
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;
The abstract of the Mizar article:

Bounded Domains and Unbounded Domains
