:: 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
cluster V21() 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 )
proof end;
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))
proof end;

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
proof end;

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
proof end;

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))
proof end;

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))
proof end;

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))
proof end;

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)))
proof end;

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))
proof end;

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))
proof end;

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))
proof end;

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))
proof end;

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)))
proof end;

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
proof end;

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)
proof end;
:: 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)
proof end;
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
proof end;
cluster BDD-Family C -> non empty ;
coherence
not BDD-Family C is empty
proof end;
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
proof end;

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)
proof end;

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))
proof end;

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))
proof end;

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))
proof end;

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))
proof end;

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
proof end;

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)
proof end;