:: Properties of Left-, and Right Components
:: by Artur Korni{\l}owicz
::
:: Received May 5, 1999
:: Copyright (c) 1999-2016 Association of Mizar Users

environ

vocabularies HIDDEN, NUMBERS, SUBSET_1, FUNCT_1, GOBOARD5, SPRECT_2, PRE_TOPC, EUCLID, RCOMP_1, SPPOL_1, GOBOARD1, STRUCT_0, JORDAN2C, TOPREAL1, REAL_1, XXREAL_0, CARD_1, METRIC_1, TARSKI, XXREAL_2, ARYTM_3, XBOOLE_0, COMPLEX1, RELAT_2, CONNSP_1, FINSEQ_1, TREES_1, CARD_3, FUNCOP_1, XXREAL_1, RELAT_1, MCART_1, MATRIX_1, ARYTM_1, SQUARE_1, JORDAN8, NEWTON, PSCOMP_1, INT_1, POWER, GOBOARD9, RLTOPSP1, GOBOARD2, PARTFUN1, TOPS_1, JORDAN1, FINSEQ_6, SPRECT_1, SEQ_4, FINSEQ_2, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, BINOP_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, XXREAL_0, XXREAL_2, SQUARE_1, NAT_1, INT_1, INT_2, NEWTON, POWER, MATRIX_0, NAT_D, MATRIX_1, FUNCT_4, SEQ_4, METRIC_1, TBSP_1, FINSEQ_1, CARD_3, FINSEQ_2, FINSEQ_6, STRUCT_0, RCOMP_1, PRE_TOPC, TOPS_1, CONNSP_1, COMPTS_1, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2, GOBOARD5, GOBOARD9, PSCOMP_1, SPPOL_1, SPRECT_1, SPRECT_2, JORDAN2C, JORDAN8, TOPREAL6;
definitions TARSKI, JORDAN2C, SPRECT_1, XBOOLE_0;
theorems ABSVALUE, CARD_3, FUNCT_4, COMPTS_1, CONNSP_1, EUCLID, FINSEQ_1, FUNCT_1, FUNCT_2, GOBOARD5, GOBOARD6, GOBOARD7, GOBOARD9, GOBRD11, GOBRD12, INT_1, JORDAN2C, JORDAN8, METRIC_1, NAT_1, POWER, PRE_TOPC, PRE_FF, PSCOMP_1, RCOMP_1, RELAT_1, SEQ_4, SPRECT_1, SPRECT_3, SPRECT_4, SQUARE_1, SPPOL_2, SUBSET_1, TARSKI, TBSP_1, TDLAT_1, TOPREAL1, TOPREAL3, TOPREAL6, TOPS_1, SPRECT_2, REVROT_1, FINSEQ_6, XBOOLE_0, XBOOLE_1, XREAL_0, XCMPLX_1, COMPLEX1, XREAL_1, NEWTON, XXREAL_0, FINSEQ_2, MATRIX_0, XXREAL_1, NAT_D, RLTOPSP1;
schemes ;
registrations SUBSET_1, NUMBERS, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_6, STRUCT_0, PRE_TOPC, TOPS_1, MONOID_0, EUCLID, GOBOARD2, GOBRD11, SPRECT_1, SPRECT_3, JORDAN2C, REVROT_1, TOPREAL6, FUNCT_1, FINSEQ_1, PSCOMP_1, RELSET_1, JORDAN5A, NEWTON, SQUARE_1, ORDINAL1;
constructors HIDDEN, FUNCT_4, REAL_1, SQUARE_1, RCOMP_1, NEWTON, POWER, NAT_D, TOPS_1, CONNSP_1, COMPTS_1, TBSP_1, MONOID_0, TOPREAL4, GOBOARD2, SPPOL_1, JORDAN1, PSCOMP_1, GOBOARD9, SPRECT_1, SPRECT_2, JORDAN2C, TOPREAL6, JORDAN8, GOBOARD1, SEQ_4, RELSET_1, CONVEX1, BINOP_2, MATRIX_1, BINOP_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities JORDAN2C, XBOOLE_0, SQUARE_1, SUBSET_1, EUCLID;
expansions TARSKI, JORDAN2C, XBOOLE_0;


