Journal of Formalized Mathematics
Volume 14, 2002
University of Bialystok
Copyright (c) 2002 Association of Mizar Users

The abstract of the Mizar article:

On the General Position of Special Polygons

by
Mariusz Giero

Received May 27, 2002

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


environ

 vocabulary JORDAN12, FINSEQ_1, EUCLID, TOPREAL1, BOOLE, RELAT_1, REALSET1,
      PRE_TOPC, FUNCT_1, GRAPH_2, GOBOARD5, CONNSP_1, SUBSET_1, CARD_1,
      MATRIX_2, INT_1, FINSET_1, TARSKI, SETFAM_1, ARYTM_1, SEQM_3, RELAT_2,
      GOBOARD9, MCART_1, MATRIX_1, GOBOARD2, FINSEQ_4, GOBOARD1, JORDAN1,
      TOPS_1, TREES_1, SPPOL_1, FINSEQ_5;
 notation TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, XCMPLX_0, XREAL_0, REAL_1,
      NAT_1, BINARITH, ABIAN, INT_1, GRAPH_2, RELAT_1, CARD_1, FINSET_1,
      FUNCT_1, FINSEQ_1, FINSEQ_4, MATRIX_1, STRUCT_0, REALSET1, PRE_TOPC,
      TOPS_1, CONNSP_1, EUCLID, TOPREAL1, SPPOL_1, JORDAN1, GOBOARD1, GOBOARD2,
      GOBOARD5, GOBOARD9, GOBRD13;
 constructors REALSET1, FINSEQ_4, GRAPH_2, CONNSP_1, ABIAN, INT_1, GOBOARD9,
      TOPS_1, GOBOARD2, BINARITH, GOBRD13, JORDAN1, SPPOL_1, COMPTS_1,
      MEMBERED;
 clusters RELSET_1, SPPOL_2, EUCLID, GOBOARD5, ABIAN, YELLOW13, SUBSET_1,
      INT_1, GOBOARD2, GOBOARD9, JORDAN10, TEX_2, MEMBERED;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;


begin

reserve i,j,k,n for Nat,
        X,Y,a,b,c,x for set,
        r,s for Real;

theorem :: JORDAN12:1
    1 < i implies 0 < i-'1;

canceled;

theorem :: JORDAN12:3
1 is odd;

theorem :: JORDAN12:4
for f be FinSequence of TOP-REAL n
for i st 1 <= i & i + 1 <= len f holds
f/.i in rng f & f/.(i+1) in rng f;

definition
 cluster s.n.c. -> s.c.c. FinSequence of TOP-REAL 2;
end;

theorem :: JORDAN12:5
for f,g be FinSequence of TOP-REAL 2 st
  f ^' g is unfolded s.c.c. & len g >= 2 holds f is unfolded s.n.c.;

theorem :: JORDAN12:6
for g1,g2 be FinSequence of TOP-REAL 2 holds L~g1 c= L~(g1^'g2);

begin

definition let n; let f1,f2 be FinSequence of TOP-REAL n;
  pred f1 is_in_general_position_wrt f2 means
:: JORDAN12:def 1
   L~f1 misses rng f2 &
    for i st 1<=i & i < len f2 holds L~f1 /\ LSeg(f2,i) is trivial;
end;

definition let n; let f1,f2 be FinSequence of TOP-REAL n;
  pred f1,f2 are_in_general_position means
:: JORDAN12:def 2
   f1 is_in_general_position_wrt f2 &
    f2 is_in_general_position_wrt f1;
  symmetry;
end;

theorem :: JORDAN12:7
for f1,f2 being FinSequence of TOP-REAL 2 st
f1,f2 are_in_general_position holds
for f being FinSequence of TOP-REAL 2 st f = f2|(Seg k)
holds f1,f are_in_general_position;

theorem :: JORDAN12:8
for f1,f2,g1,g2 be FinSequence of TOP-REAL 2 st
  f1^'f2,g1^'g2 are_in_general_position holds
        f1^'f2,g1 are_in_general_position;

reserve f,g for FinSequence of TOP-REAL 2;

theorem :: JORDAN12:9
for k,f,g st 1<=k & k+1<=len g &
        f,g are_in_general_position holds g.k in (L~f)` & g.(k+1) in (L~f)`;

theorem :: JORDAN12:10
for f1,f2 be FinSequence of TOP-REAL 2
           st f1,f2 are_in_general_position
for i,j st (1 <= i & i + 1 <= len f1 & 1 <= j & j + 1 <= len f2)
    holds LSeg(f1,i) /\ LSeg(f2,j) is trivial;

theorem :: JORDAN12:11
for f,g holds
INTERSECTION({ LSeg(f,i) : 1 <= i & i+1 <= len f },
                { LSeg(g,j) : 1 <= j & j+1 <= len g }) is finite;

theorem :: JORDAN12:12
for f,g st f,g are_in_general_position holds
      L~f /\ L~g is finite;

theorem :: JORDAN12:13
 for f,g st f,g are_in_general_position
   for k holds L~f /\ LSeg(g,k) is finite;

begin

reserve f for non constant standard special_circular_sequence,

        p,p1,p2,q for Point of TOP-REAL 2;

theorem :: JORDAN12:14
  for f,p1,p2 st LSeg(p1,p2) misses L~f
  holds (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C));

