:: 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 b₁, b₂, b₃, b₄ being Nat
for b₅ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= b₁ & b₁ + 1 <= len (Cage b₅,b₂) & [b₃,b₄] in Indices (Gauge b₅,b₂) & [b₃,(b₄ + 1)] in Indices (Gauge b₅,b₂) & (Cage b₅,b₂) /. b₁ = (Gauge b₅,b₂) * b₃,b₄ & (Cage b₅,b₂) /. (b₁ + 1) = (Gauge b₅,b₂) * b₃,(b₄ + 1) holds
b₃ < len (Gauge b₅,b₂)

proof end;

theorem Th2: :: JORDAN10:2

for b₁, b₂, b₃, b₄ being Nat
for b₅ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= b₁ & b₁ + 1 <= len (Cage b₅,b₂) & [b₃,b₄] in Indices (Gauge b₅,b₂) & [b₃,(b₄ + 1)] in Indices (Gauge b₅,b₂) & (Cage b₅,b₂) /. b₁ = (Gauge b₅,b₂) * b₃,(b₄ + 1) & (Cage b₅,b₂) /. (b₁ + 1) = (Gauge b₅,b₂) * b₃,b₄ holds
b₃ > 1

proof end;

theorem Th3: :: JORDAN10:3

for b₁, b₂, b₃, b₄ being Nat
for b₅ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= b₁ & b₁ + 1 <= len (Cage b₅,b₂) & [b₃,b₄] in Indices (Gauge b₅,b₂) & [(b₃ + 1),b₄] in Indices (Gauge b₅,b₂) & (Cage b₅,b₂) /. b₁ = (Gauge b₅,b₂) * b₃,b₄ & (Cage b₅,b₂) /. (b₁ + 1) = (Gauge b₅,b₂) * (b₃ + 1),b₄ holds
b₄ > 1

proof end;

theorem Th4: :: JORDAN10:4

for b₁, b₂, b₃, b₄ being Nat
for b₅ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= b₁ & b₁ + 1 <= len (Cage b₅,b₂) & [b₃,b₄] in Indices (Gauge b₅,b₂) & [(b₃ + 1),b₄] in Indices (Gauge b₅,b₂) & (Cage b₅,b₂) /. b₁ = (Gauge b₅,b₂) * (b₃ + 1),b₄ & (Cage b₅,b₂) /. (b₁ + 1) = (Gauge b₅,b₂) * b₃,b₄ holds
b₄ < width (Gauge b₅,b₂)

proof end;

theorem Th5: :: JORDAN10:5

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds b₂ misses L~ (Cage b₂,b₁)

proof end;

theorem Th6: :: JORDAN10:6

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds N-bound (L~ (Cage b₂,b₁)) = (N-bound b₂) + (((N-bound b₂) - (S-bound b₂)) / (2 |^ b₁))

proof end;

theorem Th7: :: JORDAN10:7

for b₁, b₂ being Nat
for b₃ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st b₁ < b₂ holds
N-bound (L~ (Cage b₃,b₂)) < N-bound (L~ (Cage b₃,b₁))

proof end;

registration

let c₁ be connected compact non horizontal non vertical Subset of (TOP-REAL 2);
let c₂ be Nat;
cluster Cl (RightComp (Cage a₁,a₂)) -> compact ;
coherence by GOBRD14:42;

end;

theorem Th8: :: JORDAN10:8

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds N-min b₂ in RightComp (Cage b₂,b₁)

proof end;

theorem Th9: :: JORDAN10:9

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds b₂ meets RightComp (Cage b₂,b₁)

proof end;

theorem Th10: :: JORDAN10:10

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds b₂ misses LeftComp (Cage b₂,b₁)

proof end;

theorem Th11: :: JORDAN10:11

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds b₂ c= RightComp (Cage b₂,b₁)

proof end;

theorem Th12: :: JORDAN10:12

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds b₂ c= BDD (L~ (Cage b₂,b₁))

proof end;

theorem Th13: :: JORDAN10:13

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds UBD (L~ (Cage b₂,b₁)) c= UBD b₂

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

end;

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

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

definition

let c₁ be compact non horizontal non vertical Subset of (TOP-REAL 2);
redefine func UBD-Family as UBD-Family c₁ -> Subset-Family of (TOP-REAL 2);
coherence

proof end;

redefine func BDD-Family as 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 a₁ -> non empty ;
coherence

proof end;

cluster BDD-Family a₁ -> non empty ;
coherence

proof end;

end;

theorem Th14: :: JORDAN10:14

for b₁ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds union (UBD-Family b₁) = UBD b₁

proof end;

theorem Th15: :: JORDAN10:15

for b₁ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds b₁ c= meet (BDD-Family b₁)

proof end;

theorem Th16: :: JORDAN10:16

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD b₂ misses LeftComp (Cage b₂,b₁)

proof end;

theorem Th17: :: JORDAN10:17

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD b₂ c= RightComp (Cage b₂,b₁)

proof end;

theorem Th18: :: JORDAN10:18

for b₁ being Nat
for b₂ being Subset of (TOP-REAL 2)
for b₃ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st b₂ is_inside_component_of b₃ holds
b₂ misses L~ (Cage b₃,b₁)

proof end;

theorem Th19: :: JORDAN10:19

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD b₂ misses L~ (Cage b₂,b₁)

proof end;

theorem Th20: :: JORDAN10:20

for b₁ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds COMPLEMENT (UBD-Family b₁) = BDD-Family b₁

proof end;

theorem Th21: :: JORDAN10:21

for b₁ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds meet (BDD-Family b₁) = b₁ \/ (BDD b₁)

proof end;