:: The Topological Space ${\calE}^2_{\rm T}$. Arcs, Line Segments and Special Polygonal Arcs :: by Agata Darmochwa{\l} and Yatsuka Nakamura :: :: Received November 21, 1991 :: Copyright (c) 1991-2012 Association of Mizar Users begin scheme :: TOPREAL1:sch 1 FraenkelAlt{ F1() -> non empty set , P1[ set ], P2[ set ] } : { v where v is Element of F1() : ( P1[v] or P2[v] ) } = { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } proofend; definition let T be TopSpace; let p1, p2 be Point of T; let P be Subset of T; predP is_an_arc_of p1,p2 means :Def1: :: TOPREAL1:def 1 ex f being Function of I[01],(T | P) st ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ); end; :: deftheorem Def1 defines is_an_arc_of TOPREAL1:def_1_:_ for T being TopSpace for p1, p2 being Point of T for P being Subset of T holds ( P is_an_arc_of p1,p2 iff ex f being Function of I[01],(T | P) st ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) ); theorem Th1: :: TOPREAL1:1 for T being TopSpace for P being Subset of T for p1, p2 being Point of T st P is_an_arc_of p1,p2 holds ( p1 in P & p2 in P ) proofend; theorem Th2: :: TOPREAL1:2 for T being T_2 TopSpace for P, Q being Subset of T for p1, p2, q1 being Point of T st P is_an_arc_of p1,p2 & Q is_an_arc_of p2,q1 & P /\ Q = {p2} holds P \/ Q is_an_arc_of p1,q1 proofend; definition func R^2-unit_square -> Subset of (TOP-REAL 2) equals :: TOPREAL1:def 2 ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|))); coherence ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|))) is Subset of (TOP-REAL 2) ; end; :: deftheorem defines R^2-unit_square TOPREAL1:def_2_:_ R^2-unit_square = ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|))); Lm1: for n being Nat for p, p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) holds LSeg (p1,p) c= LSeg (p1,p2) proofend; theorem :: TOPREAL1:3 for p1, p2, p being Point of (TOP-REAL 2) st p1 `1 <= p2 `1 & p in LSeg (p1,p2) holds ( p1 `1 <= p `1 & p `1 <= p2 `1 ) proofend; theorem :: TOPREAL1:4 for p1, p2, p being Point of (TOP-REAL 2) st p1 `2 <= p2 `2 & p in LSeg (p1,p2) holds ( p1 `2 <= p `2 & p `2 <= p2 `2 ) proofend; theorem Th5: :: TOPREAL1:5 for n being Nat for p, p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) holds LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) proofend; theorem Th6: :: TOPREAL1:6 for n being Nat for p1, p2, q1, q2 being Point of (TOP-REAL n) st q1 in LSeg (p1,p2) & q2 in LSeg (p1,p2) holds LSeg (q1,q2) c= LSeg (p1,p2) proofend; theorem :: TOPREAL1:7 for n being Nat for p, q, p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) & q in LSeg (p1,p2) holds LSeg (p1,p2) = ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2)) proofend; theorem :: TOPREAL1:8 for n being Nat for p, p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) holds (LSeg (p1,p)) /\ (LSeg (p,p2)) = {p} proofend; Lm2: for T being TopSpace holds ( T is T_2 iff TopStruct(# the carrier of T, the topology of T #) is T_2 ) proofend; registration let n be Nat; cluster the carrier of (TOP-REAL n) -> functional ; coherence the carrier of (TOP-REAL n) is functional proofend; end; theorem Th9: :: TOPREAL1:9 for n being Nat for p1, p2 being Point of (TOP-REAL n) st p1 <> p2 holds LSeg (p1,p2) is_an_arc_of p1,p2 proofend; registration let n be Nat; cluster TOP-REAL n -> T_2 ; coherence TOP-REAL n is T_2 proofend; end; theorem Th10: :: TOPREAL1:10 for n being Nat for P being Subset of (TOP-REAL n) for p1, p2, q1 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & P /\ (LSeg (p2,q1)) = {p2} holds P \/ (LSeg (p2,q1)) is_an_arc_of p1,q1 proofend; theorem Th11: :: TOPREAL1:11 for n being Nat for P being Subset of (TOP-REAL n) for p1, p2, q1 being Point of (TOP-REAL n) st P is_an_arc_of p2,p1 & (LSeg (q1,p2)) /\ P = {p2} holds (LSeg (q1,p2)) \/ P is_an_arc_of q1,p1 proofend; theorem :: TOPREAL1:12 for n being Nat for p1, p2, q1 being Point of (TOP-REAL n) st ( p1 <> p2 or p2 <> q1 ) & (LSeg (p1,p2)) /\ (LSeg (p2,q1)) = {p2} holds (LSeg (p1,p2)) \/ (LSeg (p2,q1)) is_an_arc_of p1,q1 proofend; theorem Th13: :: TOPREAL1:13 ( LSeg (|[0,0]|,|[0,1]|) = { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = 0 & p1 `2 <= 1 & p1 `2 >= 0 ) } & LSeg (|[0,1]|,|[1,1]|) = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 1 ) } & LSeg (|[0,0]|,|[1,0]|) = { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 <= 1 & q1 `1 >= 0 & q1 `2 = 0 ) } & LSeg (|[1,0]|,|[1,1]|) = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = 1 & q2 `2 <= 1 & q2 `2 >= 0 ) } ) proofend; theorem :: TOPREAL1:14 R^2-unit_square = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) or ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) or ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) or ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) ) } proofend; registration cluster R^2-unit_square -> non empty ; coherence not R^2-unit_square is empty ; end; theorem :: TOPREAL1:15 (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {|[0,1]|} proofend; theorem :: TOPREAL1:16 (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {|[1,0]|} proofend; theorem Th17: :: TOPREAL1:17 (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {|[0,0]|} proofend; theorem Th18: :: TOPREAL1:18 (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {|[1,1]|} proofend; theorem :: TOPREAL1:19 LSeg (|[0,0]|,|[1,0]|) misses LSeg (|[0,1]|,|[1,1]|) proofend; theorem Th20: :: TOPREAL1:20 LSeg (|[0,0]|,|[0,1]|) misses LSeg (|[1,0]|,|[1,1]|) proofend; definition let n be Nat; let f be FinSequence of (TOP-REAL n); let i be Nat; func LSeg (f,i) -> Subset of (TOP-REAL n) equals :Def3: :: TOPREAL1:def 3 LSeg ((f /. i),(f /. (i + 1))) if ( 1 <= i & i + 1 <= len f ) otherwise {} ; coherence ( ( 1 <= i & i + 1 <= len f implies LSeg ((f /. i),(f /. (i + 1))) is Subset of (TOP-REAL n) ) & ( ( not 1 <= i or not i + 1 <= len f ) implies {} is Subset of (TOP-REAL n) ) ) proofend; correctness consistency for b1 being Subset of (TOP-REAL n) holds verum; ; end; :: deftheorem Def3 defines LSeg TOPREAL1:def_3_:_ for n being Nat for f being FinSequence of (TOP-REAL n) for i being Nat holds ( ( 1 <= i & i + 1 <= len f implies LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) ) & ( ( not 1 <= i or not i + 1 <= len f ) implies LSeg (f,i) = {} ) ); theorem Th21: :: TOPREAL1:21 for n, i being Nat for f being FinSequence of (TOP-REAL n) st 1 <= i & i + 1 <= len f holds ( f /. i in LSeg (f,i) & f /. (i + 1) in LSeg (f,i) ) proofend; definition let n be Nat; let f be FinSequence of (TOP-REAL n); func L~ f -> Subset of (TOP-REAL n) equals :: TOPREAL1:def 4 union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; coherence union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } is Subset of (TOP-REAL n) proofend; end; :: deftheorem defines L~ TOPREAL1:def_4_:_ for n being Nat for f being FinSequence of (TOP-REAL n) holds L~ f = union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; theorem Th22: :: TOPREAL1:22 for n being Nat for f being FinSequence of (TOP-REAL n) holds ( ( len f = 0 or len f = 1 ) iff L~ f = {} ) proofend; theorem Th23: :: TOPREAL1:23 for n being Nat for f being FinSequence of (TOP-REAL n) st len f >= 2 holds L~ f <> {} proofend; definition let IT be FinSequence of (TOP-REAL 2); attrIT is special means :: TOPREAL1:def 5 for i being Nat st 1 <= i & i + 1 <= len IT & not (IT /. i) `1 = (IT /. (i + 1)) `1 holds (IT /. i) `2 = (IT /. (i + 1)) `2 ; attrIT is unfolded means :Def6: :: TOPREAL1:def 6 for i being Nat st 1 <= i & i + 2 <= len IT holds (LSeg (IT,i)) /\ (LSeg (IT,(i + 1))) = {(IT /. (i + 1))}; attrIT is s.n.c. means :Def7: :: TOPREAL1:def 7 for i, j being Nat st i + 1 < j holds LSeg (IT,i) misses LSeg (IT,j); end; :: deftheorem defines special TOPREAL1:def_5_:_ for IT being FinSequence of (TOP-REAL 2) holds ( IT is special iff for i being Nat st 1 <= i & i + 1 <= len IT & not (IT /. i) `1 = (IT /. (i + 1)) `1 holds (IT /. i) `2 = (IT /. (i + 1)) `2 ); :: deftheorem Def6 defines unfolded TOPREAL1:def_6_:_ for IT being FinSequence of (TOP-REAL 2) holds ( IT is unfolded iff for i being Nat st 1 <= i & i + 2 <= len IT holds (LSeg (IT,i)) /\ (LSeg (IT,(i + 1))) = {(IT /. (i + 1))} ); :: deftheorem Def7 defines s.n.c. TOPREAL1:def_7_:_ for IT being FinSequence of (TOP-REAL 2) holds ( IT is s.n.c. iff for i, j being Nat st i + 1 < j holds LSeg (IT,i) misses LSeg (IT,j) ); definition let f be FinSequence of (TOP-REAL 2); attrf is being_S-Seq means :Def8: :: TOPREAL1:def 8 ( f is one-to-one & len f >= 2 & f is unfolded & f is s.n.c. & f is special ); end; :: deftheorem Def8 defines being_S-Seq TOPREAL1:def_8_:_ for f being FinSequence of (TOP-REAL 2) holds ( f is being_S-Seq iff ( f is one-to-one & len f >= 2 & f is unfolded & f is s.n.c. & f is special ) ); theorem Th24: :: TOPREAL1:24 ex f1, f2 being FinSequence of (TOP-REAL 2) st ( f1 is being_S-Seq & f2 is being_S-Seq & R^2-unit_square = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {|[0,0]|,|[1,1]|} & f1 /. 1 = |[0,0]| & f1 /. (len f1) = |[1,1]| & f2 /. 1 = |[0,0]| & f2 /. (len f2) = |[1,1]| ) proofend; theorem Th25: :: TOPREAL1:25 for h being FinSequence of (TOP-REAL 2) st h is being_S-Seq holds L~ h is_an_arc_of h /. 1,h /. (len h) proofend; definition let P be Subset of (TOP-REAL 2); attrP is being_S-P_arc means :Def9: :: TOPREAL1:def 9 ex f being FinSequence of (TOP-REAL 2) st ( f is being_S-Seq & P = L~ f ); end; :: deftheorem Def9 defines being_S-P_arc TOPREAL1:def_9_:_ for P being Subset of (TOP-REAL 2) holds ( P is being_S-P_arc iff ex f being FinSequence of (TOP-REAL 2) st ( f is being_S-Seq & P = L~ f ) ); theorem Th26: :: TOPREAL1:26 for P1 being Subset of (TOP-REAL 2) st P1 is being_S-P_arc holds P1 <> {} proofend; registration cluster being_S-P_arc -> non empty for Element of K10( the carrier of (TOP-REAL 2)); coherence for b1 being Subset of (TOP-REAL 2) st b1 is being_S-P_arc holds not b1 is empty by Th26; end; theorem :: TOPREAL1:27 ex P1, P2 being non empty Subset of (TOP-REAL 2) st ( P1 is being_S-P_arc & P2 is being_S-P_arc & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {|[0,0]|,|[1,1]|} ) proofend; theorem Th28: :: TOPREAL1:28 for P being Subset of (TOP-REAL 2) st P is being_S-P_arc holds ex p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 proofend; theorem :: TOPREAL1:29 for P being Subset of (TOP-REAL 2) st P is being_S-P_arc holds ex f being Function of I[01],((TOP-REAL 2) | P) st f is being_homeomorphism proofend; scheme :: TOPREAL1:sch 2 TRSubsetEx{ F1() -> Nat, P1[ set ] } : ex A being Subset of (TOP-REAL F1()) st for p being Point of (TOP-REAL F1()) holds ( p in A iff P1[p] ) proofend; scheme :: TOPREAL1:sch 3 TRSubsetUniq{ F1() -> Nat, P1[ set ] } : for A, B being Subset of (TOP-REAL F1()) st ( for p being Point of (TOP-REAL F1()) holds ( p in A iff P1[p] ) ) & ( for p being Point of (TOP-REAL F1()) holds ( p in B iff P1[p] ) ) holds A = B proofend; definition let p be Point of (TOP-REAL 2); func north_halfline p -> Subset of (TOP-REAL 2) means :Def10: :: TOPREAL1:def 10 for x being Point of (TOP-REAL 2) holds ( x in it iff ( x `1 = p `1 & x `2 >= p `2 ) ); existence ex b1 being Subset of (TOP-REAL 2) st for x being Point of (TOP-REAL 2) holds ( x in b1 iff ( x `1 = p `1 & x `2 >= p `2 ) ) proofend; uniqueness for b1, b2 being Subset of (TOP-REAL 2) st ( for x being Point of (TOP-REAL 2) holds ( x in b1 iff ( x `1 = p `1 & x `2 >= p `2 ) ) ) & ( for x being Point of (TOP-REAL 2) holds ( x in b2 iff ( x `1 = p `1 & x `2 >= p `2 ) ) ) holds b1 = b2 proofend; func east_halfline p -> Subset of (TOP-REAL 2) means :Def11: :: TOPREAL1:def 11 for x being Point of (TOP-REAL 2) holds ( x in it iff ( x `1 >= p `1 & x `2 = p `2 ) ); existence ex b1 being Subset of (TOP-REAL 2) st for x being Point of (TOP-REAL 2) holds ( x in b1 iff ( x `1 >= p `1 & x `2 = p `2 ) ) proofend; uniqueness for b1, b2 being Subset of (TOP-REAL 2) st ( for x being Point of (TOP-REAL 2) holds ( x in b1 iff ( x `1 >= p `1 & x `2 = p `2 ) ) ) & ( for x being Point of (TOP-REAL 2) holds ( x in b2 iff ( x `1 >= p `1 & x `2 = p `2 ) ) ) holds b1 = b2 proofend; func south_halfline p -> Subset of (TOP-REAL 2) means :Def12: :: TOPREAL1:def 12 for x being Point of (TOP-REAL 2) holds ( x in it iff ( x `1 = p `1 & x `2 <= p `2 ) ); existence ex b1 being Subset of (TOP-REAL 2) st for x being Point of (TOP-REAL 2) holds ( x in b1 iff ( x `1 = p `1 & x `2 <= p `2 ) ) proofend; uniqueness for b1, b2 being Subset of (TOP-REAL 2) st ( for x being Point of (TOP-REAL 2) holds ( x in b1 iff ( x `1 = p `1 & x `2 <= p `2 ) ) ) & ( for x being Point of (TOP-REAL 2) holds ( x in b2 iff ( x `1 = p `1 & x `2 <= p `2 ) ) ) holds b1 = b2 proofend; func west_halfline p -> Subset of (TOP-REAL 2) means :Def13: :: TOPREAL1:def 13 for x being Point of (TOP-REAL 2) holds ( x in it iff ( x `1 <= p `1 & x `2 = p `2 ) ); existence ex b1 being Subset of (TOP-REAL 2) st for x being Point of (TOP-REAL 2) holds ( x in b1 iff ( x `1 <= p `1 & x `2 = p `2 ) ) proofend; uniqueness for b1, b2 being Subset of (TOP-REAL 2) st ( for x being Point of (TOP-REAL 2) holds ( x in b1 iff ( x `1 <= p `1 & x `2 = p `2 ) ) ) & ( for x being Point of (TOP-REAL 2) holds ( x in b2 iff ( x `1 <= p `1 & x `2 = p `2 ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def10 defines north_halfline TOPREAL1:def_10_:_ for p being Point of (TOP-REAL 2) for b2 being Subset of (TOP-REAL 2) holds ( b2 = north_halfline p iff for x being Point of (TOP-REAL 2) holds ( x in b2 iff ( x `1 = p `1 & x `2 >= p `2 ) ) ); :: deftheorem Def11 defines east_halfline TOPREAL1:def_11_:_ for p being Point of (TOP-REAL 2) for b2 being Subset of (TOP-REAL 2) holds ( b2 = east_halfline p iff for x being Point of (TOP-REAL 2) holds ( x in b2 iff ( x `1 >= p `1 & x `2 = p `2 ) ) ); :: deftheorem Def12 defines south_halfline TOPREAL1:def_12_:_ for p being Point of (TOP-REAL 2) for b2 being Subset of (TOP-REAL 2) holds ( b2 = south_halfline p iff for x being Point of (TOP-REAL 2) holds ( x in b2 iff ( x `1 = p `1 & x `2 <= p `2 ) ) ); :: deftheorem Def13 defines west_halfline TOPREAL1:def_13_:_ for p being Point of (TOP-REAL 2) for b2 being Subset of (TOP-REAL 2) holds ( b2 = west_halfline p iff for x being Point of (TOP-REAL 2) holds ( x in b2 iff ( x `1 <= p `1 & x `2 = p `2 ) ) ); theorem :: TOPREAL1:30 for p being Point of (TOP-REAL 2) holds north_halfline p = { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 >= p `2 ) } proofend; theorem Th31: :: TOPREAL1:31 for p being Point of (TOP-REAL 2) holds north_halfline p = { |[(p `1),r]| where r is Element of REAL : r >= p `2 } proofend; theorem :: TOPREAL1:32 for p being Point of (TOP-REAL 2) holds east_halfline p = { q where q is Point of (TOP-REAL 2) : ( q `1 >= p `1 & q `2 = p `2 ) } proofend; theorem Th33: :: TOPREAL1:33 for p being Point of (TOP-REAL 2) holds east_halfline p = { |[r,(p `2)]| where r is Element of REAL : r >= p `1 } proofend; theorem :: TOPREAL1:34 for p being Point of (TOP-REAL 2) holds south_halfline p = { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 <= p `2 ) } proofend; theorem Th35: :: TOPREAL1:35 for p being Point of (TOP-REAL 2) holds south_halfline p = { |[(p `1),r]| where r is Element of REAL : r <= p `2 } proofend; theorem :: TOPREAL1:36 for p being Point of (TOP-REAL 2) holds west_halfline p = { q where q is Point of (TOP-REAL 2) : ( q `1 <= p `1 & q `2 = p `2 ) } proofend; theorem Th37: :: TOPREAL1:37 for p being Point of (TOP-REAL 2) holds west_halfline p = { |[r,(p `2)]| where r is Element of REAL : r <= p `1 } proofend; registration let p be Point of (TOP-REAL 2); cluster north_halfline p -> non empty ; coherence not north_halfline p is empty proofend; cluster east_halfline p -> non empty ; coherence not east_halfline p is empty proofend; cluster south_halfline p -> non empty ; coherence not south_halfline p is empty proofend; cluster west_halfline p -> non empty ; coherence not west_halfline p is empty proofend; end; :: Moved from JORDAN1C, AK, 23.02.2006 theorem :: TOPREAL1:38 for p being Point of (TOP-REAL 2) holds ( p in west_halfline p & p in east_halfline p & p in north_halfline p & p in south_halfline p ) proofend;