:: JORDAN14 semantic presentation

theorem Th1: :: JORDAN14:1

for b₁ being non constant standard special_circular_sequence holds
( BDD (L~ b₁) = RightComp b₁ or BDD (L~ b₁) = LeftComp b₁ )

proof end;

theorem Th2: :: JORDAN14:2

for b₁ being non constant standard special_circular_sequence holds
( UBD (L~ b₁) = RightComp b₁ or UBD (L~ b₁) = LeftComp b₁ )

proof end;

theorem Th3: :: JORDAN14:3

for b₁ being Go-board
for b₂ being FinSequence of (TOP-REAL 2)
for b₃ being Nat st 1 <= b₃ & b₃ + 1 <= len b₂ & b₂ is_sequence_on b₁ holds
left_cell b₂,b₃,b₁ is closed

proof end;

theorem Th4: :: JORDAN14:4

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

proof end;

theorem Th5: :: JORDAN14:5

for b₁ being non constant standard special_circular_sequence holds BDD (L~ b₁) is connected

proof end;

registration

let c₁ be non constant standard special_circular_sequence;
cluster BDD (L~ a₁) -> connected ;
coherence by Th5;

end;

definition

let c₁ be Simple_closed_curve;
let c₂ be Nat;
func SpanStart c₁,c₂ -> Point of (TOP-REAL 2) equals :: JORDAN14:def 1
(Gauge a₁,a₂) * (X-SpanStart a₁,a₂),(Y-SpanStart a₁,a₂);
coherence ;

end;

:: deftheorem Def1 defines SpanStart JORDAN14:def 1 :

theorem Th6: :: JORDAN14:6

for b₁ being Simple_closed_curve
for b₂ being Nat st b₂ is_sufficiently_large_for b₁ holds
(Span b₁,b₂) /. 1 = SpanStart b₁,b₂ by JORDAN13:def 1;

theorem Th7: :: JORDAN14:7

for b₁ being Simple_closed_curve
for b₂ being Nat st b₂ is_sufficiently_large_for b₁ holds
SpanStart b₁,b₂ in BDD b₁

proof end;

theorem Th8: :: JORDAN14:8

for b₁ being Simple_closed_curve
for b₂, b₃ being Nat st b₂ is_sufficiently_large_for b₁ & 1 <= b₃ & b₃ + 1 <= len (Span b₁,b₂) holds
( right_cell (Span b₁,b₂),b₃,(Gauge b₁,b₂) misses b₁ & left_cell (Span b₁,b₂),b₃,(Gauge b₁,b₂) meets b₁ )

proof end;

theorem Th9: :: JORDAN14:9

for b₁ being Simple_closed_curve
for b₂ being Nat st b₂ is_sufficiently_large_for b₁ holds
b₁ misses L~ (Span b₁,b₂)

proof end;

registration

let c₁ be Simple_closed_curve;
let c₂ be Nat;
cluster Cl (RightComp (Span a₁,a₂)) -> compact ;
coherence by GOBRD14:42;

end;

theorem Th10: :: JORDAN14:10

for b₁ being Simple_closed_curve
for b₂ being Nat st b₂ is_sufficiently_large_for b₁ holds
b₁ meets LeftComp (Span b₁,b₂)

proof end;

theorem Th11: :: JORDAN14:11

for b₁ being Simple_closed_curve
for b₂ being Nat st b₂ is_sufficiently_large_for b₁ holds
b₁ misses RightComp (Span b₁,b₂)

proof end;

theorem Th12: :: JORDAN14:12

for b₁ being Simple_closed_curve
for b₂ being Nat st b₂ is_sufficiently_large_for b₁ holds
b₁ c= LeftComp (Span b₁,b₂)

proof end;

theorem Th13: :: JORDAN14:13

for b₁ being Simple_closed_curve
for b₂ being Nat st b₂ is_sufficiently_large_for b₁ holds
b₁ c= UBD (L~ (Span b₁,b₂))

proof end;

theorem Th14: :: JORDAN14:14

for b₁ being Simple_closed_curve
for b₂ being Nat st b₂ is_sufficiently_large_for b₁ holds
BDD (L~ (Span b₁,b₂)) c= BDD b₁

proof end;

theorem Th15: :: JORDAN14:15

for b₁ being Simple_closed_curve
for b₂ being Nat st b₂ is_sufficiently_large_for b₁ holds
UBD b₁ c= UBD (L~ (Span b₁,b₂))

proof end;

theorem Th16: :: JORDAN14:16

for b₁ being Simple_closed_curve
for b₂ being Nat st b₂ is_sufficiently_large_for b₁ holds
RightComp (Span b₁,b₂) c= BDD b₁

proof end;

theorem Th17: :: JORDAN14:17

for b₁ being Simple_closed_curve
for b₂ being Nat st b₂ is_sufficiently_large_for b₁ holds
UBD b₁ c= LeftComp (Span b₁,b₂)

proof end;

theorem Th18: :: JORDAN14:18

for b₁ being Simple_closed_curve
for b₂ being Nat st b₂ is_sufficiently_large_for b₁ holds
UBD b₁ misses BDD (L~ (Span b₁,b₂))

proof end;

theorem Th19: :: JORDAN14:19

for b₁ being Simple_closed_curve
for b₂ being Nat st b₂ is_sufficiently_large_for b₁ holds
UBD b₁ misses RightComp (Span b₁,b₂)