theorem :: JORDAN12:15
(ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)` &
     a in C & b in C))
  iff ((a in RightComp f & b in RightComp f) or
           (a in LeftComp f & b in LeftComp f));

theorem :: JORDAN12:16
a in (L~f)` & b in (L~f)` & (not ex C be Subset of TOP-REAL 2 st
                           (C is_a_component_of (L~f)` & a in C & b in C))
  iff ((a in LeftComp f & b in RightComp f) or
           (a in RightComp f & b in LeftComp f));

theorem :: JORDAN12:17
for f,a,b,c st
      ((ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
        & a in C & b in C)) &
       (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
        & b in C & c in C))) holds
       ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
        & a in C & c in C);

theorem :: JORDAN12:18
for f,a,b,c st
   a in (L~f)` & b in (L~f)` & c in (L~f)` &
      ((not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
        & a in C & b in C)) &
       (not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
        & b in C & c in C))) holds
       ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
        & a in C & c in C);

begin

reserve G for Go-board;

theorem :: JORDAN12:19
  i <= len G implies v_strip(G,i) is convex;

theorem :: JORDAN12:20
  j <= width G implies h_strip(G,j) is convex;

theorem :: JORDAN12:21
 i <= len G & j <= width G implies cell(G,i,j) is convex;

theorem :: JORDAN12:22
for f,k st 1<=k & k+1<=len f holds left_cell(f,k) is convex;

theorem :: JORDAN12:23
for f,k st 1<=k & k+1<=len f holds
left_cell(f,k,GoB f) is convex & right_cell(f,k,GoB f) is convex;

begin

theorem :: JORDAN12:24
for p1,p2,f
for r be Point of TOP-REAL 2 st
 (r in LSeg(p1,p2) &
 (ex x st (L~f) /\ LSeg(p1,p2) = {x}) &
 not r in L~f)
holds L~f misses LSeg(p1,r) or L~f misses LSeg(r,p2);

theorem :: JORDAN12:25
 for p,q,r,s being Point of TOP-REAL 2
  st LSeg(p,q) is vertical & LSeg(r,s) is vertical &
   LSeg(p,q) meets LSeg(r,s)
 holds p`1 = r`1;

theorem :: JORDAN12:26
for p,p1,p2 st not p in LSeg(p1,p2) & p1`2 = p2`2 & p2`2 = p`2
holds p1 in LSeg(p,p2) or p2 in LSeg(p,p1);

theorem :: JORDAN12:27
for p,p1,p2 st not p in LSeg(p1,p2) & p1`1 = p2`1 & p2`1 = p`1
holds p1 in LSeg(p,p2) or p2 in LSeg(p,p1);

theorem :: JORDAN12:28
p <> p1 & p <> p2 & p in LSeg(p1,p2) implies not p1 in LSeg(p,p2);

theorem :: JORDAN12:29
for p,p1,p2,q st not q in LSeg(p1,p2) &
               p in LSeg(p1,p2) & p <> p1 & p <> p2 &
     (p1`1 = p2`1 & p2`1 = q`1 or p1`2 = p2`2 & p2`2 = q`2)
holds p1 in LSeg(q,p) or p2 in LSeg(q,p);

theorem :: JORDAN12:30
for p1,p2,p3,p4,p be Point of TOP-REAL 2 st
(p1`1 = p2`1 & p3`1 = p4`1 or p1`2 = p2`2 & p3`2 = p4`2)
 & LSeg(p1,p2) /\ LSeg(p3,p4) = {p}
holds p=p1 or p=p2 or p=p3;

begin

theorem :: JORDAN12:31
for p,p1,p2,f st (L~f) /\ LSeg(p1,p2) = {p}
for r be Point of TOP-REAL 2 st not r in LSeg(p1,p2) &
          not p1 in L~f & not p2 in L~f &
 ((p1`1 = p2`1 & p1`1 = r`1) or (p1`2 = p2`2 & p1`2 = r`2)) &
 (ex i st (1<=i & i+1<= len f & (r in right_cell(f,i,GoB f) or
               r in left_cell(f,i,GoB f)) & p in LSeg(f,i))) &
 not r in L~f holds
    (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & r in C & p1 in C)) or
     (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & r in C & p2 in C));

theorem :: JORDAN12:32
for f,p1,p2,p st (L~f) /\ LSeg(p1,p2) = {p}
for rl,rp be Point of TOP-REAL 2 st
       not p1 in L~f & not p2 in L~f &
       ((p1`1 = p2`1 & p1`1 = rl`1 & rl`1 = rp`1) or
           (p1`2 = p2`2 & p1`2 = rl`2 & rl`2 = rp`2)) &
      (ex i st (1<=i & i+1<= len f & rl in left_cell(f,i,GoB f) &
          rp in right_cell(f,i,GoB f) & p in LSeg(f,i))) &
      not rl in L~f &
      not rp in L~f holds
not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C);

theorem :: JORDAN12:33
for p,f,p1,p2 st L~f /\ LSeg(p1,p2) = {p} &
                 (p1`1=p2`1 or p1`2=p2`2) &
                 not p1 in L~f & not p2 in L~f &
                 rng f misses LSeg(p1,p2) holds
not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C);

theorem :: JORDAN12:34
for f being non constant standard special_circular_sequence,
    g being special FinSequence of TOP-REAL 2 st f,g are_in_general_position
for k st 1<=k & k+1<= len g holds
      Card (L~f /\ LSeg(g,k)) is even Nat iff
          ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & g.k in C & g.(k+1) in C);

theorem :: JORDAN12:35
for f1,f2,g1 being special FinSequence of TOP-REAL 2
  st f1 ^' f2 is non constant standard special_circular_sequence &
     f1 ^' f2, g1 are_in_general_position & len g1 >= 2 &
     g1 is unfolded s.n.c. holds
     Card (L~(f1 ^' f2) /\ L~g1) is even Nat iff
ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~(f1 ^' f2))`
        & g1.1 in C & g1.len g1 in C;

theorem :: JORDAN12:36
  for f1,f2,g1,g2 being special FinSequence of TOP-REAL 2
  st f1 ^' f2 is non constant standard special_circular_sequence &
     g1 ^' g2 is non constant standard special_circular_sequence &
     L~f1 misses L~g2 & L~f2 misses L~g1 &
     f1 ^' f2 , g1 ^' g2 are_in_general_position
for p1,p2,q1,q2 being Point of TOP-REAL 2
  st f1.1 = p1 & f1.len f1 = p2 & g1.1 = q1 & g1.len g1 = q2 &
     f1/.len f1 = f2/.1 & g1/.len g1 = g2/.1 &
     p1 in L~f1 /\ L~f2 & q1 in L~g1 /\ L~g2 &
     ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~(f1 ^' f2))`
        & q1 in C & q2 in C
     ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~(g1 ^' g2))`
        & p1 in C & p2 in C;

Back to top