The abstract of the Mizar article:

Properties of the Internal Approximation of Jordan's Curve

by

Robert Milewski

Received June 27, 2002

MML identifier: JORDAN14

[ Mizar article, MML identifier index ]

environ

 vocabulary JORDAN14, FINSEQ_1, BOOLE, PRE_TOPC, RELAT_2, CONNSP_1, RELAT_1,
      ARYTM_1, GOBOARD1, EUCLID, MATRIX_1, ABSVALUE, GOBRD13, TOPREAL1,
      GOBOARD5, TOPS_1, TREES_1, SPPOL_1, MCART_1, TARSKI, SUBSET_1, SEQM_3,
      GOBOARD9, COMPTS_1, JORDAN8, PSCOMP_1, GROUP_1, ARYTM_3, JORDAN11,
      JORDAN1H, JORDAN13, TOPREAL2, FINSEQ_4, JORDAN2C;
 notation TARSKI, XBOOLE_0, SUBSET_1, GOBOARD5, STRUCT_0, XREAL_0, REAL_1,
      NAT_1, BINARITH, ABSVALUE, CARD_4, FINSEQ_1, FINSEQ_4, MATRIX_1,
      PRE_TOPC, TOPREAL2, TOPS_1, COMPTS_1, CONNSP_1, EUCLID, TOPREAL1,
      GOBOARD1, SPPOL_1, PSCOMP_1, GOBOARD9, JORDAN2C, JORDAN8, GOBRD13,
      JORDAN1H, JORDAN11, JORDAN13;
 constructors REAL_1, FINSEQ_4, CARD_4, BINARITH, TOPS_1, CONNSP_1, PSCOMP_1,
      REALSET1, GOBOARD9, GROUP_1, JORDAN1, JORDAN2C, JORDAN1H, JORDAN8,
      JORDAN11, JORDAN13, WSIERP_1, TOPREAL4;
 clusters RELSET_1, REVROT_1, SPRECT_2, JORDAN8, TOPREAL1, TOPREAL6, INT_1,
      SUBSET_1, PRE_TOPC, SPRECT_3, SPRECT_4, BORSUK_2, JORDAN1A, GOBRD14,
      TOPS_1, JORDAN1B, MEMBERED;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

  theorem :: JORDAN14:1
   for f be non constant standard special_circular_sequence holds
    BDD L~f = RightComp f or BDD L~f = LeftComp f;

  theorem :: JORDAN14:2
     for f be non constant standard special_circular_sequence holds
    UBD L~f = RightComp f or UBD L~f = LeftComp f;

  theorem :: JORDAN14:3
     for G be Go-board
   for f be FinSequence of TOP-REAL 2
   for k be Nat holds
    1 <= k & k+1 <= len f & f is_sequence_on G
     implies left_cell(f,k,G) is closed;

  theorem :: JORDAN14:4
   for G be Go-board
   for p be Point of TOP-REAL 2
   for i,j be Nat st 1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G holds
    p in Int cell(G,i,j) iff
    G*(i,j)`1 < p`1 & p`1 < G*(i+1,j)`1 & G*(i,j)`2 < p`2 & p`2 < G*(i,j+1)`2;

  theorem :: JORDAN14:5
   for f be non constant standard special_circular_sequence holds
    BDD L~f is connected;

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

  definition
   let C be Simple_closed_curve;
   let n be Nat;
   func SpanStart(C,n) -> Point of TOP-REAL 2 equals