proof end;

theorem Th20: :: JORDAN14:20

for b₁ being Simple_closed_curve
for b₂ being Subset of (TOP-REAL 2)
for b₃ being Nat st b₃ is_sufficiently_large_for b₁ & b₂ is_outside_component_of b₁ holds
b₂ misses L~ (Span b₁,b₃)

proof end;

theorem Th21: :: JORDAN14:21

for b₁ being Simple_closed_curve
for b₂ being Nat st b₂ is_sufficiently_large_for b₁ holds
UBD b₁ misses L~ (Span b₁,b₂)

proof end;

theorem Th22: :: JORDAN14:22

for b₁ being Simple_closed_curve
for b₂ being Nat st b₂ is_sufficiently_large_for b₁ holds
L~ (Span b₁,b₂) c= BDD b₁

proof end;

theorem Th23: :: JORDAN14:23

for b₁ being Simple_closed_curve
for b₂, b₃, b₄, b₅ being Nat st b₅ is_sufficiently_large_for b₁ & 1 <= b₄ & b₄ <= len (Span b₁,b₅) & [b₂,b₃] in Indices (Gauge b₁,b₅) & (Span b₁,b₅) /. b₄ = (Gauge b₁,b₅) * b₂,b₃ holds
b₂ > 1

proof end;

theorem Th24: :: JORDAN14:24

proof end;

theorem Th25: :: JORDAN14:25

proof end;

theorem Th26: :: JORDAN14:26

proof end;

theorem Th27: :: JORDAN14:27

for b₁ being Simple_closed_curve
for b₂ being Nat st b₂ is_sufficiently_large_for b₁ holds
Y-SpanStart b₁,b₂ < width (Gauge b₁,b₂)

proof end;

theorem Th28: :: JORDAN14:28

for b₁ being compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₂, b₃ being Nat st b₃ >= b₂ & b₂ >= 1 holds
X-SpanStart b₁,b₃ = ((2 |^ (b₃ -' b₂)) * ((X-SpanStart b₁,b₂) - 2)) + 2

proof end;

theorem Th29: :: JORDAN14:29

for b₁ being compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₂, b₃ being Nat st b₂ <= b₃ & b₂ is_sufficiently_large_for b₁ holds
b₃ is_sufficiently_large_for b₁

proof end;

theorem Th30: :: JORDAN14:30

for b₁ being Go-board
for b₂ being FinSequence of (TOP-REAL 2)
for b₃, b₄ being Nat st b₂ is_sequence_on b₁ & b₂ is special & b₃ <= len b₁ & b₄ <= width b₁ holds
(cell b₁,b₃,b₄) \ (L~ b₂) is connected

proof end;

theorem Th31: :: JORDAN14:31

for b₁ being Simple_closed_curve
for b₂, b₃ being Nat st b₂ is_sufficiently_large_for b₁ & Y-SpanStart b₁,b₂ <= b₃ & b₃ <= ((2 |^ (b₂ -' (ApproxIndex b₁))) * ((Y-InitStart b₁) -' 2)) + 2 holds
(cell (Gauge b₁,b₂),((X-SpanStart b₁,b₂) -' 1),b₃) \ (L~ (Span b₁,b₂)) c= BDD (L~ (Span b₁,b₂))

proof end;

theorem Th32: :: JORDAN14:32

for b₁ being Subset of (TOP-REAL 2)
for b₂, b₃, b₄ being Nat st b₃ <= b₂ & 1 < b₄ & b₄ + 1 < len (Gauge b₁,b₃) holds
(((2 |^ (b₂ -' b₃)) * (b₄ - 2)) + 2) + 1 < len (Gauge b₁,b₂)

proof end;

theorem Th33: :: JORDAN14:33

for b₁ being Simple_closed_curve
for b₂, b₃ being Nat st b₂ is_sufficiently_large_for b₁ & b₂ <= b₃ holds
RightComp (Span b₁,b₂) meets RightComp (Span b₁,b₃)

proof end;

theorem Th34: :: JORDAN14:34

for b₁ being Go-board
for b₂ being FinSequence of (TOP-REAL 2) st b₂ is_sequence_on b₁ & b₂ is special holds
for b₃, b₄ being Nat st b₃ <= len b₁ & b₄ <= width b₁ holds
Int (cell b₁,b₃,b₄) c= (L~ b₂) `

proof end;

theorem Th35: :: JORDAN14:35

for b₁ being Simple_closed_curve
for b₂, b₃ being Nat st b₂ is_sufficiently_large_for b₁ & b₂ <= b₃ holds
L~ (Span b₁,b₃) c= Cl (LeftComp (Span b₁,b₂))

proof end;

theorem Th36: :: JORDAN14:36

for b₁ being Simple_closed_curve
for b₂, b₃ being Nat st b₂ is_sufficiently_large_for b₁ & b₂ <= b₃ holds
RightComp (Span b₁,b₂) c= RightComp (Span b₁,b₃)

proof end;

theorem Th37: :: JORDAN14:37

for b₁ being Simple_closed_curve
for b₂, b₃ being Nat st b₂ is_sufficiently_large_for b₁ & b₂ <= b₃ holds
LeftComp (Span b₁,b₃) c= LeftComp (Span b₁,b₂)

proof end;