Lm1: the carrier of (TOP-REAL 2) = REAL 2
by EUCLID:22;

theorem :: GOBRD14:1
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;

theorem :: GOBRD14:2
for n being Nat
for f being FinSequence of (TOP-REAL n) st L~ f <> {} holds
2 <= len f
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).]))
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
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)
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)
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
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)) )
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)
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)
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 )
proof end;

theorem Th12: :: GOBRD14:12
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 or P = RightComp f or P = LeftComp f )
proof end;

theorem :: GOBRD14:13
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 & C2 is a_component ) ) & not ( A1 = RightComp f & A2 = LeftComp f ) holds
( A1 = LeftComp f & A2 = RightComp f )
proof end;

theorem Th14: :: GOBRD14:14
for f being non constant standard special_circular_sequence holds LeftComp f misses RightComp f
proof end;

theorem Th15: :: GOBRD14:15
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 Th16: :: GOBRD14:16
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 Th17: :: GOBRD14:17
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:18
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 Th16, Th17;

theorem Th19: :: GOBRD14:19
for f being non constant standard special_circular_sequence holds L~ f = (Cl (RightComp f)) \ (RightComp f)
proof end;

theorem Th20: :: GOBRD14:20
for f being non constant standard special_circular_sequence holds L~ f = (Cl (LeftComp f)) \ (LeftComp f)
proof end;

theorem Th21: :: GOBRD14:21
for f being non constant standard special_circular_sequence holds Cl (RightComp f) = (RightComp f) \/ (L~ f)
proof end;

theorem :: GOBRD14:22
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
L~ f is Jordan
proof end;
end;

theorem Th23: :: GOBRD14:23
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 Th24: :: GOBRD14:24
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 Th25: :: GOBRD14:25
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 Th26: :: GOBRD14:26
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 Th27: :: GOBRD14:27
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 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 non constant standard clockwise_oriented special_circular_sequence holds proj1 .: (Cl (RightComp f)) = proj1 .: (L~ f)
proof end;

theorem Th30: :: GOBRD14:30
for f being non constant standard clockwise_oriented special_circular_sequence holds proj2 .: (Cl (RightComp f)) = proj2 .: (L~ f)
proof end;

theorem Th31: :: GOBRD14:31
for g being non constant standard clockwise_oriented special_circular_sequence holds RightComp g c= RightComp (SpStSeq (L~ g))
proof end;

theorem Th32: :: GOBRD14:32
for g being non constant standard clockwise_oriented special_circular_sequence holds Cl (RightComp g) is compact
proof end;

theorem Th33: :: GOBRD14:33
for g being non constant standard clockwise_oriented special_circular_sequence holds not LeftComp g is bounded
proof end;

theorem Th34: :: GOBRD14:34
for g being non constant 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 non constant standard clockwise_oriented special_circular_sequence holds RightComp g is_inside_component_of L~ g
proof end;

theorem Th36: :: GOBRD14:36
for g being non constant standard clockwise_oriented special_circular_sequence holds UBD (L~ g) = LeftComp g
proof end;

theorem Th37: :: GOBRD14:37
for g being non constant standard clockwise_oriented special_circular_sequence holds BDD (L~ g) = RightComp g
proof end;

theorem :: GOBRD14:38
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 Th39: :: GOBRD14:39
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:40
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:41
for g being non constant standard clockwise_oriented special_circular_sequence holds W-bound (L~ g) = W-bound (RightComp g)
proof end;

theorem :: GOBRD14:42
for g being non constant standard clockwise_oriented special_circular_sequence holds E-bound (L~ g) = E-bound (RightComp g)
proof end;

theorem :: GOBRD14:43
for g being non constant standard clockwise_oriented special_circular_sequence holds N-bound (L~ g) = N-bound (RightComp g)
proof end;

theorem :: GOBRD14:44
for g being non constant standard clockwise_oriented special_circular_sequence holds S-bound (L~ g) = S-bound (RightComp g)
proof end;