:: The Topological Space ${\calE}^2_{\rm T}$. Simple Closed Curves :: by Agata Darmochwa{\l} and Yatsuka Nakamura :: :: Received December 30, 1991 :: Copyright (c) 1991-2012 Association of Mizar Users begin Lm1: now__::_thesis:_for_x,_X_being_set_st_not_x_in_X_holds_ {x}_/\_X_=_{} let x, X be set ; ::_thesis: ( not x in X implies {x} /\ X = {} ) assume not x in X ; ::_thesis: {x} /\ X = {} then {x} misses X by ZFMISC_1:50; hence {x} /\ X = {} by XBOOLE_0:def_7; ::_thesis: verum end; Lm2: (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {} by TOPREAL1:19, XBOOLE_0:def_7; Lm3: (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {} by TOPREAL1:20, XBOOLE_0:def_7; set p00 = |[0,0]|; set p01 = |[0,1]|; set p10 = |[1,0]|; set p11 = |[1,1]|; set L1 = LSeg (|[0,0]|,|[0,1]|); set L2 = LSeg (|[0,1]|,|[1,1]|); set L3 = LSeg (|[0,0]|,|[1,0]|); set L4 = LSeg (|[1,0]|,|[1,1]|); Lm4: |[0,0]| `1 = 0 by EUCLID:52; Lm5: |[0,0]| `2 = 0 by EUCLID:52; Lm6: |[0,1]| `1 = 0 by EUCLID:52; Lm7: |[0,1]| `2 = 1 by EUCLID:52; Lm8: |[1,0]| `1 = 1 by EUCLID:52; Lm9: |[1,0]| `2 = 0 by EUCLID:52; Lm10: |[1,1]| `1 = 1 by EUCLID:52; Lm11: |[1,1]| `2 = 1 by EUCLID:52; Lm12: not |[0,0]| in LSeg (|[1,0]|,|[1,1]|) by Lm4, Lm8, Lm10, TOPREAL1:3; Lm13: not |[0,0]| in LSeg (|[0,1]|,|[1,1]|) by Lm5, Lm7, Lm11, TOPREAL1:4; Lm14: not |[0,1]| in LSeg (|[0,0]|,|[1,0]|) by Lm5, Lm7, Lm9, TOPREAL1:4; Lm15: not |[0,1]| in LSeg (|[1,0]|,|[1,1]|) by Lm6, Lm8, Lm10, TOPREAL1:3; Lm16: not |[1,0]| in LSeg (|[0,0]|,|[0,1]|) by Lm4, Lm6, Lm8, TOPREAL1:3; Lm17: not |[1,0]| in LSeg (|[0,1]|,|[1,1]|) by Lm7, Lm9, Lm11, TOPREAL1:4; Lm18: not |[1,1]| in LSeg (|[0,0]|,|[0,1]|) by Lm4, Lm6, Lm10, TOPREAL1:3; Lm19: not |[1,1]| in LSeg (|[0,0]|,|[1,0]|) by Lm5, Lm9, Lm11, TOPREAL1:4; Lm20: |[0,0]| in LSeg (|[0,0]|,|[0,1]|) by RLTOPSP1:68; Lm21: |[0,0]| in LSeg (|[0,0]|,|[1,0]|) by RLTOPSP1:68; Lm22: |[0,1]| in LSeg (|[0,0]|,|[0,1]|) by RLTOPSP1:68; Lm23: |[0,1]| in LSeg (|[0,1]|,|[1,1]|) by RLTOPSP1:68; Lm24: |[1,0]| in LSeg (|[0,0]|,|[1,0]|) by RLTOPSP1:68; Lm25: |[1,0]| in LSeg (|[1,0]|,|[1,1]|) by RLTOPSP1:68; Lm26: |[1,1]| in LSeg (|[0,1]|,|[1,1]|) by RLTOPSP1:68; Lm27: |[1,1]| in LSeg (|[1,0]|,|[1,1]|) by RLTOPSP1:68; set L = { 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 ) ) } ; Lm28: |[0,0]| in { 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 ) ) } by Lm4, Lm5; Lm29: |[1,1]| in { 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 ) ) } by Lm10, Lm11; Lm30: for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p2 in R^2-unit_square & p1 in LSeg (|[0,0]|,|[0,1]|) holds ex P1, P2 being non empty Subset of (TOP-REAL 2) st ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} ) proofend; Lm31: for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p2 in R^2-unit_square & p1 in LSeg (|[0,1]|,|[1,1]|) holds ex P1, P2 being non empty Subset of (TOP-REAL 2) st ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} ) proofend; Lm32: for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p2 in R^2-unit_square & p1 in LSeg (|[0,0]|,|[1,0]|) holds ex P1, P2 being non empty Subset of (TOP-REAL 2) st ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} ) proofend; Lm33: for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p2 in R^2-unit_square & p1 in LSeg (|[1,0]|,|[1,1]|) holds ex P1, P2 being non empty Subset of (TOP-REAL 2) st ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} ) proofend; theorem Th1: :: TOPREAL2:1 for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in R^2-unit_square & p2 in R^2-unit_square holds ex P1, P2 being non empty Subset of (TOP-REAL 2) st ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} ) proofend; theorem Th2: :: TOPREAL2:2 R^2-unit_square is compact proofend; theorem Th3: :: TOPREAL2:3 for q1, q2 being Point of (TOP-REAL 2) for Q, P being non empty Subset of (TOP-REAL 2) for f being Function of ((TOP-REAL 2) | Q),((TOP-REAL 2) | P) st f is being_homeomorphism & Q is_an_arc_of q1,q2 holds for p1, p2 being Point of (TOP-REAL 2) st p1 = f . q1 & p2 = f . q2 holds P is_an_arc_of p1,p2 proofend; definition let P be Subset of (TOP-REAL 2); attrP is being_simple_closed_curve means :Def1: :: TOPREAL2:def 1 ex f being Function of ((TOP-REAL 2) | R^2-unit_square),((TOP-REAL 2) | P) st f is being_homeomorphism ; end; :: deftheorem Def1 defines being_simple_closed_curve TOPREAL2:def_1_:_ for P being Subset of (TOP-REAL 2) holds ( P is being_simple_closed_curve iff ex f being Function of ((TOP-REAL 2) | R^2-unit_square),((TOP-REAL 2) | P) st f is being_homeomorphism ); registration cluster R^2-unit_square -> being_simple_closed_curve ; coherence R^2-unit_square is being_simple_closed_curve proofend; end; registration cluster functional non empty being_simple_closed_curve for Element of K19( the carrier of (TOP-REAL 2)); existence ex b1 being Subset of (TOP-REAL 2) st ( b1 is being_simple_closed_curve & not b1 is empty ) proofend; end; definition mode Simple_closed_curve is being_simple_closed_curve Subset of (TOP-REAL 2); end; theorem Th4: :: TOPREAL2:4 for P being non empty Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds ex p1, p2 being Point of (TOP-REAL 2) st ( p1 <> p2 & p1 in P & p2 in P ) proofend; Lm34: for p1, p2 being Point of (TOP-REAL 2) for P, P1, P2 being non empty Subset of (TOP-REAL 2) st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} holds P is being_simple_closed_curve proofend; theorem Th5: :: TOPREAL2:5 for P being non empty Subset of (TOP-REAL 2) holds ( P is being_simple_closed_curve iff ( ex p1, p2 being Point of (TOP-REAL 2) st ( p1 <> p2 & p1 in P & p2 in P ) & ( for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in P & p2 in P holds ex P1, P2 being non empty Subset of (TOP-REAL 2) st ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} ) ) ) ) proofend; theorem :: TOPREAL2:6 for P being non empty Subset of (TOP-REAL 2) holds ( P is being_simple_closed_curve iff ex p1, p2 being Point of (TOP-REAL 2) ex P1, P2 being non empty Subset of (TOP-REAL 2) st ( p1 <> p2 & p1 in P & p2 in P & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} ) ) proofend; Lm35: for S, T being 1-sorted for f being Function of S,T st S is empty & rng f = [#] T holds T is empty proofend; Lm36: for S, T being 1-sorted for f being Function of S,T st T is empty & dom f = [#] S holds S is empty proofend; Lm37: for S, T being TopStruct st ex f being Function of S,T st f is being_homeomorphism holds ( S is empty iff T is empty ) proofend; registration cluster being_simple_closed_curve -> non empty compact for Element of K19( the carrier of (TOP-REAL 2)); coherence for b1 being Subset of (TOP-REAL 2) st b1 is being_simple_closed_curve holds ( not b1 is empty & b1 is compact ) proofend; end;