:: The Jordan's Property for Certain Subsets of the Plane :: by Yatsuka Nakamura and Jaros{\l}aw Kotowicz :: :: Received August 24, 1992 :: Copyright (c) 1992-2012 Association of Mizar Users begin Lm1: ( 0 in [.0,1.] & 1 in [.0,1.] ) proofend; theorem Th1: :: JORDAN1:1 for GX being non empty TopSpace st ( for x, y being Point of GX ex h being Function of I[01],GX st ( h is continuous & x = h . 0 & y = h . 1 ) ) holds GX is connected proofend; theorem Th2: :: JORDAN1:2 for GX being non empty TopSpace for A being Subset of GX st ( for xa, ya being Point of GX st xa in A & ya in A & xa <> ya holds ex h being Function of I[01],(GX | A) st ( h is continuous & xa = h . 0 & ya = h . 1 ) ) holds A is connected proofend; theorem :: JORDAN1:3 for GX being non empty TopSpace for A0, A1 being Subset of GX st A0 is connected & A1 is connected & A0 meets A1 holds A0 \/ A1 is connected by CONNSP_1:1, CONNSP_1:17; theorem Th4: :: JORDAN1:4 for GX being non empty TopSpace for A0, A1, A2 being Subset of GX st A0 is connected & A1 is connected & A2 is connected & A0 meets A1 & A1 meets A2 holds (A0 \/ A1) \/ A2 is connected proofend; theorem Th5: :: JORDAN1:5 for GX being non empty TopSpace for A0, A1, A2, A3 being Subset of GX st A0 is connected & A1 is connected & A2 is connected & A3 is connected & A0 meets A1 & A1 meets A2 & A2 meets A3 holds ((A0 \/ A1) \/ A2) \/ A3 is connected proofend; begin definition let V be RealLinearSpace; let P be Subset of V; redefine attr P is convex means :: JORDAN1:def 1 for w1, w2 being Element of V st w1 in P & w2 in P holds LSeg (w1,w2) c= P; compatibility ( P is convex iff for w1, w2 being Element of V st w1 in P & w2 in P holds LSeg (w1,w2) c= P ) by RLTOPSP1:22; end; :: deftheorem defines convex JORDAN1:def_1_:_ for V being RealLinearSpace for P being Subset of V holds ( P is convex iff for w1, w2 being Element of V st w1 in P & w2 in P holds LSeg (w1,w2) c= P ); registration let n be Nat; cluster convex -> connected for Element of K6( the carrier of (TOP-REAL n)); coherence for b1 being Subset of (TOP-REAL n) st b1 is convex holds b1 is connected proofend; end; Lm2: the carrier of (TOP-REAL 2) = REAL 2 by EUCLID:22; Lm3: for s1 being Real holds { |[sb,tb]| where sb, tb is Real : sb < s1 } is Subset of (REAL 2) proofend; Lm4: for t1 being Real holds { |[sb,tb]| where sb, tb is Real : tb < t1 } is Subset of (REAL 2) proofend; Lm5: for s2 being Real holds { |[sb,tb]| where sb, tb is Real : s2 < sb } is Subset of (REAL 2) proofend; Lm6: for t2 being Real holds { |[sb,tb]| where sb, tb is Real : t2 < tb } is Subset of (REAL 2) proofend; Lm7: for s1, s2, t1, t2 being Real holds { |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) } is Subset of (REAL 2) proofend; Lm8: for s1, s2, t1, t2 being Real holds { |[s,t]| where s, t is Real : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) } is Subset of (REAL 2) proofend; theorem :: JORDAN1:6 canceled; theorem Th7: :: JORDAN1:7 for s1, s2, t1, t2 being Real holds { |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) } = (( { |[s3,t3]| where s3, t3 is Real : s1 < s3 } /\ { |[s4,t4]| where s4, t4 is Real : s4 < s2 } ) /\ { |[s5,t5]| where s5, t5 is Real : t1 < t5 } ) /\ { |[s6,t6]| where s6, t6 is Real : t6 < t2 } proofend; theorem Th8: :: JORDAN1:8 for s1, s2, t1, t2 being Real holds { |[s,t]| where s, t is Real : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) } = (( { |[s3,t3]| where s3, t3 is Real : s3 < s1 } \/ { |[s4,t4]| where s4, t4 is Real : t4 < t1 } ) \/ { |[s5,t5]| where s5, t5 is Real : s2 < s5 } ) \/ { |[s6,t6]| where s6, t6 is Real : t2 < t6 } proofend; theorem Th9: :: JORDAN1:9 for s1, t1, s2, t2 being Real for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) } holds P is convex proofend; theorem :: JORDAN1:10 canceled; theorem Th11: :: JORDAN1:11 for s1 being Real for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : s1 < s } holds P is convex proofend; theorem :: JORDAN1:12 canceled; theorem Th13: :: JORDAN1:13 for s2 being Real for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : s < s2 } holds P is convex proofend; theorem :: JORDAN1:14 canceled; theorem Th15: :: JORDAN1:15 for t1 being Real for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : t1 < t } holds P is convex proofend; theorem :: JORDAN1:16 canceled; theorem Th17: :: JORDAN1:17 for t2 being Real for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : t < t2 } holds P is convex proofend; theorem :: JORDAN1:18 canceled; theorem Th19: :: JORDAN1:19 for s1, t1, s2, t2 being Real for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) } holds P is connected proofend; Lm9: TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def_8; theorem Th20: :: JORDAN1:20 for s1 being Real for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : s1 < s } holds P is open proofend; theorem Th21: :: JORDAN1:21 for s1 being Real for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : s1 > s } holds P is open proofend; theorem Th22: :: JORDAN1:22 for s1 being Real for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : s1 < t } holds P is open proofend; theorem Th23: :: JORDAN1:23 for s1 being Real for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : s1 > t } holds P is open proofend; theorem Th24: :: JORDAN1:24 for s1, t1, s2, t2 being Real for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) } holds P is open proofend; theorem Th25: :: JORDAN1:25 for s1, t1, s2, t2 being Real for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) } holds P is open proofend; theorem Th26: :: JORDAN1:26 for s1, t1, s2, t2 being Real for P, Q being Subset of (TOP-REAL 2) st P = { |[sa,ta]| where sa, ta is Real : ( s1 < sa & sa < s2 & t1 < ta & ta < t2 ) } & Q = { |[sb,tb]| where sb, tb is Real : ( not s1 <= sb or not sb <= s2 or not t1 <= tb or not tb <= t2 ) } holds P misses Q proofend; theorem Th27: :: JORDAN1:27 for s1, s2, t1, t2 being Real holds { p where p is Point of (TOP-REAL 2) : ( s1 < p `1 & p `1 < s2 & t1 < p `2 & p `2 < t2 ) } = { |[sa,ta]| where sa, ta is Real : ( s1 < sa & sa < s2 & t1 < ta & ta < t2 ) } proofend; theorem Th28: :: JORDAN1:28 for s1, s2, t1, t2 being Real holds { qc where qc is Point of (TOP-REAL 2) : ( not s1 <= qc `1 or not qc `1 <= s2 or not t1 <= qc `2 or not qc `2 <= t2 ) } = { |[sb,tb]| where sb, tb is Real : ( not s1 <= sb or not sb <= s2 or not t1 <= tb or not tb <= t2 ) } proofend; theorem Th29: :: JORDAN1:29 for s1, s2, t1, t2 being Real holds { p0 where p0 is Point of (TOP-REAL 2) : ( s1 < p0 `1 & p0 `1 < s2 & t1 < p0 `2 & p0 `2 < t2 ) } is Subset of (TOP-REAL 2) proofend; theorem Th30: :: JORDAN1:30 for s1, s2, t1, t2 being Real holds { pq where pq is Point of (TOP-REAL 2) : ( not s1 <= pq `1 or not pq `1 <= s2 or not t1 <= pq `2 or not pq `2 <= t2 ) } is Subset of (TOP-REAL 2) proofend; theorem Th31: :: JORDAN1:31 for s1, t1, s2, t2 being Real for P being Subset of (TOP-REAL 2) st P = { p0 where p0 is Point of (TOP-REAL 2) : ( s1 < p0 `1 & p0 `1 < s2 & t1 < p0 `2 & p0 `2 < t2 ) } holds P is convex proofend; theorem Th32: :: JORDAN1:32 for s1, t1, s2, t2 being Real for P being Subset of (TOP-REAL 2) st P = { pq where pq is Point of (TOP-REAL 2) : ( not s1 <= pq `1 or not pq `1 <= s2 or not t1 <= pq `2 or not pq `2 <= t2 ) } holds P is connected proofend; theorem Th33: :: JORDAN1:33 for s1, t1, s2, t2 being Real for P being Subset of (TOP-REAL 2) st P = { p0 where p0 is Point of (TOP-REAL 2) : ( s1 < p0 `1 & p0 `1 < s2 & t1 < p0 `2 & p0 `2 < t2 ) } holds P is open proofend; theorem Th34: :: JORDAN1:34 for s1, t1, s2, t2 being Real for P being Subset of (TOP-REAL 2) st P = { pq where pq is Point of (TOP-REAL 2) : ( not s1 <= pq `1 or not pq `1 <= s2 or not t1 <= pq `2 or not pq `2 <= t2 ) } holds P is open proofend; theorem Th35: :: JORDAN1:35 for s1, t1, s2, t2 being Real for P, Q being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : ( s1 < p `1 & p `1 < s2 & t1 < p `2 & p `2 < t2 ) } & Q = { qc where qc is Point of (TOP-REAL 2) : ( not s1 <= qc `1 or not qc `1 <= s2 or not t1 <= qc `2 or not qc `2 <= t2 ) } holds P misses Q proofend; theorem Th36: :: JORDAN1:36 for s1, t1, s2, t2 being Real for P, P1, P2 being Subset of (TOP-REAL 2) st s1 < s2 & t1 < t2 & P = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = s1 & p `2 <= t2 & p `2 >= t1 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) or ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ) } & P1 = { pa where pa is Point of (TOP-REAL 2) : ( s1 < pa `1 & pa `1 < s2 & t1 < pa `2 & pa `2 < t2 ) } & P2 = { pb where pb is Point of (TOP-REAL 2) : ( not s1 <= pb `1 or not pb `1 <= s2 or not t1 <= pb `2 or not pb `2 <= t2 ) } holds ( P ` = P1 \/ P2 & P ` <> {} & P1 misses P2 & ( for P1A, P2B being Subset of ((TOP-REAL 2) | (P `)) st P1A = P1 & P2B = P2 holds ( P1A is a_component & P2B is a_component ) ) ) proofend; Lm10: for s1, t1, s2, t2 being Real for P, P1 being Subset of (TOP-REAL 2) st s1 < s2 & t1 < t2 & P = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = s1 & p `2 <= t2 & p `2 >= t1 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) or ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ) } & P1 = { pa where pa is Point of (TOP-REAL 2) : ( s1 < pa `1 & pa `1 < s2 & t1 < pa `2 & pa `2 < t2 ) } holds Cl P1 = P \/ P1 proofend; Lm11: for s1, t1, s2, t2 being Real for P, P2 being Subset of (TOP-REAL 2) st s1 < s2 & t1 < t2 & P = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = s1 & p `2 <= t2 & p `2 >= t1 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) or ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ) } & P2 = { pb where pb is Point of (TOP-REAL 2) : ( not s1 <= pb `1 or not pb `1 <= s2 or not t1 <= pb `2 or not pb `2 <= t2 ) } holds Cl P2 = P \/ P2 proofend; theorem Th37: :: JORDAN1:37 for s1, t1, s2, t2 being Real for P, P1, P2 being Subset of (TOP-REAL 2) st s1 < s2 & t1 < t2 & P = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = s1 & p `2 <= t2 & p `2 >= t1 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) or ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ) } & P1 = { pa where pa is Point of (TOP-REAL 2) : ( s1 < pa `1 & pa `1 < s2 & t1 < pa `2 & pa `2 < t2 ) } & P2 = { pb where pb is Point of (TOP-REAL 2) : ( not s1 <= pb `1 or not pb `1 <= s2 or not t1 <= pb `2 or not pb `2 <= t2 ) } holds ( P = (Cl P1) \ P1 & P = (Cl P2) \ P2 ) proofend; theorem Th38: :: JORDAN1:38 for s1, s2, t1, t2 being Real for P, P1 being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = s1 & p `2 <= t2 & p `2 >= t1 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) or ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ) } & P1 = { pa where pa is Point of (TOP-REAL 2) : ( s1 < pa `1 & pa `1 < s2 & t1 < pa `2 & pa `2 < t2 ) } holds P1 c= [#] ((TOP-REAL 2) | (P `)) proofend; theorem :: JORDAN1:39 for s1, s2, t1, t2 being Real for P, P1 being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = s1 & p `2 <= t2 & p `2 >= t1 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) or ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ) } & P1 = { pa where pa is Point of (TOP-REAL 2) : ( s1 < pa `1 & pa `1 < s2 & t1 < pa `2 & pa `2 < t2 ) } holds P1 is Subset of ((TOP-REAL 2) | (P `)) proofend; theorem Th40: :: JORDAN1:40 for s1, s2, t1, t2 being Real for P, P2 being Subset of (TOP-REAL 2) st s1 < s2 & t1 < t2 & P = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = s1 & p `2 <= t2 & p `2 >= t1 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) or ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ) } & P2 = { pb where pb is Point of (TOP-REAL 2) : ( not s1 <= pb `1 or not pb `1 <= s2 or not t1 <= pb `2 or not pb `2 <= t2 ) } holds P2 c= [#] ((TOP-REAL 2) | (P `)) proofend; theorem :: JORDAN1:41 for s1, s2, t1, t2 being Real for P, P2 being Subset of (TOP-REAL 2) st s1 < s2 & t1 < t2 & P = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = s1 & p `2 <= t2 & p `2 >= t1 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) or ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ) } & P2 = { pb where pb is Point of (TOP-REAL 2) : ( not s1 <= pb `1 or not pb `1 <= s2 or not t1 <= pb `2 or not pb `2 <= t2 ) } holds P2 is Subset of ((TOP-REAL 2) | (P `)) proofend; begin :: :: The Jordan's property :: definition let S be Subset of (TOP-REAL 2); attrS is Jordan means :Def2: :: JORDAN1:def 2 ( S ` <> {} & ex A1, A2 being Subset of (TOP-REAL 2) st ( S ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & ( for C1, C2 being Subset of ((TOP-REAL 2) | (S `)) st C1 = A1 & C2 = A2 holds ( C1 is a_component & C2 is a_component ) ) ) ); end; :: deftheorem Def2 defines Jordan JORDAN1:def_2_:_ for S being Subset of (TOP-REAL 2) holds ( S is Jordan iff ( S ` <> {} & ex A1, A2 being Subset of (TOP-REAL 2) st ( S ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & ( for C1, C2 being Subset of ((TOP-REAL 2) | (S `)) st C1 = A1 & C2 = A2 holds ( C1 is a_component & C2 is a_component ) ) ) ) ); theorem :: JORDAN1:42 for S being Subset of (TOP-REAL 2) st S is Jordan holds ( S ` <> {} & ex A1, A2 being Subset of (TOP-REAL 2) ex C1, C2 being Subset of ((TOP-REAL 2) | (S `)) st ( S ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & C1 = A1 & C2 = A2 & C1 is a_component & C2 is a_component & ( for C3 being Subset of ((TOP-REAL 2) | (S `)) holds ( not C3 is a_component or C3 = C1 or C3 = C2 ) ) ) ) proofend; theorem :: JORDAN1:43 for s1, s2, t1, t2 being Real for P being Subset of (TOP-REAL 2) st s1 < s2 & t1 < t2 & P = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = s1 & p `2 <= t2 & p `2 >= t1 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) or ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ) } holds P is Jordan proofend; theorem :: JORDAN1:44 for s1, t1, s2, t2 being Real for P, P2 being Subset of (TOP-REAL 2) st s1 < s2 & t1 < t2 & P = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = s1 & p `2 <= t2 & p `2 >= t1 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) or ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ) } & P2 = { pb where pb is Point of (TOP-REAL 2) : ( not s1 <= pb `1 or not pb `1 <= s2 or not t1 <= pb `2 or not pb `2 <= t2 ) } holds Cl P2 = P \/ P2 by Lm11; theorem :: JORDAN1:45 for s1, t1, s2, t2 being Real for P, P1 being Subset of (TOP-REAL 2) st s1 < s2 & t1 < t2 & P = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = s1 & p `2 <= t2 & p `2 >= t1 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) or ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ) } & P1 = { pa where pa is Point of (TOP-REAL 2) : ( s1 < pa `1 & pa `1 < s2 & t1 < pa `2 & pa `2 < t2 ) } holds Cl P1 = P \/ P1 by Lm10; :: Moved from JORDAN1H, AK, 22.02.2006 theorem :: JORDAN1:46 for p, q being Point of (TOP-REAL 2) holds (LSeg (p,q)) \ {p,q} is convex proofend; Lm12: for x0, y0 being Real for P being Subset of (TOP-REAL 2) st P = { |[x,y0]| where x is Real : x <= x0 } holds P is convex proofend; Lm13: for x0, y0 being Real for P being Subset of (TOP-REAL 2) st P = { |[x0,y]| where y is Real : y <= y0 } holds P is convex proofend; Lm14: for x0, y0 being Real for P being Subset of (TOP-REAL 2) st P = { |[x,y0]| where x is Real : x >= x0 } holds P is convex proofend; Lm15: for x0, y0 being Real for P being Subset of (TOP-REAL 2) st P = { |[x0,y]| where y is Real : y >= y0 } holds P is convex proofend; registration let p be Point of (TOP-REAL 2); cluster north_halfline p -> convex ; coherence north_halfline p is convex proofend; cluster east_halfline p -> convex ; coherence east_halfline p is convex proofend; cluster south_halfline p -> convex ; coherence south_halfline p is convex proofend; cluster west_halfline p -> convex ; coherence west_halfline p is convex proofend; end;