Volume 14, 2002

University of Bialystok

Copyright (c) 2002 Association of Mizar Users

### The abstract of the Mizar article:

### On the Decompositions of Intervals and Simple Closed Curves

**by****Adam Grabowski**- Received August 7, 2002
- MML identifier: BORSUK_4

- [ Mizar article, MML identifier index ]

environ vocabulary BOOLE, TOPREAL1, EUCLID, ARYTM_1, PRE_TOPC, COMPTS_1, SEQ_1, TOPREAL2, RELAT_2, BORSUK_1, SUBSET_1, RCOMP_1, TOPS_2, TOPMETR, CONNSP_1, ARYTM_3, SQUARE_1, RELAT_1, ORDINAL2, LATTICES, T_0TOPSP, SEQ_2, INTEGRA1, REALSET1, FUNCT_1, BORSUK_4, PARTFUN1, TREAL_1, FUNCT_4, ARYTM, JORDAN1; notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, SQUARE_1, RELAT_1, FUNCT_1, PARTFUN1, REALSET1, FUNCT_2, STRUCT_0, PRE_TOPC, COMPTS_1, FUNCT_4, RCOMP_1, EUCLID, TOPREAL1, TOPREAL2, SEQ_4, T_0TOPSP, TREAL_1, CONNSP_1, BORSUK_1, BORSUK_3, TSEP_1, RCOMP_2, JORDAN1, TOPMETR, PSCOMP_1, INTEGRA1, TOPS_2; constructors REALSET1, JORDAN2C, TOPS_2, TOPREAL2, TOPREAL1, CONNSP_1, RCOMP_2, PSCOMP_1, INTEGRA1, TMAP_1, BORSUK_3, COMPTS_1, YELLOW_8, PARTFUN1, LIMFUNC1, SPPOL_1, TOPGRP_1, TREAL_1, DOMAIN_1, XCMPLX_0, MEMBERED, JORDAN1; clusters XREAL_0, RELSET_1, REVROT_1, TOPREAL6, STRUCT_0, PRE_TOPC, BORSUK_2, REALSET1, INTEGRA1, TEX_1, TEX_2, JORDAN1B, YELLOW13, EUCLID, MEMBERED, ZFMISC_1; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; begin :: Preliminaries definition cluster -> non trivial Simple_closed_curve; end; definition let T be non empty TopSpace; cluster non empty compact connected Subset of T; end; definition cluster -> real Element of I[01]; end; theorem :: BORSUK_4:1 for X being non empty set, A, B being non empty Subset of X st A c< B holds ex p being Element of X st p in B & A c= B \ {p}; theorem :: BORSUK_4:2 for X being non empty set, A being non empty Subset of X holds A is trivial iff ex x being Element of X st A = {x}; definition let T be non trivial 1-sorted; cluster non trivial Subset of T; end; theorem :: BORSUK_4:3 for X being non trivial set, p being set ex q being Element of X st q <> p; definition let X be non trivial set; cluster non trivial Subset of X; end; theorem :: BORSUK_4:4 for T being non trivial set, X being non trivial Subset of T, p being set ex q being Element of T st q in X & q <> p; 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 } holds f +* g is one-to-one; theorem :: BORSUK_4:6 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:7 for n being Nat, A being non empty 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:8 for n being Nat, a,b being Point of TOP-REAL n holds LSeg (a,b) is convex; theorem :: BORSUK_4:9 for s1, s3, s4, l being real number st s1 <= s3 & s1 < s4 & 0 <= l & l <= 1 holds s1 <= (1-l) * s3+l*s4; theorem :: BORSUK_4:10 for x being set, a, b being real number st a <= b & x in [. a, b .] holds x in ]. a, b .[ or x = a or x = b; theorem :: BORSUK_4:11 for a, b, c, d being real number st ].a,b.[ meets [.c,d.] holds b > c; theorem :: BORSUK_4:12 for a, b, c, d being real number st b <= c holds [. a, b .] misses ]. c, d .[; theorem :: BORSUK_4:13 for a, b, c, d being real number st b <= c holds ]. a, b .[ misses [. c, d .]; theorem :: BORSUK_4:14 for a, b, c, d being real number st a < b & [.a,b.] c= [.c,d.] holds c <= a & b <= d; theorem :: BORSUK_4:15 for a, b, c, d being real number st a < b & ].a,b.[ c= [.c,d.] holds c <= a & b <= d; theorem :: BORSUK_4:16 for a, b, c, d being real number st a < b & ].a,b.[ c= [.c,d.] holds [.a,b.] c= [.c,d.]; theorem :: BORSUK_4:17 for A being Subset of I[01], a, b being real number st a < b & A = ].a,b.[ holds [.a,b.] c= the carrier of I[01]; theorem :: BORSUK_4:18 for A being Subset of I[01], a, b being real number st a < b & A = ].a,b.] holds [.a,b.] c= the carrier of I[01]; theorem :: BORSUK_4:19 for A being Subset of I[01], a, b being real number st a < b & A = [.a,b.[ holds [.a,b.] c= the carrier of I[01]; theorem :: BORSUK_4:20 for a, b being real number st a <> b holds Cl ].a,b.] = [.a,b.]; theorem :: BORSUK_4:21 for a, b being real number st a <> b holds Cl [.a,b.[ = [.a,b.]; theorem :: BORSUK_4:22 for A being Subset of I[01], a, b being real number st a < b & A = ].a,b.[ holds Cl A = [.a,b.]; theorem :: BORSUK_4:23 for A being Subset of I[01], a, b being real number st a < b & A = ].a,b.] holds Cl A = [.a,b.]; theorem :: BORSUK_4:24 for A being Subset of I[01], a, b being real number st a < b & A = [.a,b.[ holds Cl A = [.a,b.]; theorem :: BORSUK_4:25 for a,b being real number st a < b holds [.a,b.] <> ].a,b.]; theorem :: BORSUK_4:26 for a, b being real number holds [.a,b.[ misses {b} & ].a,b.] misses {a}; theorem :: BORSUK_4:27 for a, b being real number st a <= b holds [. a, b .] \ { a } = ]. a, b .]; theorem :: BORSUK_4:28 for a, b being real number st a <= b holds [. a, b .] \ { b } = [. a, b .[; theorem :: BORSUK_4:29 for a, b, c being real number st a < b & b < c holds ]. a, b .] /\ [. b, c .[ = { b }; theorem :: BORSUK_4:30 for a, b, c being real number holds [. a, b .[ misses [. b, c .] & [. a, b .] misses ]. b, c .]; theorem :: BORSUK_4:31 for a, b, c being real number st a <= b & b <= c holds [.a,c.] \ {b} = [.a,b.[ \/ ].b,c.]; theorem :: BORSUK_4:32 for A being Subset of I[01], a, b being real number st a <= b & A = [.a,b.] holds 0 <= a & b <= 1; theorem :: BORSUK_4:33 for A, B being Subset of I[01], a, b, c being real number st a < b & b < c & A = [.a,b.[ & B = ].b,c.] holds A, B are_separated; theorem :: BORSUK_4:34 for a, b being real number st a <= b holds [. a, b .] = [. a, b .[ \/ { b }; theorem :: BORSUK_4:35 for a, b being real number st a <= b holds [. a, b .] = { a } \/ ]. a, b .]; theorem :: BORSUK_4:36 for a, b, c, d being real number st a <= b & b < c & c <= d holds [. a, d .] = [. a, b .] \/ ]. b, c .[ \/ [. c, d .]; theorem :: BORSUK_4:37 for a, b, c, d being real number st a <= b & b < c & c <= d holds [. a, d .] \ ([. a, b .] \/ [. c, d .]) = ]. b, c .[; theorem :: BORSUK_4:38 for a, b, c being real number st a < b & b < c holds ]. a, b .] \/ ]. b, c .[ = ]. a, c .[; theorem :: BORSUK_4:39 for a, b, c being real number st a < b & b < c holds [. b, c .[ c= ]. a, c .[; theorem :: BORSUK_4:40 for a, b, c being real number st a < b & b < c holds ]. a, b .] \/ [. b, c .[ = ]. a, c .[; theorem :: BORSUK_4:41 for a, b, c being real number st a < b & b < c holds ]. a, c .[ \ ]. a, b .] = ]. b, c .[; theorem :: BORSUK_4:42 for a, b, c being real number st a < b & b < c holds ]. a, c .[ \ [. b, c .[ = ]. a, b .[; theorem :: BORSUK_4:43 for p1, p2 being Point of I[01] holds [. p1, p2 .] is Subset of I[01]; theorem :: BORSUK_4:44 for a, b being Point of I[01] holds ]. a, b .[ is Subset of I[01]; begin :: Decompositions of Intervals theorem :: BORSUK_4:45 for p being real number holds {p} is closed-interval Subset of REAL; theorem :: BORSUK_4:46 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:47 for A being non empty connected Subset of I[01], a, b being real number st a in A & b in A holds [.a,b.] c= A; theorem :: BORSUK_4:48 for a, b being real number, A being Subset of I[01] st a <= b & A = [.a,b.] holds A is closed; theorem :: BORSUK_4:49 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:50 for X being Subset of I[01], X' being Subset of REAL st X' = X holds X' is bounded_above bounded_below; theorem :: BORSUK_4:51 for X being Subset of I[01], X' being Subset of REAL, x being real number st x in X' & X' = X holds inf X' <= x & x <= sup X'; theorem :: BORSUK_4:52 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:53 for C being closed-interval Subset of REAL holds inf C <= sup C; theorem :: BORSUK_4:54 for C being non empty compact connected Subset of I[01], C' being Subset of REAL st C = C' & [. inf C', sup C' .] c= C' holds [. inf C', sup C' .] = C'; theorem :: BORSUK_4:55 for C being non empty compact connected Subset of I[01] holds C is closed-interval Subset of REAL; theorem :: BORSUK_4:56 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 non empty SubSpace of I[01] means :: BORSUK_4:def 1 the carrier of it = ]. 0,1 .[; end; theorem :: BORSUK_4:57 for A being Subset of I[01] st A = the carrier of I(01) holds I(01) = I[01] | A; theorem :: BORSUK_4:58 the carrier of I(01) = (the carrier of I[01]) \ {0,1}; theorem :: BORSUK_4:59 I(01) is open SubSpace of I[01]; theorem :: BORSUK_4:60 for r being real number holds r in the carrier of I(01) iff 0 < r & r < 1; theorem :: BORSUK_4:61 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:62 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:63 for D being Simple_closed_curve holds (TOP-REAL 2) | R^2-unit_square, (TOP-REAL 2) | D are_homeomorphic; theorem :: BORSUK_4:64 for D being non empty Subset of TOP-REAL 2, p1, p2 being Point of TOP-REAL 2 st D is_an_arc_of p1, p2 holds I(01), (TOP-REAL 2) | (D \ {p1,p2}) are_homeomorphic; theorem :: BORSUK_4:65 for D being Subset of TOP-REAL 2, p1, p2 being Point of TOP-REAL 2 st D is_an_arc_of p1, p2 holds I[01], (TOP-REAL 2) | D are_homeomorphic; theorem :: BORSUK_4:66 for p1, p2 being Point of TOP-REAL 2 st p1 <> p2 holds I[01], (TOP-REAL 2) | LSeg (p1, p2) are_homeomorphic; theorem :: BORSUK_4:67 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:68 for A being non empty Subset of TOP-REAL 2, p, q being Point of TOP-REAL 2, 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 map of I[01]|E, (TOP-REAL 2)|A st E = [. a, b .] & f is_homeomorphism & f.a = p & f.b = q; theorem :: BORSUK_4:69 for A being TopSpace, B being non empty TopSpace, f being map of A, B, C being TopSpace, X being Subset of A st f is continuous & C is SubSpace of B holds for h being map of A|X, C st h = f|X holds h is continuous; theorem :: BORSUK_4:70 for X being Subset of I[01], a, b being Point of I[01] st a <= b & X = ]. a, b .[ holds X is open; theorem :: BORSUK_4:71 for X being Subset of I(01), a, b being Point of I[01] st a <= b & X = ]. a, b .[ holds X is open; theorem :: BORSUK_4:72 for X being non empty Subset of I(01), a being Point of I[01] st 0 < a & X = ]. 0, a .] holds X is closed; theorem :: BORSUK_4:73 for X being non empty Subset of I(01), a being Point of I[01] st X = [. a, 1 .[ holds X is closed; theorem :: BORSUK_4:74 for A being non empty Subset of TOP-REAL 2, p, q being Point of TOP-REAL 2, 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 map of I(01)|E, (TOP-REAL 2)|(A \ {p}) st E = ]. a, b .] & f is_homeomorphism & f.b = q; theorem :: BORSUK_4:75 for A being non empty Subset of TOP-REAL 2, p, q being Point of TOP-REAL 2, 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 map of I(01)|E, (TOP-REAL 2)|(A \ {q}) st E = [. a, b .[ & f is_homeomorphism & f.a = p; theorem :: BORSUK_4:76 for A, B being non empty Subset of TOP-REAL 2, p, q being Point of TOP-REAL 2 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 2) | ((A \ {p}) \/ (B \ {p})) are_homeomorphic; theorem :: BORSUK_4:77 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:78 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:79 for C being non empty Subset of TOP-REAL 2, 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 2)|C are_homeomorphic holds ex s1, s2 being Point of TOP-REAL 2 st C is_an_arc_of s1,s2; theorem :: BORSUK_4:80 for Dp being non empty Subset of TOP-REAL 2, f being map of (TOP-REAL 2) | Dp, I(01), C being non empty Subset of TOP-REAL 2 st f is_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:81 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});

Back to top