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

registration

cluster V23() connected compact non horizontal non vertical for Element of K16( the carrier of (TOP-REAL 2));

existence
ex b₁ being Subset of (TOP-REAL 2) st
( b₁ is connected & b₁ is compact & not b₁ is vertical & not b₁ 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 (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 i, j, k, n being 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 i, j, k, n being 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 i, j, k, n being 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 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 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 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 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (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 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (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 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 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 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 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;