:: GOBRD14 semantic presentation

Lm1: Euclid 2 = MetrStruct(# (REAL 2),(Pitag_dist 2) #)
by EUCLID:def 7;

theorem :: GOBRD14:1

for T being TopSpace
for A, B being Subset of T st B is_a_component_of A holds
B is connected

proof end;

theorem :: GOBRD14:2

for n being Nat
for A, B being Subset of (TOP-REAL n) st B is_inside_component_of A holds
B is connected

proof end;

theorem Th3: :: GOBRD14:3

for n being Nat
for A, B being Subset of (TOP-REAL n) st B is_outside_component_of A holds
B is connected

proof end;

theorem :: GOBRD14:4

for n being Nat
for A, B being Subset of (TOP-REAL n) st B is_a_component_of A ` holds
A misses B

proof end;

theorem :: GOBRD14:5

for P, Q, R being Subset of (TOP-REAL 2) st P is_outside_component_of Q & R is_inside_component_of Q holds
P misses R

proof end;

theorem Th6: :: GOBRD14:6

for n being Nat st 2 <= n holds
for A, B, P being Subset of (TOP-REAL n) st P is Bounded & A is_outside_component_of P & B is_outside_component_of P holds
A = B

proof end;

theorem :: GOBRD14:7

for f being non constant standard special_circular_sequence
for P being Subset of (TOP-REAL 2)
for p being Point of (Euclid 2) st p = 0.REAL 2 & P is_outside_component_of L~ f holds
ex r being Real st
( r > 0 & (Ball p,r) ` c= P )

proof end;

registration

let C be closed Subset of (TOP-REAL 2);
cluster BDD C -> open ;
coherence

proof end;

cluster UBD C -> open ;
coherence

proof end;

end;

registration

let C be compact Subset of (TOP-REAL 2);
cluster UBD C -> connected ;
coherence

proof end;

end;

theorem :: GOBRD14:8

for n being Nat
for f being FinSequence of (TOP-REAL n) st L~ f <> {} holds
2 <= len f

proof end;

definition

let n be Nat;
let a, b be Point of (TOP-REAL n);
func dist a,b -> Real means :Def1: :: GOBRD14:def 1
ex p, q being Point of (Euclid n) st
( p = a & q = b & it = dist p,q );
existence

proof end;

uniqueness ;
commutativity ;

end;

:: deftheorem Def1 defines dist GOBRD14:def 1 :

theorem Th9: :: GOBRD14:9

for p, q being Point of (TOP-REAL 2) holds dist p,q = sqrt ((((p `1 ) - (q `1 )) ^2 ) + (((p `2 ) - (q `2 )) ^2 ))

proof end;

theorem Th10: :: GOBRD14:10

for n being Nat
for p being Point of (TOP-REAL n) holds dist p,p = 0

proof end;

theorem :: GOBRD14:11

for n being Nat
for p, q, r being Point of (TOP-REAL n) holds dist p,r <= (dist p,q) + (dist q,r)

proof end;

theorem :: GOBRD14:12

for x1, x2, y1, y2 being real number
for a, b being Point of (TOP-REAL 2) st x1 <= a `1 & a `1 <= x2 & y1 <= a `2 & a `2 <= y2 & x1 <= b `1 & b `1 <= x2 & y1 <= b `2 & b `2 <= y2 holds
dist a,b <= (x2 - x1) + (y2 - y1)

proof end;

theorem Th13: :: GOBRD14:13

for i, j being Nat
for G being Go-board st 1 <= i & i < len G & 1 <= j & j < width G holds
cell G,i,j = product (1,2 --> [.((G * i,1) `1 ),((G * (i + 1),1) `1 ).],[.((G * 1,j) `2 ),((G * 1,(j + 1)) `2 ).])

proof end;

theorem :: GOBRD14:14

for i, j being Nat
for G being Go-board st 1 <= i & i < len G & 1 <= j & j < width G holds
cell G,i,j is compact

proof end;

theorem :: GOBRD14:15

for i, j, n being Nat
for G being Go-board st [i,j] in Indices G & [(i + n),j] in Indices G holds
dist (G * i,j),(G * (i + n),j) = ((G * (i + n),j) `1 ) - ((G * i,j) `1 )

proof end;

theorem :: GOBRD14:16

