:: Properties of the External Approximation of Jordan's Curve :: by Artur Korni{\l}owicz :: :: Received June 24, 1999 :: Copyright (c) 1999-2012 Association of Mizar Users begin registration clusterV21() connected compact non horizontal non vertical for Element of K6( the carrier of (TOP-REAL 2)); existence ex b1 being Subset of (TOP-REAL 2) st ( b1 is connected & b1 is compact & not b1 is vertical & not b1 is horizontal ) proofend; end; theorem Th1: :: JORDAN10:1 for k, n, i, j being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 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)) holds i < len (Gauge (C,n)) proofend; theorem Th2: :: JORDAN10:2 for k, n, i, j being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 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) holds i > 1 proofend; theorem Th3: :: JORDAN10:3 for k, n, i, j being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 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) holds j > 1 proofend; theorem Th4: :: JORDAN10:4 for k, n, i, j being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 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) holds j < width (Gauge (C,n)) proofend; theorem Th5: :: JORDAN10:5 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C misses L~ (Cage (C,n)) proofend; theorem Th6: :: JORDAN10:6 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds N-bound (L~ (Cage (C,n))) = (N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n)) proofend; theorem Th7: :: JORDAN10:7 for i, j being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st i < j holds N-bound (L~ (Cage (C,j))) < N-bound (L~ (Cage (C,i))) proofend; registration let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); let n be Element of NAT ; cluster Cl (RightComp (Cage (C,n))) -> compact ; coherence Cl (RightComp (Cage (C,n))) is compact by GOBRD14:32; end; theorem Th8: :: JORDAN10:8 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds N-min C in RightComp (Cage (C,n)) proofend; theorem Th9: :: JORDAN10:9 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C meets RightComp (Cage (C,n)) proofend; theorem Th10: :: JORDAN10:10 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C misses LeftComp (Cage (C,n)) proofend; theorem Th11: :: JORDAN10:11 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C c= RightComp (Cage (C,n)) proofend; theorem Th12: :: JORDAN10:12 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C c= BDD (L~ (Cage (C,n))) proofend; theorem Th13: :: JORDAN10:13 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds UBD (L~ (Cage (C,n))) c= UBD C proofend; definition let C be compact non horizontal non vertical Subset of (TOP-REAL 2); func UBD-Family C -> set equals :: JORDAN10:def 1 { (UBD (L~ (Cage (C,n)))) where n is Element of NAT : verum } ; coherence { (UBD (L~ (Cage (C,n)))) where n is Element of NAT : verum } is set ; func BDD-Family C -> set equals :: JORDAN10:def 2 { (Cl (BDD (L~ (Cage (C,n))))) where n is Element of NAT : verum } ; coherence { (Cl (BDD (L~ (Cage (C,n))))) where n is Element of NAT : verum } is set ; end; :: deftheorem defines UBD-Family JORDAN10:def_1_:_ for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds UBD-Family C = { (UBD (L~ (Cage (C,n)))) where n is Element of NAT : verum } ; :: deftheorem defines BDD-Family JORDAN10:def_2_:_ for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD-Family C = { (Cl (BDD (L~ (Cage (C,n))))) where n is Element of NAT : verum } ; definition let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: original:UBD-Family redefine func UBD-Family C -> Subset-Family of (TOP-REAL 2); coherence UBD-Family C is Subset-Family of (TOP-REAL 2) proofend; :: original:BDD-Family redefine func BDD-Family C -> Subset-Family of (TOP-REAL 2); coherence BDD-Family C is Subset-Family of (TOP-REAL 2) proofend; end; registration let C be compact non horizontal non vertical Subset of (TOP-REAL 2); cluster UBD-Family C -> non empty ; coherence not UBD-Family C is empty proofend; cluster BDD-Family C -> non empty ; coherence not BDD-Family C is empty proofend; end; theorem Th14: :: JORDAN10:14 for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds union (UBD-Family C) = UBD C proofend; theorem Th15: :: JORDAN10:15 for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C c= meet (BDD-Family C) proofend; theorem Th16: :: JORDAN10:16 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD C misses LeftComp (Cage (C,n)) proofend; theorem Th17: :: JORDAN10:17 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD C c= RightComp (Cage (C,n)) proofend; theorem Th18: :: JORDAN10:18 for n being Element of NAT for P being Subset of (TOP-REAL 2) for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st P is_inside_component_of C holds P misses L~ (Cage (C,n)) proofend; theorem Th19: :: JORDAN10:19 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD C misses L~ (Cage (C,n)) proofend; theorem Th20: :: JORDAN10:20 for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds COMPLEMENT (UBD-Family C) = BDD-Family C proofend; theorem :: JORDAN10:21 for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds meet (BDD-Family C) = C \/ (BDD C) proofend;