The abstract of the Mizar article:

Properties of the External Approximation of Jordan's Curve

by

Artur Kornilowicz

Received June 24, 1999

MML identifier: JORDAN10

[ Mizar article, MML identifier index ]

environ

 vocabulary RELAT_2, COMPTS_1, SPPOL_1, EUCLID, TOPREAL1, FINSEQ_1, JORDAN9,
      MATRIX_1, JORDAN8, GOBOARD1, GOBOARD5, TREES_1, BOOLE, ARYTM_1, TARSKI,
      PSCOMP_1, ARYTM_3, GROUP_1, MCART_1, PRE_TOPC, GOBOARD9, TOPS_1,
      SUBSET_1, CONNSP_1, RELAT_1, JORDAN2C, LATTICES, CONNSP_3, SETFAM_1,
      TOPREAL4, PCOMPS_1, WEIERSTR, METRIC_1, JORDAN10, FINSEQ_4;
 notation TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, XREAL_0, REAL_1, NAT_1,
      BINARITH, STRUCT_0, METRIC_1, TBSP_1, FINSEQ_1, NEWTON, FINSEQ_4,
      WEIERSTR, PRE_TOPC, TOPS_1, CONNSP_1, CONNSP_3, COMPTS_1, PCOMPS_1,
      MATRIX_1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD5, TOPREAL4, PSCOMP_1,
      GOBOARD9, SPPOL_1, JORDAN2C, JORDAN8, GOBRD13, GOBRD14, JORDAN9;
 constructors BINARITH, CARD_4, CONNSP_1, CONNSP_3, FINSEQ_4, GOBOARD9,
      GOBRD13, GOBRD14, JORDAN2C, JORDAN8, JORDAN9, PSCOMP_1, REAL_1, REALSET1,
      TBSP_1, TOPREAL4, TOPS_1, WEIERSTR, JORDAN1;
 clusters XREAL_0, BORSUK_2, EUCLID, GOBRD14, JORDAN8, PCOMPS_1, PRE_TOPC,
      PSCOMP_1, RELSET_1, SPPOL_2, SPRECT_1, STRUCT_0, TOPREAL6, SUBSET_1,
      FINSEQ_1, ARYTM_3, SPRECT_4, JORDAN2C, MEMBERED;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin  :: Properties of the external approximation of Jordan's curve

definition
 cluster connected compact non vertical non horizontal Subset of TOP-REAL 2;
end;

reserve i, j, k, n for Nat,
   P for Subset of TOP-REAL 2,
   C for connected compact non vertical non horizontal Subset of TOP-REAL 2;

theorem :: JORDAN10:1
 1 <= k & k+1 <= len Cage(C,n) &
  [i,j] in Indices Gauge(C,n) & [i,j+1] in Indices Gauge(C,n) &
   Cage(C,n)/.k = Gauge(C,n)*(i,j) & Cage(C,n)/.(k+1) = Gauge(C,n)*(i,j+1)
 implies i < len Gauge(C,n);

theorem :: JORDAN10:2
 1 <= k & k+1 <= len Cage(C,n) &
  [i,j] in Indices Gauge(C,n) & [i,j+1] in Indices Gauge(C,n) &
   Cage(C,n)/.k = Gauge(C,n)*(i,j+1) & Cage(C,n)/.(k+1) = Gauge(C,n)*(i,j)
 implies i > 1;

theorem :: JORDAN10:3
 1 <= k & k+1 <= len Cage(C,n) &
  [i,j] in Indices Gauge(C,n) & [i+1,j] in Indices Gauge(C,n) &
   Cage(C,n)/.k = Gauge(C,n)*(i,j) & Cage(C,n)/.(k+1) = Gauge(C,n)*(i+1,j)
 implies j > 1;

theorem :: JORDAN10:4
 1 <= k & k+1 <= len Cage(C,n) &
  [i,j] in Indices Gauge(C,n) & [i+1,j] in Indices Gauge(C,n) &
   Cage(C,n)/.k = Gauge(C,n)*(i+1,j) & Cage(C,n)/.(k+1) = Gauge(C,n)*(i,j)
 implies j < width Gauge(C,n);

theorem :: JORDAN10:5
 C misses L~Cage(C,n);

theorem :: JORDAN10:6
 N-bound L~Cage(C,n) = N-bound C + (N-bound C - S-bound C)/(2|^n);

theorem :: JORDAN10:7
 i < j implies N-bound L~Cage(C,j) < N-bound L~Cage(C,i);

definition
 let C be connected compact non vertical non horizontal Subset of TOP-REAL 2,
     n be Nat;
 cluster Cl RightComp Cage(C,n) -> compact;
end;

theorem :: JORDAN10:8
 N-min C in RightComp Cage(C,n);

theorem :: JORDAN10:9
 C meets RightComp Cage (C,n);

theorem :: JORDAN10:10
 C misses LeftComp Cage(C,n);

theorem :: JORDAN10:11
 C c= RightComp Cage(C,n);

theorem :: JORDAN10:12
 C c= BDD L~Cage(C,n);

theorem :: JORDAN10:13
 UBD L~Cage(C,n) c= UBD C;

definition
  let C be compact non vertical non horizontal Subset of TOP-REAL 2;
 func UBD-Family C equals
:: JORDAN10:def 1
  { UBD L~Cage(C,n) where n is Nat : not contradiction };
 func BDD-Family C equals
:: JORDAN10:def 2
  { Cl BDD L~Cage(C,n) where n is Nat : not contradiction };
end;

definition
  let C be compact non vertical non horizontal Subset of TOP-REAL 2;
 redefine func UBD-Family C -> Subset-Family of TOP-REAL 2;
 redefine func BDD-Family C -> Subset-Family of TOP-REAL 2;
end;

definition
  let C be compact non vertical non horizontal Subset of TOP-REAL 2;
 cluster UBD-Family C -> non empty;
 cluster BDD-Family C -> non empty;
end;

theorem :: JORDAN10:14
 union UBD-Family C = UBD C;

theorem :: JORDAN10:15
 C c= meet BDD-Family C;

theorem :: JORDAN10:16
 BDD C misses LeftComp Cage(C,n);

theorem :: JORDAN10:17
 BDD C c= RightComp Cage(C,n);

theorem :: JORDAN10:18
 P is_inside_component_of C implies P misses L~Cage(C,n);

theorem :: JORDAN10:19
 BDD C misses L~Cage(C,n);

theorem :: JORDAN10:20
 COMPLEMENT UBD-Family C = BDD-Family C;

theorem :: JORDAN10:21
   meet BDD-Family C = C \/ BDD C;