:: GOBRD14 semantic presentation

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

theorem Th1: :: GOBRD14:1

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₃ is_a_component_of b₂ holds
b₃ is connected

proof end;

theorem Th2: :: GOBRD14:2

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) st b₃ is_inside_component_of b₂ holds
b₃ is connected

proof end;

theorem Th3: :: GOBRD14:3

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) st b₃ is_outside_component_of b₂ holds
b₃ is connected

proof end;

theorem Th4: :: GOBRD14:4

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) st b₃ is_a_component_of b₂ ` holds
b₂ misses b₃

proof end;

theorem Th5: :: GOBRD14:5

for b₁, b₂, b₃ being Subset of (TOP-REAL 2) st b₁ is_outside_component_of b₂ & b₃ is_inside_component_of b₂ holds
b₁ misses b₃

proof end;

theorem Th6: :: GOBRD14:6

for b₁ being Nat st 2 <= b₁ holds
for b₂, b₃, b₄ being Subset of (TOP-REAL b₁) st b₄ is Bounded & b₂ is_outside_component_of b₄ & b₃ is_outside_component_of b₄ holds
b₂ = b₃

proof end;

theorem Th7: :: GOBRD14:7

for b₁ being non constant standard special_circular_sequence
for b₂ being Subset of (TOP-REAL 2)
for b₃ being Point of (Euclid 2) st b₃ = 0.REAL 2 & b₂ is_outside_component_of L~ b₁ holds
ex b₄ being Real st
( b₄ > 0 & (Ball b₃,b₄) ` c= b₂ )

proof end;

registration

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

proof end;

cluster UBD a₁ -> open ;
coherence

proof end;

end;

registration

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

proof end;

end;

theorem Th8: :: GOBRD14:8

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

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Point of (TOP-REAL c₁);
func dist c₂,c₃ -> Real means :Def1: :: GOBRD14:def 1
ex b₁, b₂ being Point of (Euclid a₁) st
( b₁ = a₂ & b₂ = a₃ & a₄ = dist b₁,b₂ );
existence

proof end;

uniqueness ;
commutativity ;

end;

:: deftheorem Def1 defines dist GOBRD14:def 1 :

theorem Th9: :: GOBRD14:9

for b₁, b₂ being Point of (TOP-REAL 2) holds dist b₁,b₂ = sqrt ((((b₁ `1 ) - (b₂ `1 )) ^2 ) + (((b₁ `2 ) - (b₂ `2 )) ^2 ))

proof end;

theorem Th10: :: GOBRD14:10

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁) holds dist b₂,b₂ = 0

proof end;

theorem Th11: :: GOBRD14:11

for b₁ being Nat
for b₂, b₃, b₄ being Point of (TOP-REAL b₁) holds dist b₂,b₄ <= (dist b₂,b₃) + (dist b₃,b₄)

proof end;

theorem Th12: :: GOBRD14:12

for b₁, b₂, b₃, b₄ being real number
for b₅, b₆ being Point of (TOP-REAL 2) st b₁ <= b₅ `1 & b₅ `1 <= b₂ & b₃ <= b₅ `2 & b₅ `2 <= b₄ & b₁ <= b₆ `1 & b₆ `1 <= b₂ & b₃ <= b₆ `2 & b₆ `2 <= b₄ holds
dist b₅,b₆ <= (b₂ - b₁) + (b₄ - b₃)

proof end;

theorem Th13: :: GOBRD14:13

for b₁, b₂ being Nat
for b₃ being Go-board st 1 <= b₁ & b₁ < len b₃ & 1 <= b₂ & b₂ < width b₃ holds
cell b₃,b₁,b₂ = product (1,2 --> [.((b₃ * b₁,1) `1 ),((b₃ * (b₁ + 1),1) `1 ).],[.((b₃ * 1,b₂) `2 ),((b₃ * 1,(b₂ + 1)) `2 ).])

proof end;

theorem Th14: :: GOBRD14:14

for b₁, b₂ being Nat
for b₃ being Go-board st 1 <= b₁ & b₁ < len b₃ & 1 <= b₂ & b₂ < width b₃ holds
cell b₃,b₁,b₂ is compact

proof end;

theorem Th15: :: GOBRD14:15

for b₁, b₂, b₃ being Nat
for b₄ being Go-board st [b₁,b₂] in Indices b₄ & [(b₁ + b₃),b₂] in Indices b₄ holds
dist (b₄ * b₁,b₂),(b₄ * (b₁ + b₃),b₂) = ((b₄ * (b₁ + b₃),b₂) `1 ) - ((b₄ * b₁,b₂) `1 )

proof end;

theorem Th16: :: GOBRD14:16

for b₁, b₂, b₃ being Nat
for b₄ being Go-board st [b₁,b₂] in Indices b₄ & [b₁,(b₂ + b₃)] in Indices b₄ holds
dist (b₄ * b₁,b₂),(b₄ * b₁,(b₂ + b₃)) = ((b₄ * b₁,(b₂ + b₃)) `2 ) - ((b₄ * b₁,b₂) `2 )

proof end;

theorem Th17: :: GOBRD14:17

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

proof end;

theorem Th18: :: GOBRD14:18

