Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999 Association of Mizar Users

The abstract of the Mizar article:

Properties of Left and Right Components

by
Artur Kornilowicz

Received May 5, 1999

MML identifier: GOBRD14
[ Mizar article, MML identifier index ]


environ

 vocabulary SEQM_3, GOBOARD5, SPRECT_2, PRE_TOPC, EUCLID, COMPTS_1, SPPOL_1,
      GOBOARD1, METRIC_1, CONNSP_1, RELAT_2, RELAT_1, JORDAN2C, SUBSET_1,
      LATTICES, BOOLE, TOPREAL1, TARSKI, COMPLEX1, ABSVALUE, SETFAM_1, ARYTM_1,
      FINSEQ_1, SQUARE_1, MCART_1, TREES_1, CARD_3, FUNCOP_1, RCOMP_1, FUNCT_1,
      MATRIX_1, JORDAN8, GROUP_1, ARYTM_3, PSCOMP_1, INT_1, POWER, GOBOARD9,
      GOBOARD2, TOPS_1, JORDAN1, FINSEQ_6, SPRECT_1, ORDINAL2, FUNCT_5, SEQ_2,
      FINSEQ_4, ARYTM;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
      BINOP_1, ORDINAL1, XCMPLX_0, XREAL_0, REAL_1, SQUARE_1, NAT_1, ABSVALUE,
      INT_1, POWER, MATRIX_1, BINARITH, FUNCT_4, SEQ_4, STRUCT_0, GROUP_1,
      METRIC_1, LIMFUNC1, TBSP_1, FINSEQ_1, CARD_3, CARD_4, FINSEQ_4, FINSEQ_6,
      RCOMP_1, PRE_TOPC, TOPS_1, TOPS_2, CONNSP_1, COMPTS_1, EUCLID, TOPREAL1,
      GOBOARD1, GOBOARD2, GOBOARD5, GOBOARD9, PSCOMP_1, SPPOL_1, JGRAPH_1,
      SPRECT_1, SPRECT_2, JORDAN2C, JORDAN8;
 constructors BINARITH, CARD_4, COMPTS_1, CONNSP_1, FINSEQ_4, GOBOARD2,
      GOBOARD9, JORDAN1, JORDAN2C, JORDAN8, LIMFUNC1, POWER, PSCOMP_1, RCOMP_1,
      REAL_1, REALSET1, SPPOL_1, SPRECT_1, SPRECT_2, TBSP_1, TOPGRP_1,
      TOPREAL2, TOPREAL4, TOPS_1, TOPS_2, WAYBEL_3, TOPRNS_1, MEMBERED,
      PARTFUN1;
 clusters SUBSET_1, XREAL_0, EUCLID, GOBOARD2, GOBRD11, PRE_TOPC, PSCOMP_1,
      RELSET_1, SPRECT_1, SPRECT_3, TOPREAL6, TOPS_1, REVROT_1, INT_1,
      JORDAN2C, MEMBERED, FUNCT_2, SEQM_3, RELAT_1, ZFMISC_1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin  :: Components

reserve i, j, n for Nat,
        f for non constant standard special_circular_sequence,
        g for clockwise_oriented
              non constant standard special_circular_sequence,
        p, q for Point of TOP-REAL 2,
        P, Q, R for Subset of TOP-REAL 2,
        C for compact non vertical non horizontal Subset of TOP-REAL 2,
        G for Go-board;

theorem :: GOBRD14:1
   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 :: GOBRD14:2
   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 :: GOBRD14:3
 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 :: GOBRD14:4
   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 :: GOBRD14:5
   P is_outside_component_of Q & R is_inside_component_of Q implies P misses R;

theorem :: GOBRD14:6
 for A, B being Subset of TOP-REAL 2 st
  A is_outside_component_of L~f & B is_outside_component_of L~f holds
 A = B;

theorem :: GOBRD14:7
   for p being Point of Euclid 2 st p = 0.REAL 2 & P is_outside_component_of L~
