:: On the Decompositions of Intervals and Simple Closed Curves
:: by Adam Grabowski
::
:: Received August 7, 2002
:: Copyright (c) 2002-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, ZFMISC_1, TOPREAL2, PRE_TOPC, EUCLID, XBOOLE_0,
SUBSET_1, TARSKI, STRUCT_0, FUNCT_1, RELAT_1, FUNCT_4, PARTFUN1,
TOPREAL1, XXREAL_0, ARYTM_3, CARD_1, ARYTM_1, BORSUK_1, XXREAL_1,
TOPMETR, CONNSP_1, REAL_1, RELAT_2, RCOMP_1, XXREAL_2, ORDINAL2, SEQ_4,
T_0TOPSP, TOPS_2, RLTOPSP1, TREAL_1, VALUED_1, BORSUK_4, FUNCT_2,
MEASURE5;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
XXREAL_2, XREAL_0, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
DOMAIN_1, RCOMP_1, FUNCT_4, XXREAL_0, STRUCT_0, MEASURE6, PRE_TOPC,
COMPTS_1, RLTOPSP1, EUCLID, TOPREAL1, TOPREAL2, SEQ_4, TREAL_1, CONNSP_1,
BORSUK_1, BORSUK_3, TSEP_1, TOPMETR, MEASURE5, TOPS_2;
constructors FUNCT_4, CONNSP_1, TOPS_2, COMPTS_1, TSEP_1, TOPREAL1, TOPREAL2,
TREAL_1, MEASURE6, BORSUK_3, INTEGRA1, SEQ_4, BINOP_2;
registrations XBOOLE_0, RELSET_1, FUNCT_2, XXREAL_0, XREAL_0, MEMBERED,
RCOMP_1, STRUCT_0, PRE_TOPC, TOPS_1, COMPTS_1, BORSUK_1, EUCLID,
TOPREAL1, TOPREAL2, BORSUK_2, REVROT_1, TOPREAL6, XXREAL_2, TOPMETR,
SUBSET_1, MEASURE5, JORDAN2C, ORDINAL1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
begin :: Preliminaries
registration
cluster -> non trivial for Simple_closed_curve;
end;
::$CT 3
theorem :: BORSUK_4:4
for f, g being Function, a being set st f is one-to-one & g is
one-to-one & dom f /\ dom g = { a } & rng f /\ rng g = { f.a } holds f +* g is
one-to-one;
theorem :: BORSUK_4:5
for f, g being Function, a being set st f is one-to-one & g is
one-to-one & dom f /\ dom g = { a } & rng f /\ rng g = { f.a } & f.a = g.a
holds (f +* g)" = f" +* g";
theorem :: BORSUK_4:6
for n being Element of NAT, A being Subset of TOP-REAL n, p, q
being Point of TOP-REAL n st A is_an_arc_of p, q holds A \ {p} is non empty;
theorem :: BORSUK_4:7
for s1, s3, s4, l being Real st s1 <= s3 & s1 < s4 & 0 <= l & l
<= 1 holds s1 <= (1-l) * s3+l*s4;
theorem :: BORSUK_4:8
for A being Subset of I[01], a, b being Real st a < b & A
= ].a,b.[ holds [.a,b.] c= the carrier of I[01];
theorem :: BORSUK_4:9
for A being Subset of I[01], a, b being Real st a < b & A
= ].a,b.] holds [.a,b.] c= the carrier of I[01];
theorem :: BORSUK_4:10
for A being Subset of I[01], a, b being Real st a < b & A
= [.a,b.[ holds [.a,b.] c= the carrier of I[01];
theorem :: BORSUK_4:11
for a, b being Real st a <> b holds Cl ].a,b.] = [.a,b.];
theorem :: BORSUK_4:12
for a, b being Real st a <> b holds Cl [.a,b.[ = [.a,b.];
theorem :: BORSUK_4:13
for A being Subset of I[01], a, b being Real st a < b & A = ].a
,b.[ holds Cl A = [.a,b.];
theorem :: BORSUK_4:14
for A being Subset of I[01], a, b being Real st a < b & A
= ].a,b.] holds Cl A = [.a,b.];
theorem :: BORSUK_4:15
for A being Subset of I[01], a, b being Real st a < b & A
= [.a,b.[ holds Cl A = [.a,b.];
theorem :: BORSUK_4:16
for A being Subset of I[01], a, b being Real st a <= b &
A = [.a,b.] holds 0 <= a & b <= 1;
theorem :: BORSUK_4:17
for A, B being Subset of I[01], a, b, c being Real st a <
b & b < c & A = [.a,b.[ & B = ].b,c.] holds A, B are_separated;
theorem :: BORSUK_4:18
for p1, p2 being Point of I[01] holds [. p1, p2 .] is Subset of I[01];
theorem :: BORSUK_4:19
for a, b being Point of I[01] holds ]. a, b .[ is Subset of I[01];
begin :: Decompositions of Intervals
theorem :: BORSUK_4:20
for p being Real holds {p} is non empty closed_interval Subset of REAL;
theorem :: BORSUK_4:21
for A being non empty connected Subset of I[01], a, b, c being
Point of I[01] st a <= b & b <= c & a in A & c in A holds b in A;
theorem :: BORSUK_4:22
for A being non empty connected Subset of I[01], a, b being Real
st a in A & b in A holds [.a,b.] c= A;
theorem :: BORSUK_4:23
for a, b being Real, A being Subset of I[01] st A = [.a,b
.] holds A is closed;
theorem :: BORSUK_4:24
for p1, p2 being Point of I[01] st p1 <= p2 holds [. p1, p2 .]
is non empty compact connected Subset of I[01];
theorem :: BORSUK_4:25
for X being Subset of I[01], X9 being Subset of REAL st X9 = X
holds X9 is bounded_above bounded_below;
theorem :: BORSUK_4:26
for X being Subset of I[01], X9 being Subset of REAL, x being
Real st x in X9 & X9 = X holds lower_bound X9 <= x &
x <= upper_bound X9;
theorem :: BORSUK_4:27
for A being Subset of REAL, B being Subset of I[01] st A = B
holds A is closed iff B is closed;
theorem :: BORSUK_4:28
for C being non empty closed_interval Subset of REAL
holds lower_bound C <= upper_bound C;
theorem :: BORSUK_4:29
for C being non empty compact connected Subset of I[01], C9
being Subset of REAL st C = C9 &
[. lower_bound C9, upper_bound C9 .] c= C9 holds [. lower_bound C9,
upper_bound C9 .] = C9;
theorem :: BORSUK_4:30
for C being non empty compact connected Subset of I[01] holds C
is non empty closed_interval Subset of REAL;
theorem :: BORSUK_4:31
for C being non empty compact connected Subset of I[01] ex p1,
p2 being Point of I[01] st p1 <= p2 & C = [. p1, p2 .];
begin :: Decompositions of Simple Closed Curves
definition
func I(01) -> strict SubSpace of I[01] means
:: BORSUK_4:def 1
the carrier of it = ]. 0,1 .[;
end;
registration
cluster I(01) -> non empty;
end;
theorem :: BORSUK_4:32
for A being Subset of I[01] st A = the carrier of I(01) holds
I(01) = I[01] | A;
theorem :: BORSUK_4:33
the carrier of I(01) = (the carrier of I[01]) \ {0,1};
registration
cluster I(01) -> open;
end;
theorem :: BORSUK_4:34
I(01) is open;
theorem :: BORSUK_4:35
for r being Real holds r in the carrier of I(01) iff 0 < r & r < 1;
theorem :: BORSUK_4:36
for a, b being Point of I[01] st a < b & b <> 1 holds ]. a, b .]
is non empty Subset of I(01);
theorem :: BORSUK_4:37
for a, b being Point of I[01] st a < b & a <> 0 holds [. a, b .[
is non empty Subset of I(01);
theorem :: BORSUK_4:38
for D being Simple_closed_curve holds (TOP-REAL 2) | R^2-unit_square,
(TOP-REAL 2) | D are_homeomorphic;
theorem :: BORSUK_4:39
for n being Element of NAT, D being non empty Subset of TOP-REAL n, p1
, p2 being Point of TOP-REAL n st D is_an_arc_of p1, p2 holds I(01), (TOP-REAL
n) | (D \ {p1,p2}) are_homeomorphic;
theorem :: BORSUK_4:40
for n being Element of NAT, D being Subset of TOP-REAL n, p1, p2
being Point of TOP-REAL n st D is_an_arc_of p1, p2 holds I[01], (TOP-REAL n) |
D are_homeomorphic;
theorem :: BORSUK_4:41
for n being Element of NAT, p1, p2 being Point of TOP-REAL n st p1 <>
p2 holds I[01], (TOP-REAL n) | LSeg (p1, p2) are_homeomorphic;
theorem :: BORSUK_4:42
for E being Subset of I(01) st (ex p1, p2 being Point of I[01]
st p1 < p2 & E = [. p1,p2 .]) holds I[01], I(01)|E are_homeomorphic;
theorem :: BORSUK_4:43
for n being Element of NAT, A being Subset of TOP-REAL n, p, q
being Point of TOP-REAL n, a, b being Point of I[01] st A is_an_arc_of p, q & a
< b ex E being non empty Subset of I[01], f being Function of I[01]|E, (
TOP-REAL n)|A st E = [. a, b .] & f is being_homeomorphism & f.a = p & f.b = q;
theorem :: BORSUK_4:44
for A being TopSpace, B being non empty TopSpace, f being
Function of A, B, C being TopSpace, X being Subset of A st f is continuous & C
is SubSpace of B holds for h being Function of A|X, C st h = f|X holds h is
continuous;
theorem :: BORSUK_4:45
for X being Subset of I[01], a, b being Point of I[01] st X = ].
a, b .[ holds X is open;
theorem :: BORSUK_4:46
for X being Subset of I(01), a, b being Point of I[01] st X = ].
a, b .[ holds X is open;
theorem :: BORSUK_4:47
for X being Subset of I(01), a being Point of I[01] st X = ]. 0,
a .] holds X is closed;
theorem :: BORSUK_4:48
for X being Subset of I(01), a being Point of I[01] st X = [. a,
1 .[ holds X is closed;
theorem :: BORSUK_4:49
for n being Element of NAT, A being Subset of TOP-REAL n, p, q
being Point of TOP-REAL n, a, b being Point of I[01] st A is_an_arc_of p, q & a
< b & b <> 1 ex E being non empty Subset of I(01), f being Function of I(01)|E,
(TOP-REAL n)|(A \ {p}) st E = ]. a, b .] & f is being_homeomorphism & f.b = q
;
theorem :: BORSUK_4:50
for n being Element of NAT, A being Subset of TOP-REAL n, p, q
being Point of TOP-REAL n, a, b being Point of I[01] st A is_an_arc_of p, q & a
< b & a <> 0 ex E being non empty Subset of I(01), f being Function of I(01)|E,
(TOP-REAL n)|(A \ {q}) st E = [. a, b .[ & f is being_homeomorphism & f.a = p
;
theorem :: BORSUK_4:51
for n being Element of NAT, A, B being Subset of TOP-REAL n, p,
q being Point of TOP-REAL n st A is_an_arc_of p, q & B is_an_arc_of q, p & A /\
B = { p, q } & p <> q holds I(01), (TOP-REAL n) | ((A \ {p}) \/ (B \ {p}))
are_homeomorphic;
theorem :: BORSUK_4:52
for D being Simple_closed_curve, p being Point of TOP-REAL 2 st
p in D holds (TOP-REAL 2) | (D \ {p}), I(01) are_homeomorphic;
theorem :: BORSUK_4:53
for D being Simple_closed_curve, p, q being Point of TOP-REAL 2 st p
in D & q in D holds (TOP-REAL 2) | (D \ {p}), (TOP-REAL 2) | (D \ {q})
are_homeomorphic;
theorem :: BORSUK_4:54
for n being Element of NAT, C being non empty Subset of TOP-REAL
n, E being Subset of I(01) st (ex p1, p2 being Point of I[01] st p1 < p2 & E =
[. p1,p2 .]) & I(01)|E, (TOP-REAL n)|C are_homeomorphic holds ex s1, s2 being
Point of TOP-REAL n st C is_an_arc_of s1,s2;
theorem :: BORSUK_4:55
for Dp being non empty Subset of TOP-REAL 2, f being Function of
(TOP-REAL 2) | Dp, I(01), C being non empty Subset of TOP-REAL 2 st f is
being_homeomorphism & C c= Dp & (ex p1, p2 being Point of I[01] st p1 < p2 & f
.:C = [. p1,p2 .]) holds ex s1, s2 being Point of TOP-REAL 2 st C is_an_arc_of
s1,s2;
theorem :: BORSUK_4:56
for D being Simple_closed_curve, C being non empty compact connected
Subset of TOP-REAL 2 st C c= D holds C = D or (ex p1, p2 being Point of
TOP-REAL 2 st C is_an_arc_of p1,p2) or ex p being Point of TOP-REAL 2 st C = {p
};
begin :: Addenda
theorem :: BORSUK_4:57
for C being non empty compact Subset of I[01] st C c= ].0,1.[
holds ex D being non empty closed_interval Subset of REAL
st C c= D & D c= ].0,1.[ &
lower_bound C = lower_bound D & upper_bound C = upper_bound D;
theorem :: BORSUK_4:58
for C being non empty compact Subset of I[01] st C c= ].0,1.[
holds ex p1, p2 being Point of I[01] st p1 <= p2 & C c= [. p1, p2 .] & [.p1,p2
.] c= ]. 0, 1 .[;
theorem :: BORSUK_4:59
for D being Simple_closed_curve, C being closed Subset of TOP-REAL 2
st C c< D ex p1,p2 being Point of TOP-REAL 2, B being Subset of TOP-REAL 2 st B
is_an_arc_of p1,p2 & C c= B & B c= D;