:: JORDAN1B semantic presentation

registration

cluster -> non horizontal non vertical Element of K40(the carrier of (TOP-REAL 2));
coherence

proof end;

end;

registration

let c₁ be non empty TopSpace;
cluster non empty a_union_of_components of a₁;
existence

proof end;

end;

theorem Th1: :: JORDAN1B:1

for b₁ being non empty TopSpace
for b₂ being non empty a_union_of_components of b₁ st b₂ is connected holds
b₂ is_a_component_of b₁

proof end;

theorem Th2: :: JORDAN1B:2

for b₁ being FinSequence holds
( b₁ is empty iff Rev b₁ is empty )

proof end;

theorem Th3: :: JORDAN1B:3

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃, b₄ being Nat st 1 <= b₃ & b₃ <= len b₂ & 1 <= b₄ & b₄ <= len b₂ holds
not mid b₂,b₃,b₄ is empty

proof end;

theorem Th4: :: JORDAN1B:4

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st 1 <= len b₁ & b₂ in L~ b₁ holds
(R_Cut b₁,b₂) . 1 = b₁ . 1

proof end;

theorem Th5: :: JORDAN1B:5

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₁ is_S-Seq & b₂ in L~ b₁ holds
(L_Cut b₁,b₂) . (len (L_Cut b₁,b₂)) = b₁ . (len b₁)

proof end;

theorem Th6: :: JORDAN1B:6

for b₁ being Simple_closed_curve holds W-max b₁ <> E-max b₁

proof end;

theorem Th7: :: JORDAN1B:7