f
  ex r being Real st r > 0 & Ball(p,r)` c= P;

definition let C be closed Subset of TOP-REAL 2;
 cluster BDD C -> open;
 cluster UBD C -> open;
end;

definition let C be compact Subset of TOP-REAL 2;
 cluster UBD C -> connected;
end;

begin  :: Go-boards

theorem :: GOBRD14:8  :: TOPREAL1:29
   for f being FinSequence of TOP-REAL n st L~f <> {} holds 2 <= len f;

definition let n be Nat, a, b be Point of TOP-REAL n;
 func dist(a,b) -> Real means
:: GOBRD14:def 1
  ex p, q being Point of Euclid n st p = a & q = b & it = dist(p,q);
commutativity;
end;

theorem :: GOBRD14:9
 dist(p,q) = sqrt ((p`1-q`1)^2 + (p`2-q`2)^2);

theorem :: GOBRD14:10
 for p being Point of TOP-REAL n holds dist(p,p) = 0;

theorem :: GOBRD14:11
   for p, q, r being Point of TOP-REAL n holds
  dist(p,r) <= dist (p,q) + dist(q,r);

theorem :: GOBRD14:12
   for x1, x2, y1, y2 being real number,
     a, b being Point of TOP-REAL 2 st
  x1 <= a`1 & a`1 <= x2 & y1 <= a`2 & a`2 <= y2 &
  x1 <= b`1 & b`1 <= x2 & y1 <= b`2 & b`2 <= y2 holds
 dist(a,b) <= (x2-x1) + (y2-y1);

theorem :: GOBRD14:13
 1 <= i & i < len G & 1 <= j & j < width G implies
  cell(G,i,j) =
   product ((1,2) --> ([.G*(i,1)`1,G*(i+1,1)`1.],[.G*(1,j)`2,G*(1,j+1)`2.]));

theorem :: GOBRD14:14
   1 <= i & i < len G & 1 <= j & j < width G implies cell(G,i,j) is compact;

theorem :: GOBRD14:15
   [i,j] in Indices G & [i+n,j] in Indices G implies
  dist(G*(i,j),G*(i+n,j)) = G*(i+n,j)`1 - G*(i,j)`1;

theorem :: GOBRD14:16
   [i,j] in Indices G & [i,j+n] in Indices G implies
  dist(G*(i,j),G*(i,j+n)) = G*(i,j+n)`2 - G*(i,j)`2;

theorem :: GOBRD14:17
   3 <= len Gauge(C,n)-'1;

theorem :: GOBRD14:18
   i <= j implies
  for a, b being Nat st 2 <= a & a <= len Gauge(C,i) - 1 &
                        2 <= b & b <= len Gauge(C,i) - 1
   ex c, d being Nat st 2 <= c & c <= len Gauge(C,j) - 1 &
                        2 <= d & d <= len Gauge(C,j) - 1 &
      [c,d] in Indices Gauge(C,j) & Gauge(C,i)*(a,b) = Gauge(C,j)*(c,d) &
      c = 2 + 2|^(j-'i)*(a-'2) & d = 2 + 2|^(j-'i)*(b-'2);

theorem :: GOBRD14:19
 [i,j] in Indices Gauge(C,n) & [i,j+1] in Indices Gauge(C,n) implies
  dist(Gauge(C,n)*(i,j),Gauge(C,n)*(i,j+1)) = (N-bound C - S-bound C)/2|^n;

theorem :: GOBRD14:20
 [i,j] in Indices Gauge(C,n) & [i+1,j] in Indices Gauge(C,n) implies
  dist(Gauge(C,n)*(i,j),Gauge(C,n)*(i+1,j)) = (E-bound C - W-bound C)/2|^n;

theorem :: GOBRD14:21
   for r, t being real number holds r > 0 & t > 0 implies
  ex n being Nat st 1 < n &
   dist(Gauge(C,n)*(1,1),Gauge(C,n)*(1,2)) < r &
   dist(Gauge(C,n)*(1,1),Gauge(C,n)*(2,1)) < t;

begin  :: LeftComp and RightComp

theorem :: GOBRD14:22
 for P being Subset of (TOP-REAL 2)|(L~f)` st
  P is_a_component_of (TOP-REAL 2)|(L~f)` holds
 P = RightComp f or P = LeftComp f;

theorem :: GOBRD14:23
   for A1, A2 being Subset of TOP-REAL 2 st
  (L~f)` = A1 \/ A2 & A1 misses A2 &
  for C1, C2 being Subset of (TOP-REAL 2)|(L~f)`
    st C1 = A1 & C2 = A2 holds
     C1 is_a_component_of (TOP-REAL 2)|(L~f)` &
     C2 is_a_component_of (TOP-REAL 2)|(L~f)`
 holds A1 = RightComp f & A2 = LeftComp f or
       A1 = LeftComp f & A2 = RightComp f;

theorem :: GOBRD14:24
 LeftComp f misses RightComp f;

theorem :: GOBRD14:25
 L~f \/ RightComp f \/ LeftComp f = the carrier of TOP-REAL 2;

theorem :: GOBRD14:26
 p in L~f iff not p in LeftComp f & not p in RightComp f;

theorem :: GOBRD14:27
 p in LeftComp f iff not p in L~f & not p in RightComp f;

theorem :: GOBRD14:28
   p in RightComp f iff not p in L~f & not p in LeftComp f;

theorem :: GOBRD14:29
 L~f = (Cl RightComp f) \ RightComp f;

theorem :: GOBRD14:30
 L~f = (Cl LeftComp f) \ LeftComp f;

theorem :: GOBRD14:31
 Cl RightComp f = (RightComp f) \/ L~f;

theorem :: GOBRD14:32
   Cl LeftComp f = (LeftComp f) \/ L~f;

definition let f be non constant standard special_circular_sequence;
 cluster L~f -> Jordan;
end;

 reserve f for clockwise_oriented
              non constant standard special_circular_sequence;

theorem :: GOBRD14:33
 p in RightComp f implies W-bound L~f < p`1;

