:: Properties of Left-, and Right Components :: by Artur Korni{\l}owicz :: :: Received May 5, 1999 :: Copyright (c) 1999-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies 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 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; constructors 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; 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; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin :: Components reserve i, j, n for Nat, f for non constant standard special_circular_sequence, g for clockwise_oriented non constant standard special_circular_sequence, p, q for Point of TOP-REAL 2, P for Subset of TOP-REAL 2, C for compact non vertical non horizontal Subset of TOP-REAL 2, G for Go-board; theorem :: GOBRD14:1 for p being Point of Euclid 2 st p = 0.REAL 2 & P is_outside_component_of L~f ex r being Real st r > 0 & Ball(p,r)` c= P; begin :: Go-boards theorem :: GOBRD14:2 for f being FinSequence of TOP-REAL n st L~f <> {} holds 2 <= len f; theorem :: GOBRD14:3 1 <= i & i < len G & 1 <= j & j < width G implies 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.])); theorem :: GOBRD14:4 1 <= i & i < len G & 1 <= j & j < width G implies cell(G,i,j) is compact; theorem :: GOBRD14:5 [i,j] in Indices G & [i+n,j] in Indices G implies dist(G*(i,j),G*(i+n, j)) = G*(i+n,j)`1 - G*(i,j)`1; theorem :: GOBRD14:6 [i,j] in Indices G & [i,j+n] in Indices G implies dist(G*(i,j),G*(i,j+ n)) = G*(i,j+n)`2 - G*(i,j)`2; theorem :: GOBRD14:7 3 <= len Gauge(C,n)-'1; theorem :: GOBRD14:8 i <= j implies for a, b being Nat st 2 <= a & a <= len Gauge(C,i) - 1 & 2 <= b & b <= len Gauge(C,i) - 1 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); theorem :: GOBRD14:9 [i,j] in Indices Gauge(C,n) & [i,j+1] in Indices Gauge(C,n) implies dist(Gauge(C,n)*(i,j),Gauge(C,n)*(i,j+1)) = (N-bound C - S-bound C)/2|^ n; theorem :: GOBRD14:10 [i,j] in Indices Gauge(C,n) & [i+1,j] in Indices Gauge(C,n) implies dist(Gauge(C,n)*(i,j),Gauge(C,n)*(i+1,j)) = (E-bound C - W-bound C)/2|^ n; theorem :: GOBRD14:11 for r, t being Real holds r > 0 & t > 0 implies 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; begin :: LeftComp and RightComp theorem :: GOBRD14:12 for P being Subset of (TOP-REAL 2)|(L~f)` st P is a_component holds P = RightComp f or P = LeftComp f; theorem :: GOBRD14:13 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 holds A1 = RightComp f & A2 = LeftComp f or A1 = LeftComp f & A2 = RightComp f; theorem :: GOBRD14:14 LeftComp f misses RightComp f; theorem :: GOBRD14:15 L~f \/ RightComp f \/ LeftComp f = the carrier of TOP-REAL 2; theorem :: GOBRD14:16 p in L~f iff not p in LeftComp f & not p in RightComp f; theorem :: GOBRD14:17 p in LeftComp f iff not p in L~f & not p in RightComp f; theorem :: GOBRD14:18 p in RightComp f iff not p in L~f & not p in LeftComp f; theorem :: GOBRD14:19 L~f = (Cl RightComp f) \ RightComp f; theorem :: GOBRD14:20 L~f = (Cl LeftComp f) \ LeftComp f; theorem :: GOBRD14:21 Cl RightComp f = (RightComp f) \/ L~f; theorem :: GOBRD14:22 Cl LeftComp f = (LeftComp f) \/ L~f; registration let f be non constant standard special_circular_sequence; cluster L~f -> Jordan; end; reserve f for clockwise_oriented non constant standard special_circular_sequence; theorem :: GOBRD14:23 p in RightComp f implies W-bound L~f < p`1; theorem :: GOBRD14:24 p in RightComp f implies E-bound L~f > p`1; theorem :: GOBRD14:25 p in RightComp f implies N-bound L~f > p`2; theorem :: GOBRD14:26 p in RightComp f implies S-bound L~f < p`2; theorem :: GOBRD14:27 p in RightComp f & q in LeftComp f implies LSeg(p,q) meets L~f; theorem :: GOBRD14:28 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.])); theorem :: GOBRD14:29 proj1.:(Cl RightComp f) = proj1.:(L~f); theorem :: GOBRD14:30 proj2.:(Cl RightComp f) = proj2.:(L~f); theorem :: GOBRD14:31 RightComp g c= RightComp SpStSeq L~g; theorem :: GOBRD14:32 Cl RightComp g is compact; theorem :: GOBRD14:33 LeftComp g is non bounded; theorem :: GOBRD14:34 LeftComp g is_outside_component_of L~g; theorem :: GOBRD14:35 RightComp g is_inside_component_of L~g; theorem :: GOBRD14:36 UBD L~g = LeftComp g; theorem :: GOBRD14:37 BDD L~g = RightComp g; theorem :: GOBRD14:38 P is_outside_component_of L~g implies P = LeftComp g; theorem :: GOBRD14:39 P is_inside_component_of L~g implies P meets RightComp g; theorem :: GOBRD14:40 P is_inside_component_of L~g implies P = BDD L~g; theorem :: GOBRD14:41 W-bound L~g = W-bound RightComp g; theorem :: GOBRD14:42 E-bound L~g = E-bound RightComp g; theorem :: GOBRD14:43 N-bound L~g = N-bound RightComp g; theorem :: GOBRD14:44 S-bound L~g = S-bound RightComp g;