for b₁, b₂ being Nat
for b₃ being compact non horizontal non vertical Subset of (TOP-REAL 2) st b₁ <= b₂ holds
for b₄, b₅ being Nat st 2 <= b₄ & b₄ <= (len (Gauge b₃,b₁)) - 1 & 2 <= b₅ & b₅ <= (len (Gauge b₃,b₁)) - 1 holds
ex b₆, b₇ being Nat st
( 2 <= b₆ & b₆ <= (len (Gauge b₃,b₂)) - 1 & 2 <= b₇ & b₇ <= (len (Gauge b₃,b₂)) - 1 & [b₆,b₇] in Indices (Gauge b₃,b₂) & (Gauge b₃,b₁) * b₄,b₅ = (Gauge b₃,b₂) * b₆,b₇ & b₆ = 2 + ((2 |^ (b₂ -' b₁)) * (b₄ -' 2)) & b₇ = 2 + ((2 |^ (b₂ -' b₁)) * (b₅ -' 2)) )

proof end;

theorem Th19: :: GOBRD14:19

for b₁, b₂, b₃ being Nat
for b₄ being compact non horizontal non vertical Subset of (TOP-REAL 2) st [b₁,b₂] in Indices (Gauge b₄,b₃) & [b₁,(b₂ + 1)] in Indices (Gauge b₄,b₃) holds
dist ((Gauge b₄,b₃) * b₁,b₂),((Gauge b₄,b₃) * b₁,(b₂ + 1)) = ((N-bound b₄) - (S-bound b₄)) / (2 |^ b₃)

proof end;

theorem Th20: :: GOBRD14:20

for b₁, b₂, b₃ being Nat
for b₄ being compact non horizontal non vertical Subset of (TOP-REAL 2) st [b₁,b₂] in Indices (Gauge b₄,b₃) & [(b₁ + 1),b₂] in Indices (Gauge b₄,b₃) holds
dist ((Gauge b₄,b₃) * b₁,b₂),((Gauge b₄,b₃) * (b₁ + 1),b₂) = ((E-bound b₄) - (W-bound b₄)) / (2 |^ b₃)

proof end;

theorem Th21: :: GOBRD14:21

for b₁ being compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₂, b₃ being real number st b₂ > 0 & b₃ > 0 holds
ex b₄ being Nat st
( 1 < b₄ & dist ((Gauge b₁,b₄) * 1,1),((Gauge b₁,b₄) * 1,2) < b₂ & dist ((Gauge b₁,b₄) * 1,1),((Gauge b₁,b₄) * 2,1) < b₃ )

proof end;

theorem Th22: :: GOBRD14:22

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

proof end;

theorem Th23: :: GOBRD14:23

for b₁ being non constant standard special_circular_sequence
for b₂, b₃ being Subset of (TOP-REAL 2) st (L~ b₁) ` = b₂ \/ b₃ & b₂ misses b₃ & ( for b₄, b₅ being Subset of ((TOP-REAL 2) | ((L~ b₁) ` )) st b₄ = b₂ & b₅ = b₃ holds
( b₄ is_a_component_of (TOP-REAL 2) | ((L~ b₁) ` ) & b₅ is_a_component_of (TOP-REAL 2) | ((L~ b₁) ` ) ) ) & not ( b₂ = RightComp b₁ & b₃ = LeftComp b₁ ) holds
( b₂ = LeftComp b₁ & b₃ = RightComp b₁ )

proof end;

theorem Th24: :: GOBRD14:24

for b₁ being non constant standard special_circular_sequence holds LeftComp b₁ misses RightComp b₁

proof end;

theorem Th25: :: GOBRD14:25

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

proof end;

theorem Th26: :: GOBRD14:26

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

proof end;

theorem Th27: :: GOBRD14:27

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

proof end;

theorem Th28: :: GOBRD14:28

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

theorem Th29: :: GOBRD14:29

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

proof end;

theorem Th30: :: GOBRD14:30

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

proof end;

theorem Th31: :: GOBRD14:31

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

proof end;

theorem Th32: :: GOBRD14:32

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

proof end;

registration

let c₁ be non constant standard special_circular_sequence;
cluster L~ a₁ -> Jordan ;
coherence

proof end;

end;

theorem Th33: :: GOBRD14:33

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

proof end;

theorem Th34: :: GOBRD14:34

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

proof end;

theorem Th35: :: GOBRD14:35

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

proof end;

theorem Th36: :: GOBRD14:36

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

proof end;

theorem Th37: :: GOBRD14:37

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being non constant standard clockwise_oriented special_circular_sequence st b₁ in RightComp b₃ & b₂ in LeftComp b₃ holds
LSeg b₁,b₂ meets L~ b₃

proof end;

theorem Th38: :: GOBRD14:38

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

proof end;

theorem Th39: :: GOBRD14:39

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

proof end;

theorem Th40: :: GOBRD14:40

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

proof end;

theorem Th41: :: GOBRD14:41

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

proof end;

theorem Th42: :: GOBRD14:42

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

proof end;

theorem Th43: :: GOBRD14:43

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

proof end;

theorem Th44: :: GOBRD14:44

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

proof end;

theorem Th45: :: GOBRD14:45

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

proof end;

theorem Th46: :: GOBRD14:46

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

proof end;

theorem Th47: :: GOBRD14:47

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

proof end;

theorem Th48: :: GOBRD14:48

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

proof end;

theorem Th49: :: GOBRD14:49

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

proof end;

theorem Th50: :: GOBRD14:50

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

proof end;

theorem Th51: :: GOBRD14:51

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

proof end;

theorem Th52: :: GOBRD14:52

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

proof end;

theorem Th53: :: GOBRD14:53

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

proof end;

theorem Th54: :: GOBRD14:54

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

proof end;