:: The Topological Space ${\calE}^2_{\rm T}$. Simple Closed Curves
:: by Agata Darmochwa{\l} and Yatsuka Nakamura
::
:: Copyright (c) 1991-2019 Association of Mizar Users

Lm1: for x, X being set st not x in X holds
{x} /\ X = {}

by ;

Lm2: (LSeg (,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {}
by ;

Lm3: (LSeg (,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {}
by ;

set p00 = ;

set p01 = |[0,1]|;

set p10 = |[1,0]|;

set p11 = |[1,1]|;

set L1 = LSeg (,|[0,1]|);

set L2 = LSeg (|[0,1]|,|[1,1]|);

set L3 = LSeg (,|[1,0]|);

set L4 = LSeg (|[1,0]|,|[1,1]|);

Lm4:
by EUCLID:52;

Lm5:
by EUCLID:52;

Lm6:
by EUCLID:52;

Lm7: |[0,1]| 2 = 1
by EUCLID:52;

Lm8: |[1,0]| 1 = 1
by EUCLID:52;

Lm9:
by EUCLID:52;

Lm10: |[1,1]| 1 = 1
by EUCLID:52;

Lm11: |[1,1]| 2 = 1
by EUCLID:52;

Lm12: not in LSeg (|[1,0]|,|[1,1]|)
by ;

Lm13: not in LSeg (|[0,1]|,|[1,1]|)
by ;

Lm14: not |[0,1]| in LSeg (,|[1,0]|)
by ;

Lm15: not |[0,1]| in LSeg (|[1,0]|,|[1,1]|)
by ;

Lm16: not |[1,0]| in LSeg (,|[0,1]|)
by ;

Lm17: not |[1,0]| in LSeg (|[0,1]|,|[1,1]|)
by ;

Lm18: not |[1,1]| in LSeg (,|[0,1]|)
by ;

Lm19: not |[1,1]| in LSeg (,|[1,0]|)
by ;

Lm20: in LSeg (,|[0,1]|)
by RLTOPSP1:68;

Lm21: in LSeg (,|[1,0]|)
by RLTOPSP1:68;

Lm22: |[0,1]| in LSeg (,|[0,1]|)
by RLTOPSP1:68;

Lm23: |[0,1]| in LSeg (|[0,1]|,|[1,1]|)
by RLTOPSP1:68;

Lm24: |[1,0]| in LSeg (,|[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 () : ( ( 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: in { p where p is Point of () : ( ( 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 ;

Lm29: |[1,1]| in { p where p is Point of () : ( ( 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 ;

Lm30: for p1, p2 being Point of () st p1 <> p2 & p2 in R^2-unit_square & p1 in LSeg (,|[0,1]|) holds
ex P1, P2 being non empty Subset of () 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} )

proof end;

Lm31: for p1, p2 being Point of () 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 () 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} )

proof end;

Lm32: for p1, p2 being Point of () st p1 <> p2 & p2 in R^2-unit_square & p1 in LSeg (,|[1,0]|) holds
ex P1, P2 being non empty Subset of () 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} )

proof end;

Lm33: for p1, p2 being Point of () 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 () 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} )

proof end;

theorem Th1: :: TOPREAL2:1
for p1, p2 being Point of () st p1 <> p2 & p1 in R^2-unit_square & p2 in R^2-unit_square holds
ex P1, P2 being non empty Subset of () 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} )
proof end;

theorem Th2: :: TOPREAL2:2
proof end;

theorem Th3: :: TOPREAL2:3
for q1, q2 being Point of ()
for Q, P being non empty Subset of ()
for f being Function of (() | Q),(() | P) st f is being_homeomorphism & Q is_an_arc_of q1,q2 holds
for p1, p2 being Point of () st p1 = f . q1 & p2 = f . q2 holds
P is_an_arc_of p1,p2
proof end;

definition
let P be Subset of ();
attr P is being_simple_closed_curve means :: TOPREAL2:def 1
ex f being Function of (),(() | P) st f is being_homeomorphism ;
end;

:: deftheorem defines being_simple_closed_curve TOPREAL2:def 1 :
for P being Subset of () holds
( P is being_simple_closed_curve iff ex f being Function of (),(() | P) st f is being_homeomorphism );

registration end;

registration
cluster functional non empty being_simple_closed_curve for Element of K19( the carrier of ());
existence
ex b1 being Subset of () st
( b1 is being_simple_closed_curve & not b1 is empty )
proof end;
end;

definition end;

theorem Th4: :: TOPREAL2:4
for P being non empty Subset of () st P is being_simple_closed_curve holds
ex p1, p2 being Point of () st
( p1 <> p2 & p1 in P & p2 in P )
proof end;

Lm34: for p1, p2 being Point of ()
for P, P1, P2 being non empty Subset of () 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

proof end;

theorem Th5: :: TOPREAL2:5
for P being non empty Subset of () holds
( P is being_simple_closed_curve iff ( ex p1, p2 being Point of () st
( p1 <> p2 & p1 in P & p2 in P ) & ( for p1, p2 being Point of () st p1 <> p2 & p1 in P & p2 in P holds
ex P1, P2 being non empty Subset of () st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} ) ) ) )
proof end;

theorem :: TOPREAL2:6
for P being non empty Subset of () holds
( P is being_simple_closed_curve iff ex p1, p2 being Point of () ex P1, P2 being non empty Subset of () 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} ) )
proof end;

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

proof end;

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

proof end;

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 )

by ;

registration
cluster being_simple_closed_curve -> non empty compact for Element of K19( the carrier of ());
coherence
for b1 being Subset of () st b1 is being_simple_closed_curve holds
( not b1 is empty & b1 is compact )
proof end;
end;