:: by Artur Korni{\l}owicz

::

:: Received May 5, 1999

:: Copyright (c) 1999-2021 Association of Mizar Users

Lm1: the carrier of (TOP-REAL 2) = REAL 2

by EUCLID:22;

theorem :: GOBRD14:1

for f being V8() 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 )

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;

theorem Th3: :: GOBRD14:3

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).]))

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:4

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

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:5

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)

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:6

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)

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:7

for n being Nat

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

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

proof end;

theorem :: GOBRD14:8

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)) )

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 Th9: :: GOBRD14:9

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)

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 Th10: :: GOBRD14:10

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)

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:11

for C being compact non horizontal non vertical Subset of (TOP-REAL 2)

for r, t being Real 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 )

for r, t being Real 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 Th12: :: GOBRD14:12

for f being V8() standard special_circular_sequence

for P being Subset of ((TOP-REAL 2) | ((L~ f) `)) holds

( not P is a_component or P = RightComp f or P = LeftComp f )

for P being Subset of ((TOP-REAL 2) | ((L~ f) `)) holds

( not P is a_component or P = RightComp f or P = LeftComp f )

proof end;

theorem :: GOBRD14:13

for f being V8() 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 & C2 is a_component ) ) & not ( A1 = RightComp f & A2 = LeftComp f ) holds

( A1 = LeftComp f & A2 = RightComp f )

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 & C2 is a_component ) ) & not ( A1 = RightComp f & A2 = LeftComp f ) holds

( A1 = LeftComp f & A2 = RightComp f )

proof end;

theorem Th15: :: GOBRD14:15

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

proof end;

theorem Th16: :: GOBRD14:16

for f being V8() 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 ) )

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 Th17: :: GOBRD14:17

for f being V8() 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 ) )

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:18

theorem Th21: :: GOBRD14:21

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

proof end;

registration
end;

theorem Th23: :: GOBRD14:23

for p being Point of (TOP-REAL 2)

for f being V8() standard clockwise_oriented special_circular_sequence st p in RightComp f holds

W-bound (L~ f) < p `1

for f being V8() standard clockwise_oriented special_circular_sequence st p in RightComp f holds

W-bound (L~ f) < p `1

proof end;

theorem Th24: :: GOBRD14:24

for p being Point of (TOP-REAL 2)

for f being V8() standard clockwise_oriented special_circular_sequence st p in RightComp f holds

E-bound (L~ f) > p `1

for f being V8() standard clockwise_oriented special_circular_sequence st p in RightComp f holds

E-bound (L~ f) > p `1

proof end;

theorem Th25: :: GOBRD14:25

for p being Point of (TOP-REAL 2)

for f being V8() standard clockwise_oriented special_circular_sequence st p in RightComp f holds

N-bound (L~ f) > p `2

for f being V8() standard clockwise_oriented special_circular_sequence st p in RightComp f holds

N-bound (L~ f) > p `2

proof end;

theorem Th26: :: GOBRD14:26

for p being Point of (TOP-REAL 2)

for f being V8() standard clockwise_oriented special_circular_sequence st p in RightComp f holds

S-bound (L~ f) < p `2

for f being V8() standard clockwise_oriented special_circular_sequence st p in RightComp f holds

S-bound (L~ f) < p `2

proof end;

theorem Th27: :: GOBRD14:27

for p, q being Point of (TOP-REAL 2)

for f being V8() standard clockwise_oriented special_circular_sequence st p in RightComp f & q in LeftComp f holds

LSeg (p,q) meets L~ f

for f being V8() 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 Th28: :: GOBRD14:28

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 Th29: :: GOBRD14:29

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

proof end;

theorem Th30: :: GOBRD14:30

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

proof end;

theorem Th31: :: GOBRD14:31

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

proof end;

theorem Th32: :: GOBRD14:32

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

proof end;

theorem Th33: :: GOBRD14:33

for g being V8() standard clockwise_oriented special_circular_sequence holds not LeftComp g is bounded

proof end;

theorem Th34: :: GOBRD14:34

for g being V8() standard clockwise_oriented special_circular_sequence holds LeftComp g is_outside_component_of L~ g by GOBOARD9:def 1, Th33;

theorem :: GOBRD14:35

for g being V8() standard clockwise_oriented special_circular_sequence holds RightComp g is_inside_component_of L~ g

proof end;

theorem Th36: :: GOBRD14:36

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

proof end;

theorem Th37: :: GOBRD14:37

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

proof end;

theorem :: GOBRD14:38

for g being V8() 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

for P being Subset of (TOP-REAL 2) st P is_outside_component_of L~ g holds

P = LeftComp g

proof end;

theorem Th39: :: GOBRD14:39

for g being V8() 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

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:40

for g being V8() 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)

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:41

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

proof end;

theorem :: GOBRD14:42

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

proof end;

theorem :: GOBRD14:43

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

proof end;

theorem :: GOBRD14:44

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

proof end;