for i, j, n being Nat
for G being Go-board st [i,j] in Indices G & [i,(j + n)] in Indices G holds
dist (G * i,j),(G * i,(j + n)) = ((G * i,(j + n)) `2 ) - ((G * i,j) `2 )

proof end;

theorem :: GOBRD14:17

for n being Nat
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds 3 <= (len (Gauge C,n)) -' 1

proof end;

theorem :: GOBRD14:18

for i, j being Nat
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st i <= j holds
for a, b being Nat st 2 <= a & a <= (len (Gauge C,i)) - 1 & 2 <= b & b <= (len (Gauge C,i)) - 1 holds
ex c, d being Nat st
( 2 <= c & c <= (len (Gauge C,j)) - 1 & 2 <= d & d <= (len (Gauge C,j)) - 1 & [c,d] in Indices (Gauge C,j) & (Gauge C,i) * a,b = (Gauge C,j) * c,d & c = 2 + ((2 |^ (j -' i)) * (a -' 2)) & d = 2 + ((2 |^ (j -' i)) * (b -' 2)) )

proof end;

theorem Th19: :: GOBRD14:19

for i, j, n being Nat
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st [i,j] in Indices (Gauge C,n) & [i,(j + 1)] in Indices (Gauge C,n) holds
dist ((Gauge C,n) * i,j),((Gauge C,n) * i,(j + 1)) = ((N-bound C) - (S-bound C)) / (2 |^ n)

proof end;

theorem Th20: :: GOBRD14:20

for i, j, n being Nat
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st [i,j] in Indices (Gauge C,n) & [(i + 1),j] in Indices (Gauge C,n) holds
dist ((Gauge C,n) * i,j),((Gauge C,n) * (i + 1),j) = ((E-bound C) - (W-bound C)) / (2 |^ n)

proof end;

theorem :: GOBRD14:21

for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for r, t being real number st r > 0 & t > 0 holds
ex n being Nat st
( 1 < n & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) < r & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 2,1) < t )

proof end;

theorem Th22: :: GOBRD14:22