theorem :: GOBRD14:34
 p in RightComp f implies E-bound L~f > p`1;

theorem :: GOBRD14:35
 p in RightComp f implies N-bound L~f > p`2;

theorem :: GOBRD14:36
 p in RightComp f implies S-bound L~f < p`2;

theorem :: GOBRD14:37
 p in RightComp f & q in LeftComp f implies LSeg(p,q) meets L~f;

theorem :: GOBRD14:38
 Cl RightComp SpStSeq C =
  product((1,2)-->([.W-bound L~SpStSeq C,E-bound L~SpStSeq C.],
                   [.S-bound L~SpStSeq C,N-bound L~SpStSeq C.]));

theorem :: GOBRD14:39
 proj1.:(Cl RightComp f) = proj1.:(L~f);

theorem :: GOBRD14:40
  proj2.:(Cl RightComp f) = proj2.:(L~f);

theorem :: GOBRD14:41
 RightComp g c= RightComp SpStSeq L~g;

theorem :: GOBRD14:42
 Cl RightComp g is compact;

theorem :: GOBRD14:43
 LeftComp g is non Bounded;

theorem :: GOBRD14:44
 LeftComp g is_outside_component_of L~g;

theorem :: GOBRD14:45
   RightComp g is_inside_component_of L~g;

theorem :: GOBRD14:46
 UBD L~g = LeftComp g;

theorem :: GOBRD14:47
 BDD L~g = RightComp g;

theorem :: GOBRD14:48
   P is_outside_component_of L~g implies P = LeftComp g;

theorem :: GOBRD14:49
 P is_inside_component_of L~g implies P meets RightComp g;

theorem :: GOBRD14:50
   P is_inside_component_of L~g implies P = BDD L~g;

theorem :: GOBRD14:51
   W-bound L~g = W-bound RightComp g;

theorem :: GOBRD14:52
   E-bound L~g = E-bound RightComp g;

theorem :: GOBRD14:53
   N-bound L~g = N-bound RightComp g;

theorem :: GOBRD14:54
   S-bound L~g = S-bound RightComp g;


Back to top