for b₁ being Nat
for b₂ being non empty set
for b₃ being FinSequence of b₂ st 1 <= b₁ & b₁ < len b₃ holds
(mid b₃,b₁,((len b₃) -' 1)) ^ <*(b₃ /. (len b₃))*> = mid b₃,b₁,(len b₃)

proof end;

theorem Th8: :: JORDAN1B:8

for b₁, b₂ being Point of (TOP-REAL 2) st b₁ <> b₂ & LSeg b₁,b₂ is vertical holds
<*b₁,b₂*> is_S-Seq

proof end;

theorem Th9: :: JORDAN1B:9

for b₁, b₂ being Point of (TOP-REAL 2) st b₁ <> b₂ & LSeg b₁,b₂ is horizontal holds
<*b₁,b₂*> is_S-Seq

proof end;

theorem Th10: :: JORDAN1B:10

for b₁, b₂ being FinSequence of (TOP-REAL 2)
for b₃ being Point of (TOP-REAL 2) st b₁ is_in_the_area_of b₂ holds
Rotate b₁,b₃ is_in_the_area_of b₂

proof end;

theorem Th11: :: JORDAN1B:11

for b₁ being non trivial FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) holds Rotate b₁,b₂ is_in_the_area_of b₁

proof end;

theorem Th12: :: JORDAN1B:12

for b₁ being FinSequence holds Center b₁ >= 1

proof end;

theorem Th13: :: JORDAN1B:13

for b₁ being FinSequence st len b₁ >= 1 holds
Center b₁ <= len b₁

proof end;

theorem Th14: :: JORDAN1B:14

for b₁ being Go-board holds Center b₁ <= len b₁

proof end;

theorem Th15: :: JORDAN1B:15

for b₁ being FinSequence st len b₁ >= 2 holds
Center b₁ > 1

proof end;

theorem Th16: :: JORDAN1B:16

for b₁ being FinSequence st len b₁ >= 3 holds
Center b₁ < len b₁

proof end;

E7: now

let c₁ be non empty Subset of (TOP-REAL 2);
thus (len (Gauge c₁,0)) -' 1 = ((2 |^ 0) + 3) -' 1 by JORDAN8:def 1
.= (1 + 3) -' 1 by NEWTON:9
.= 3 by BINARITH:39 ;

end;

theorem Th17: :: JORDAN1B:17

for b₁ being compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₂ being Nat holds Center (Gauge b₁,b₂) = (2 |^ (b₂ -' 1)) + 2

proof end;

theorem Th18: :: JORDAN1B:18

for b₁ being compact non horizontal non vertical Subset of (TOP-REAL 2) holds b₁ c= cell (Gauge b₁,0),2,2

proof end;

theorem Th19: :: JORDAN1B:19

for b₁ being compact non horizontal non vertical Subset of (TOP-REAL 2) holds not cell (Gauge b₁,0),2,2 c= BDD b₁

proof end;

theorem Th20: :: JORDAN1B:20

for b₁ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (Gauge b₁,1) * (Center (Gauge b₁,1)),1 = |[(((W-bound b₁) + (E-bound b₁)) / 2),(S-bound (L~ (Cage b₁,1)))]|

proof end;

theorem Th21: :: JORDAN1B:21

for b₁ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (Gauge b₁,1) * (Center (Gauge b₁,1)),(len (Gauge b₁,1)) = |[(((W-bound b₁) + (E-bound b₁)) / 2),(N-bound (L~ (Cage b₁,1)))]|

proof end;

Lemma10: for b₁, b₂ being Nat st b₁ <= b₂ & b₂ <= b₁ + 1 & not b₁ = b₂ holds
b₁ = b₂ -' 1

proof end;

theorem Th22: :: JORDAN1B:22

for b₁ being Go-board
for b₂, b₃, b₄ being Nat
for b₅ being Point of (TOP-REAL 2) st 1 <= b₂ & b₂ < width b₁ & 1 <= b₃ & b₃ <= len b₁ & 1 <= b₄ & b₄ <= width b₁ & b₅ in cell b₁,(len b₁),b₂ & b₅ `1 = (b₁ * b₃,b₄) `1 holds
len b₁ = b₃

proof end;

theorem Th23: :: JORDAN1B:23

for b₁ being Go-board
for b₂, b₃, b₄, b₅ being Nat
for b₆ being Point of (TOP-REAL 2) st 1 <= b₂ & b₂ <= len b₁ & 1 <= b₃ & b₃ < width b₁ & 1 <= b₄ & b₄ <= len b₁ & 1 <= b₅ & b₅ <= width b₁ & b₆ in cell b₁,b₂,b₃ & b₆ `1 = (b₁ * b₄,b₅) `1 & not b₂ = b₄ holds
b₂ = b₄ -' 1

proof end;

theorem Th24: :: JORDAN1B:24

for b₁ being Go-board
for b₂, b₃, b₄ being Nat
for b₅ being Point of (TOP-REAL 2) st 1 <= b₂ & b₂ < len b₁ & 1 <= b₃ & b₃ <= len b₁ & 1 <= b₄ & b₄ <= width b₁ & b₅ in cell b₁,b₂,(width b₁) & b₅ `2 = (b₁ * b₃,b₄) `2 holds
width b₁ = b₄

proof end;

theorem Th25: :: JORDAN1B:25

for b₁ being Go-board
for b₂, b₃, b₄, b₅ being Nat
for b₆ being Point of (TOP-REAL 2) st 1 <= b₂ & b₂ < len b₁ & 1 <= b₃ & b₃ <= width b₁ & 1 <= b₄ & b₄ <= len b₁ & 1 <= b₅ & b₅ <= width b₁ & b₆ in cell b₁,b₂,b₃ & b₆ `2 = (b₁ * b₄,b₅) `2 & not b₃ = b₅ holds
b₃ = b₅ -' 1

proof end;

theorem Th26: :: JORDAN1B:26

for b₁ being Simple_closed_curve
for b₂ being real number st W-bound b₁ <= b₂ & b₂ <= E-bound b₁ holds
LSeg |[b₂,(S-bound b₁)]|,|[b₂,(N-bound b₁)]| meets Upper_Arc b₁

proof end;

theorem Th27: :: JORDAN1B:27

for b₁ being Simple_closed_curve
for b₂ being real number st W-bound b₁ <= b₂ & b₂ <= E-bound b₁ holds
LSeg |[b₂,(S-bound b₁)]|,|[b₂,(N-bound b₁)]| meets Lower_Arc b₁

proof end;

theorem Th28: :: JORDAN1B:28

for b₁ being Nat
for b₂ being Simple_closed_curve
for b₃ being Nat st 1 < b₃ & b₃ < len (Gauge b₂,b₁) holds
LSeg ((Gauge b₂,b₁) * b₃,1),((Gauge b₂,b₁) * b₃,(len (Gauge b₂,b₁))) meets Upper_Arc b₂

proof end;

theorem Th29: :: JORDAN1B:29

for b₁ being Nat
for b₂ being Simple_closed_curve
for b₃ being Nat st 1 < b₃ & b₃ < len (Gauge b₂,b₁) holds
LSeg ((Gauge b₂,b₁) * b₃,1),((Gauge b₂,b₁) * b₃,(len (Gauge b₂,b₁))) meets Lower_Arc b₂

proof end;

theorem Th30: :: JORDAN1B:30

for b₁ being Nat
for b₂ being Simple_closed_curve holds LSeg ((Gauge b₂,b₁) * (Center (Gauge b₂,b₁)),1),((Gauge b₂,b₁) * (Center (Gauge b₂,b₁)),(len (Gauge b₂,b₁))) meets Upper_Arc b₂

proof end;

theorem Th31: :: JORDAN1B:31

for b₁ being Nat
for b₂ being Simple_closed_curve holds LSeg ((Gauge b₂,b₁) * (Center (Gauge b₂,b₁)),1),((Gauge b₂,b₁) * (Center (Gauge b₂,b₁)),(len (Gauge b₂,b₁))) meets Lower_Arc b₂

proof end;

theorem Th32: :: JORDAN1B:32

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₃ being Nat st 1 <= b₃ & b₃ <= len (Gauge b₂,b₁) holds
LSeg ((Gauge b₂,b₁) * b₃,1),((Gauge b₂,b₁) * b₃,(len (Gauge b₂,b₁))) meets Upper_Arc (L~ (Cage b₂,b₁))

proof end;

theorem Th33: :: JORDAN1B:33

proof end;

theorem Th34: :: JORDAN1B:34

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds LSeg ((Gauge b₂,b₁) * (Center (Gauge b₂,b₁)),1),((Gauge b₂,b₁) * (Center (Gauge b₂,b₁)),(len (Gauge b₂,b₁))) meets Upper_Arc (L~ (Cage b₂,b₁))

proof end;

theorem Th35: :: JORDAN1B:35

proof end;

theorem Th36: :: JORDAN1B:36

for b₁ being Go-board
for b₂ being Nat st b₂ <= width b₁ holds
not cell b₁,0,b₂ is Bounded

proof end;

theorem Th37: :: JORDAN1B:37

for b₁ being Go-board
for b₂ being Nat st b₂ <= width b₁ holds
not cell b₁,(len b₁),b₂ is Bounded

proof end;

theorem Th38: :: JORDAN1B:38

for b₁ being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₂, b₃ being Nat st b₂ <= width (Gauge b₁,b₃) holds
cell (Gauge b₁,b₃),0,b₂ c= UBD b₁

proof end;

theorem Th39: :: JORDAN1B:39

for b₁ being compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₂, b₃ being Nat st b₂ <= len (Gauge b₁,b₃) holds
cell (Gauge b₁,b₃),(len (Gauge b₁,b₃)),b₂ c= UBD b₁

proof end;

Lemma23: for b₁ being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₂, b₃, b₄ being Nat st b₂ <= width (Gauge b₁,b₃) & cell (Gauge b₁,b₃),b₄,b₂ c= BDD b₁ holds
b₄ <> 0

proof end;

Lemma24: for b₁ being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₂, b₃, b₄ being Nat st b₂ <= len (Gauge b₁,b₃) & cell (Gauge b₁,b₃),b₂,b₄ c= BDD b₁ holds
b₄ <> 0

proof end;

Lemma25: for b₁ being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₂, b₃, b₄ being Nat st b₂ <= width (Gauge b₁,b₃) & cell (Gauge b₁,b₃),b₄,b₂ c= BDD b₁ holds
b₄ <> len (Gauge b₁,b₃)

proof end;

Lemma26: for b₁ being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₂, b₃, b₄ being Nat st b₂ <= len (Gauge b₁,b₃) & cell (Gauge b₁,b₃),b₂,b₄ c= BDD b₁ holds
b₄ <> width (Gauge b₁,b₃)

proof end;

theorem Th40: :: JORDAN1B:40

for b₁ being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₂, b₃, b₄ being Nat st b₂ <= len (Gauge b₁,b₃) & b₄ <= width (Gauge b₁,b₃) & cell (Gauge b₁,b₃),b₂,b₄ c= BDD b₁ holds
b₄ > 1

proof end;

theorem Th41: :: JORDAN1B:41

proof end;

theorem Th42: :: JORDAN1B:42

proof end;

theorem Th43: :: JORDAN1B:43

proof end;

theorem Th44: :: JORDAN1B:44

for b₁ being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₂ being Nat st ex b₃, b₄ being Nat st
( b₃ <= len (Gauge b₁,b₂) & b₄ <= width (Gauge b₁,b₂) & cell (Gauge b₁,b₂),b₃,b₄ c= BDD b₁ ) holds
b₂ >= 1

proof end;