for f being non constant standard special_circular_sequence
for P being Subset of ((TOP-REAL 2) | ((L~ f) ` )) holds
( not P is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) or P = RightComp f or P = LeftComp f )

proof end;

theorem :: GOBRD14:23

for f being non constant standard special_circular_sequence
for A1, A2 being Subset of (TOP-REAL 2) st (L~ f) ` = A1 \/ A2 & A1 misses A2 & ( for C1, C2 being Subset of ((TOP-REAL 2) | ((L~ f) ` )) st C1 = A1 & C2 = A2 holds
( C1 is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) & C2 is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) ) ) & not ( A1 = RightComp f & A2 = LeftComp f ) holds
( A1 = LeftComp f & A2 = RightComp f )

proof end;

theorem Th24: :: GOBRD14:24

for f being non constant standard special_circular_sequence holds LeftComp f misses RightComp f

proof end;

theorem Th25: :: GOBRD14:25

for f being non constant standard special_circular_sequence holds ((L~ f) \/ (RightComp f)) \/ (LeftComp f) = the carrier of (TOP-REAL 2)

proof end;

theorem Th26: :: GOBRD14:26

for f being non constant standard special_circular_sequence
for p being Point of (TOP-REAL 2) holds
( p in L~ f iff ( not p in LeftComp f & not p in RightComp f ) )

proof end;

theorem Th27: :: GOBRD14:27

for f being non constant standard special_circular_sequence
for p being Point of (TOP-REAL 2) holds
( p in LeftComp f iff ( not p in L~ f & not p in RightComp f ) )

proof end;

theorem :: GOBRD14:28

for f being non constant standard special_circular_sequence
for p being Point of (TOP-REAL 2) holds
( p in RightComp f iff ( not p in L~ f & not p in LeftComp f ) ) by Th26, Th27;

theorem Th29: :: GOBRD14:29

for f being non constant standard special_circular_sequence holds L~ f = (Cl (RightComp f)) \ (RightComp f)

proof end;

theorem Th30: :: GOBRD14:30

for f being non constant standard special_circular_sequence holds L~ f = (Cl (LeftComp f)) \ (LeftComp f)

proof end;

theorem Th31: :: GOBRD14:31

for f being non constant standard special_circular_sequence holds Cl (RightComp f) = (RightComp f) \/ (L~ f)

proof end;

theorem :: GOBRD14:32

for f being non constant standard special_circular_sequence holds Cl (LeftComp f) = (LeftComp f) \/ (L~ f)

proof end;

registration

let f be non constant standard special_circular_sequence;
cluster L~ f -> Jordan ;
coherence

proof end;

end;

theorem Th33: :: GOBRD14:33

for p being Point of (TOP-REAL 2)
for f being non constant standard clockwise_oriented special_circular_sequence st p in RightComp f holds
W-bound (L~ f) < p `1

proof end;

theorem Th34: :: GOBRD14:34

for p being Point of (TOP-REAL 2)
for f being non constant standard clockwise_oriented special_circular_sequence st p in RightComp f holds
E-bound (L~ f) > p `1

proof end;

theorem Th35: :: GOBRD14:35

for p being Point of (TOP-REAL 2)
for f being non constant standard clockwise_oriented special_circular_sequence st p in RightComp f holds
N-bound (L~ f) > p `2

proof end;

theorem Th36: :: GOBRD14:36

for p being Point of (TOP-REAL 2)
for f being non constant standard clockwise_oriented special_circular_sequence st p in RightComp f holds
S-bound (L~ f) < p `2

proof end;

theorem Th37: :: GOBRD14:37

for p, q being Point of (TOP-REAL 2)
for f being non constant standard clockwise_oriented special_circular_sequence st p in RightComp f & q in LeftComp f holds
LSeg p,q meets L~ f

proof end;

theorem Th38: :: GOBRD14:38

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds Cl (RightComp (SpStSeq C)) = product (1,2 --> [.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])

proof end;

theorem Th39: :: GOBRD14:39

for f being non constant standard clockwise_oriented special_circular_sequence holds proj1 .: (Cl (RightComp f)) = proj1 .: (L~ f)

proof end;

theorem Th40: :: GOBRD14:40

for f being non constant standard clockwise_oriented special_circular_sequence holds proj2 .: (Cl (RightComp f)) = proj2 .: (L~ f)

proof end;

theorem Th41: :: GOBRD14:41

for g being non constant standard clockwise_oriented special_circular_sequence holds RightComp g c= RightComp (SpStSeq (L~ g))

proof end;

theorem Th42: :: GOBRD14:42

for g being non constant standard clockwise_oriented special_circular_sequence holds Cl (RightComp g) is compact

proof end;

theorem Th43: :: GOBRD14:43

for g being non constant standard clockwise_oriented special_circular_sequence holds not LeftComp g is Bounded

proof end;

theorem Th44: :: GOBRD14:44

for g being non constant standard clockwise_oriented special_circular_sequence holds LeftComp g is_outside_component_of L~ g

proof end;

theorem :: GOBRD14:45

for g being non constant standard clockwise_oriented special_circular_sequence holds RightComp g is_inside_component_of L~ g

proof end;

theorem Th46: :: GOBRD14:46

for g being non constant standard clockwise_oriented special_circular_sequence holds UBD (L~ g) = LeftComp g

proof end;

theorem Th47: :: GOBRD14:47

for g being non constant standard clockwise_oriented special_circular_sequence holds BDD (L~ g) = RightComp g

proof end;

theorem :: GOBRD14:48

for g being non constant standard clockwise_oriented special_circular_sequence
for P being Subset of (TOP-REAL 2) st P is_outside_component_of L~ g holds
P = LeftComp g

proof end;

theorem Th49: :: GOBRD14:49

for g being non constant standard clockwise_oriented special_circular_sequence
for P being Subset of (TOP-REAL 2) st P is_inside_component_of L~ g holds
P meets RightComp g

proof end;

theorem :: GOBRD14:50

for g being non constant standard clockwise_oriented special_circular_sequence
for P being Subset of (TOP-REAL 2) st P is_inside_component_of L~ g holds
P = BDD (L~ g)

proof end;

theorem :: GOBRD14:51

for g being non constant standard clockwise_oriented special_circular_sequence holds W-bound (L~ g) = W-bound (RightComp g)

proof end;

theorem :: GOBRD14:52

for g being non constant standard clockwise_oriented special_circular_sequence holds E-bound (L~ g) = E-bound (RightComp g)

proof end;

theorem :: GOBRD14:53

for g being non constant standard clockwise_oriented special_circular_sequence holds N-bound (L~ g) = N-bound (RightComp g)

proof end;

theorem :: GOBRD14:54

for g being non constant standard clockwise_oriented special_circular_sequence holds S-bound (L~ g) = S-bound (RightComp g)

proof end;