:: Properties of the External Approximation of Jordan's Curve
:: by Artur Korni{\l}owicz
::
:: Copyright (c) 1999-2021 Association of Mizar Users

registration
cluster V23() connected compact non horizontal non vertical for Element of K16( the carrier of ());
existence
ex b1 being Subset of () st
( b1 is connected & b1 is compact & not b1 is vertical & not b1 is horizontal )
proof end;
end;

theorem Th1: :: JORDAN10:1
for i, j, k, n being Nat
for C being connected compact non horizontal non vertical Subset of () 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 i, j, k, n being Nat
for C being connected compact non horizontal non vertical Subset of () 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 i, j, k, n being Nat
for C being connected compact non horizontal non vertical Subset of () 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 i, j, k, n being Nat
for C being connected compact non horizontal non vertical Subset of () 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 Nat
for C being connected compact non horizontal non vertical Subset of () holds C misses L~ (Cage (C,n))
proof end;

theorem Th6: :: JORDAN10:6
for n being Nat
for C being connected compact non horizontal non vertical Subset of () holds N-bound (L~ (Cage (C,n))) = () + ((() - ()) / (2 |^ n))
proof end;

theorem Th7: :: JORDAN10:7
for i, j being Nat
for C being connected compact non horizontal non vertical Subset of () 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 ();
let n be 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 Nat
for C being connected compact non horizontal non vertical Subset of () holds N-min C in RightComp (Cage (C,n))
proof end;

theorem Th9: :: JORDAN10:9
for n being Nat
for C being connected compact non horizontal non vertical Subset of () holds C meets RightComp (Cage (C,n))
proof end;

theorem Th10: :: JORDAN10:10
for n being Nat
for C being connected compact non horizontal non vertical Subset of () holds C misses LeftComp (Cage (C,n))
proof end;

theorem Th11: :: JORDAN10:11
for n being Nat
for C being connected compact non horizontal non vertical Subset of () holds C c= RightComp (Cage (C,n))
proof end;

theorem Th12: :: JORDAN10:12
for n being Nat
for C being connected compact non horizontal non vertical Subset of () holds C c= BDD (L~ (Cage (C,n)))
proof end;

theorem Th13: :: JORDAN10:13
for n being Nat
for C being connected compact non horizontal non vertical Subset of () holds UBD (L~ (Cage (C,n))) c= UBD C
proof end;

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

:: deftheorem defines UBD-Family JORDAN10:def 1 :
for C being compact non horizontal non vertical Subset of () holds UBD-Family C = { (UBD (L~ (Cage (C,n)))) where n is Nat : verum } ;

:: deftheorem defines BDD-Family JORDAN10:def 2 :
for C being compact non horizontal non vertical Subset of () holds BDD-Family C = { (Cl (BDD (L~ (Cage (C,n))))) where n is Nat : verum } ;

definition
let C be compact non horizontal non vertical Subset of ();
:: original: UBD-Family
redefine func UBD-Family C -> Subset-Family of ();
coherence
UBD-Family C is Subset-Family of ()
proof end;
:: original: BDD-Family
redefine func BDD-Family C -> Subset-Family of ();
coherence
BDD-Family C is Subset-Family of ()
proof end;
end;

registration
let C be compact non horizontal non vertical Subset of ();
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 () holds union () = UBD C
proof end;

theorem Th15: :: JORDAN10:15
for C being connected compact non horizontal non vertical Subset of () holds C c= meet ()
proof end;

theorem Th16: :: JORDAN10:16
for n being Nat
for C being connected compact non horizontal non vertical Subset of () holds BDD C misses LeftComp (Cage (C,n))
proof end;

theorem Th17: :: JORDAN10:17
for n being Nat
for C being connected compact non horizontal non vertical Subset of () holds BDD C c= RightComp (Cage (C,n))
proof end;

theorem Th18: :: JORDAN10:18
for n being Nat
for P being Subset of ()
for C being connected compact non horizontal non vertical Subset of () st P is_inside_component_of C holds
P misses L~ (Cage (C,n))
proof end;

theorem Th19: :: JORDAN10:19
for n being Nat
for C being connected compact non horizontal non vertical Subset of () 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 () holds COMPLEMENT () = BDD-Family C
proof end;

theorem :: JORDAN10:21
for C being connected compact non horizontal non vertical Subset of () holds meet () = C \/ (BDD C)
proof end;