Journal of Formalized Mathematics
Volume 3, 1991
University of Bialystok
Copyright (c) 1991 Association of Mizar Users

### The Topological Space \$\calE^2_\rmT\$. Simple Closed Curves

by
Agata Darmochwal, and
Yatsuka Nakamura

MML identifier: TOPREAL2
[ Mizar article, MML identifier index ]

```environ

vocabulary PRE_TOPC, EUCLID, FINSEQ_1, TOPREAL1, MCART_1, BOOLE, COMPTS_1,
BORSUK_1, RELAT_1, TOPS_2, ORDINAL2, SUBSET_1, FUNCT_1, RCOMP_1,
PCOMPS_1, FUNCT_4, TOPREAL2, FINSEQ_4;
notation TARSKI, XBOOLE_0, SUBSET_1, XREAL_0, RELAT_1, FUNCT_1, FUNCT_2,
FUNCT_4, STRUCT_0, GRCAT_1, PRE_TOPC, TOPS_2, COMPTS_1, RCOMP_1,
FINSEQ_1, FINSEQ_4, PCOMPS_1, EUCLID, TOPMETR, TOPREAL1;
constructors TOPS_2, COMPTS_1, RCOMP_1, TOPMETR, TOPREAL1, FINSEQ_4, GRCAT_1,
XCMPLX_0, MEMBERED, XBOOLE_0;
clusters SUBSET_1, FUNCT_1, PRE_TOPC, RELSET_1, STRUCT_0, EUCLID, BORSUK_1,
TOPREAL1, XREAL_0, XBOOLE_0, MEMBERED, ZFMISC_1;
requirements NUMERALS, REAL, BOOLE, SUBSET;

begin

reserve a for set;
reserve p,p1,p2,q,q1,q2 for Point of TOP-REAL 2;
reserve h1,h2 for FinSequence of TOP-REAL 2;

theorem :: TOPREAL2:1
p1 <> p2 & p1 in R^2-unit_square & p2 in R^2-unit_square implies
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};

theorem :: TOPREAL2:2
R^2-unit_square is compact;

theorem :: TOPREAL2:3
for Q, P being non empty Subset of TOP-REAL 2
for f being map of (TOP-REAL 2)|Q, (TOP-REAL 2)|P st f is_homeomorphism &
Q is_an_arc_of q1,q2 holds
for p1, p2 st p1 = f.q1 & p2 = f.q2 holds P is_an_arc_of p1,p2;

definition let P be Subset of TOP-REAL 2;
attr P is being_simple_closed_curve means
:: TOPREAL2:def 1

ex f being map of (TOP-REAL 2)|R^2-unit_square, (TOP-REAL 2)|P
st f is_homeomorphism;
synonym P is_simple_closed_curve;
end;

definition
cluster R^2-unit_square -> being_simple_closed_curve;
end;

definition
cluster being_simple_closed_curve Subset of TOP-REAL 2;
end;

definition
mode Simple_closed_curve is being_simple_closed_curve Subset of TOP-REAL 2;
end;

theorem :: TOPREAL2:4
for P being non empty Subset of TOP-REAL 2 st
P is_simple_closed_curve ex p1,p2 st p1 <> p2 & p1 in P & p2 in P;

theorem :: TOPREAL2:5
for P being non empty Subset of TOP-REAL 2 holds
P is_simple_closed_curve iff
(ex p1,p2 st p1 <> p2 & p1 in P & p2 in P)
& for p1,p2 st p1 <> p2 & p1 in P & p2 in P
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};

theorem :: TOPREAL2:6
for P being non empty Subset of TOP-REAL 2 holds
P is_simple_closed_curve iff
ex p1,p2 being Point of TOP-REAL 2,
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};
```