:: JORDAN10 semantic presentation

registration

cluster connected compact non horizontal non vertical Element of K40(the carrier of (TOP-REAL 2));
existence

proof end;

end;

theorem Th1: :: JORDAN10:1

for k, n, i, j 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 k, n, i, j 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 k, n, i, j 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 k, n, i, j 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 by GOBRD14:42;

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 ;
func BDD-Family C -> set equals :: JORDAN10:def 2
{ (Cl (BDD (L~ (Cage C,n)))) where n is Nat : verum } ;
coherence ;

end;

:: deftheorem defines UBD-Family JORDAN10:def 1 :

:: deftheorem defines BDD-Family JORDAN10:def 2 :

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

proof end;

:: original: BDD-Family
redefine func BDD-Family C -> Subset-Family of (TOP-REAL 2);
coherence

proof end;

end;

registration

let C be compact non horizontal non vertical Subset of (TOP-REAL 2);
cluster UBD-Family C -> non empty ;
coherence

proof end;

cluster BDD-Family C -> non empty ;
coherence

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;