:: JORDAN14:def 1
    Gauge(C,n)*(X-SpanStart(C,n),Y-SpanStart(C,n));
  end;

  theorem :: JORDAN14:6
   for C be Simple_closed_curve
   for n be Nat st n is_sufficiently_large_for C holds
    Span(C,n)/.1 = SpanStart(C,n);

  theorem :: JORDAN14:7
   for C be Simple_closed_curve
   for n be Nat st n is_sufficiently_large_for C holds
    SpanStart(C,n) in BDD C;

  theorem :: JORDAN14:8
   for C be Simple_closed_curve
   for n,k be Nat st n is_sufficiently_large_for C holds
    1 <= k & k+1 <= len Span(C,n) implies
     right_cell(Span(C,n),k,Gauge(C,n)) misses C &
     left_cell(Span(C,n),k,Gauge(C,n)) meets C;

  theorem :: JORDAN14:9
   for C be Simple_closed_curve
   for n be Nat st n is_sufficiently_large_for C holds
    C misses L~Span(C,n);

  definition
   let C be Simple_closed_curve;
   let n be Nat;
   cluster Cl RightComp Span(C,n) -> compact;
  end;

  theorem :: JORDAN14:10
   for C be Simple_closed_curve
   for n be Nat st n is_sufficiently_large_for C holds
    C meets LeftComp Span(C,n);

  theorem :: JORDAN14:11
   for C be Simple_closed_curve
   for n be Nat st n is_sufficiently_large_for C holds
    C misses RightComp Span(C,n);

  theorem :: JORDAN14:12
   for C be Simple_closed_curve
   for n be Nat st n is_sufficiently_large_for C holds
    C c= LeftComp Span(C,n);

  theorem :: JORDAN14:13
   for C be Simple_closed_curve
   for n be Nat st n is_sufficiently_large_for C holds
    C c= UBD L~Span(C,n);

  theorem :: JORDAN14:14
   for C be Simple_closed_curve
   for n be Nat st n is_sufficiently_large_for C holds
    BDD L~Span(C,n) c= BDD C;

  theorem :: JORDAN14:15
   for C be Simple_closed_curve
   for n be Nat st n is_sufficiently_large_for C holds
    UBD C c= UBD L~Span(C,n);

  theorem :: JORDAN14:16
     for C be Simple_closed_curve
   for n be Nat st n is_sufficiently_large_for C holds
    RightComp Span(C,n) c= BDD C;

  theorem :: JORDAN14:17
   for C be Simple_closed_curve
   for n be Nat st n is_sufficiently_large_for C holds
    UBD C c= LeftComp Span(C,n);

  theorem :: JORDAN14:18
   for C be Simple_closed_curve
   for n be Nat st n is_sufficiently_large_for C holds
    UBD C misses BDD L~Span(C,n);

  theorem :: JORDAN14:19
     for C be Simple_closed_curve
   for n be Nat st n is_sufficiently_large_for C holds
    UBD C misses RightComp Span(C,n);

  theorem :: JORDAN14:20
   for C be Simple_closed_curve
   for P be Subset of TOP-REAL 2
   for n be Nat st n is_sufficiently_large_for C holds
    P is_outside_component_of C implies P misses L~Span(C,n);

  theorem :: JORDAN14:21
   for C be Simple_closed_curve
   for n be Nat st n is_sufficiently_large_for C holds
    UBD C misses L~Span(C,n);

  theorem :: JORDAN14:22
   for C be Simple_closed_curve
   for n be Nat st n is_sufficiently_large_for C holds
    L~Span(C,n) c= BDD C;

  theorem :: JORDAN14:23
   for C be Simple_closed_curve
   for i,j,k,n be Nat st
    n is_sufficiently_large_for C & 1 <= k & k <= len Span(C,n) &
     [i,j] in Indices Gauge(C,n) & Span(C,n)/.k = Gauge(C,n)*(i,j) holds
      i > 1;

  theorem :: JORDAN14:24
   for C be Simple_closed_curve
   for i,j,k,n be Nat st
    n is_sufficiently_large_for C & 1 <= k & k <= len Span(C,n) &
     [i,j] in Indices Gauge(C,n) & Span(C,n)/.k = Gauge(C,n)*(i,j) holds
      i < len Gauge(C,n);

  theorem :: JORDAN14:25
   for C be Simple_closed_curve
   for i,j,k,n be Nat st
    n is_sufficiently_large_for C & 1 <= k & k <= len Span(C,n) &
     [i,j] in Indices Gauge(C,n) & Span(C,n)/.k = Gauge(C,n)*(i,j) holds
      j > 1;

  theorem :: JORDAN14:26
   for C be Simple_closed_curve
   for i,j,k,n be Nat st
    n is_sufficiently_large_for C & 1 <= k & k <= len Span(C,n) &
     [i,j] in Indices Gauge(C,n) & Span(C,n)/.k = Gauge(C,n)*(i,j) holds
      j < width Gauge(C,n);

  theorem :: JORDAN14:27
     for C be Simple_closed_curve
   for n be Nat st n is_sufficiently_large_for C holds
    Y-SpanStart(C,n) < width Gauge(C,n);

  theorem :: JORDAN14:28
   for C be compact non vertical non horizontal Subset of TOP-REAL 2
   for n,m be Nat st m >= n & n >= 1 holds
    X-SpanStart(C,m) = 2|^(m-'n)*(X-SpanStart(C,n)-2)+2;

  theorem :: JORDAN14:29
   for C be compact non vertical non horizontal Subset of TOP-REAL 2
   for n,m be Nat st n <= m & n is_sufficiently_large_for C holds
    m is_sufficiently_large_for C;

  theorem :: JORDAN14:30
   for G be Go-board
   for f be FinSequence of TOP-REAL 2
   for i,j be Nat holds
    f is_sequence_on G & f is special & i <= len G & j <= width G implies
     cell(G,i,j)\L~f is connected;

  theorem :: JORDAN14:31
   for C be Simple_closed_curve
   for n,k be Nat st n is_sufficiently_large_for C & Y-SpanStart(C,n) <= k &
    k <= 2|^(n-'ApproxIndex C)*(Y-InitStart C-'2)+2 holds
     cell(Gauge(C,n),X-SpanStart(C,n)-'1,k)\L~Span(C,n) c= BDD L~Span(C,n);

  theorem :: JORDAN14:32
   for C be Subset of TOP-REAL 2
   for n,m,i be Nat st m <= n & 1 < i & i+1 < len Gauge(C,m) holds
    2|^(n-'m)*(i-2)+2+1 < len Gauge(C,n);

  theorem :: JORDAN14:33
   for C be Simple_closed_curve
   for n,m be Nat st n is_sufficiently_large_for C & n <= m holds
    RightComp Span(C,n) meets RightComp Span(C,m);

  theorem :: JORDAN14:34
   for G be Go-board
   for f be FinSequence of TOP-REAL 2 st f is_sequence_on G & f is special
   for i,j be Nat st i <= len G & j <= width G holds
    Int cell(G,i,j) c= (L~f)`;

  theorem :: JORDAN14:35
   for C be Simple_closed_curve
   for n,m be Nat st n is_sufficiently_large_for C & n <= m holds
    L~Span(C,m) c= Cl LeftComp(Span(C,n));

  theorem :: JORDAN14:36
   for C be Simple_closed_curve
   for n,m be Nat st n is_sufficiently_large_for C & n <= m holds
    RightComp(Span(C,n)) c= RightComp(Span(C,m));

  theorem :: JORDAN14:37
     for C be Simple_closed_curve
   for n,m be Nat st n is_sufficiently_large_for C & n <= m holds
    LeftComp(Span(C,m)) c= LeftComp(Span(C,n));