### The Mizar article:

### Some Lemmas for the Jordan Curve Theorem

**by****Andrzej Trybulec**

- Received August 28, 2000
Copyright (c) 2000 Association of Mizar Users

- MML identifier: JCT_MISC
- [ MML identifier index ]

environ vocabulary BOOLE, TARSKI, FUNCT_1, RELAT_1, SUBSET_1, ARYTM_1, ARYTM, RCOMP_1, ARYTM_3, ORDINAL2, SEQM_3, PROB_1, ABSVALUE, SQUARE_1, FUNCT_3, MCART_1, PRE_TOPC, SETFAM_1, COMPTS_1, SEQ_1, SEQ_2, RELAT_2, PSCOMP_1, LIMFUNC1, CONNSP_1, METRIC_1, SEQ_4, TOPMETR, INTEGRA1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, DTCONSTR, INTEGRA1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, ABSVALUE, BINARITH, SQUARE_1, SEQ_1, SEQ_2, SEQ_4, RCOMP_1, STRUCT_0, PRE_TOPC, COMPTS_1, BORSUK_1, PSCOMP_1, SEQM_3, TOPMETR, LIMFUNC1, CONNSP_1; constructors BINARITH, REAL_1, SEQM_3, COMPTS_1, MCART_1, DTCONSTR, INTEGRA1, RFUNCT_2, ABSVALUE, PSCOMP_1, PARTFUN1, TOPMETR, TSP_1, INT_1, PROB_1, LIMFUNC1, CONNSP_1, MEMBERED; clusters XREAL_0, INT_1, STRUCT_0, PRE_TOPC, RELSET_1, SUBSET_1, INTEGRA1, SEQM_3, PSCOMP_1, BORSUK_1, BORSUK_3, SEQ_1, TOPREAL6, MEMBERED, ZFMISC_1, ORDINAL2; requirements NUMERALS, REAL, SUBSET, BOOLE; definitions TARSKI, RCOMP_1, SEQ_4, XBOOLE_0; theorems AMI_5, JORDAN3, REAL_1, REAL_2, ZFMISC_1, TARSKI, SUBSET_1, MCART_1, FUNCT_2, DTCONSTR, FUNCT_1, RFUNCT_2, RCOMP_1, SEQ_4, SEQM_3, ABSVALUE, TOPREAL5, PSCOMP_1, AXIOMS, GOBOARD7, BORSUK_1, TOPMETR, JORDAN6, UNIFORM1, JORDAN1, PRE_TOPC, SQUARE_1, RELAT_1, SEQ_2, TOPREAL6, TSP_1, SEQ_1, INTEGRA1, CONNSP_1, XREAL_0, LIMFUNC1, PROB_1, FCONT_3, TSEP_1, SETFAM_1, XBOOLE_0, XBOOLE_1, XCMPLX_1; schemes FUNCT_2, PSCOMP_1; begin :: Preliminaries scheme NonEmpty{ A()-> non empty set, F(set)-> set}: { F(a) where a is Element of A(): not contradiction } is non empty proof consider a0 being set such that A1: a0 in A() by XBOOLE_0:def 1; F(a0) in { F(a) where a is Element of A(): not contradiction } by A1; hence thesis; end; canceled 2; theorem Th3: for A,B being set, f being Function st A c= dom f & f.:A c= B holds A c= f"B proof let A,B be set, f being Function; assume A c= dom f; then A1: A c= f"(f.:A) by FUNCT_1:146; assume f.:A c= B; then f"(f.:A) c= f"B by RELAT_1:178; hence A c= f"B by A1,XBOOLE_1:1; end; theorem Th4: for f being Function, A,B being set st A misses B holds f"A misses f"B proof let f be Function, A,B be set; assume A misses B; then A /\ B = {} by XBOOLE_0:def 7; then {} = f"(A /\ B) by RELAT_1:171 .= f"A /\ f"B by FUNCT_1:137; hence f"A misses f"B by XBOOLE_0:def 7; end; theorem Th5: for S,X being set, f being Function of S,X, A being Subset of X st X = {} implies S = {} holds (f"A)` = f"(A`) proof let S,X be set, f be Function of S,X, A be Subset of X such that A1: X = {} implies S = {}; A misses A` by SUBSET_1:26; then A /\ A` = {} by XBOOLE_0:def 7; then f"A /\ f"(A`) = f"({}X) by FUNCT_1:137 .= {} by RELAT_1:171; then A2: f"A misses f"(A`) by XBOOLE_0:def 7; f"A \/ f"(A`) = f"(A \/ A`) by RELAT_1:175 .= f"[#]X by SUBSET_1:25 .= f"X by SUBSET_1:def 4 .= S by A1,FUNCT_2:48 .= [#]S by SUBSET_1:def 4; then (f"A)` /\ (f"(A`))` = ([#]S)` by SUBSET_1:29 .= {}S by SUBSET_1:21; then (f"A)` misses (f"(A`))` by XBOOLE_0:def 7; hence (f"A)` = f"(A`) by A2,SUBSET_1:46; end; theorem Th6: for S being 1-sorted, X being non empty set, f being Function of the carrier of S,X, A being Subset of X holds (f"A)` = f"(A`) by Th5; reserve i,j,m,n for Nat, r,s,r0,s0,t for real number; theorem m <= n implies n-'(n-'m) = m proof assume A1: m <= n; n -' m <= n by JORDAN3:13; then n-'(n-'m) + (n-'m) = n by AMI_5:4 .= m + (n-'m) by A1,AMI_5:4; hence thesis by XCMPLX_1:2; end; canceled; theorem Th9: for a,b being real number st r in [.a,b.] & s in [.a,b.] holds (r + s)/2 in [.a,b.] proof let a,b be real number such that A1: r in [.a,b.] and A2: s in [.a,b.]; reconsider a,b,r,s as Real by XREAL_0:def 1; a <= r & a <= s by A1,A2,TOPREAL5:1; then a+a <= r+s by REAL_1:55; then (a+a)/2 <= (r+s)/2 by REAL_1:73; then A3: a <= (r + s)/2 by XCMPLX_1:65; r <= b & s <= b by A1,A2,TOPREAL5:1; then r+s <= b+b by REAL_1:55; then (r+s)/2 <= (b+b)/2 by REAL_1:73; then (r + s)/2 <= b by XCMPLX_1:65; hence thesis by A3,TOPREAL5:1; end; theorem Th10: for Nseq being increasing Seq_of_Nat, i,j st i <= j holds Nseq.i <= Nseq.j proof let Nseq be increasing Seq_of_Nat; Nseq is non-decreasing by SEQM_3:23; hence thesis by SEQM_3:12; end; theorem Th11: abs(abs(r0-s0)-abs(r-s)) <= abs(r0-r) + abs(s0-s) proof A1: abs(abs(r0-s0) - abs(r-s)) <= abs(r0-s0 - (r-s)) by ABSVALUE:22; r0-s0 - (r-s) = r0-s0 - r + s by XCMPLX_1:37 .= r0-r - s0 + s by XCMPLX_1:21 .= r0-r - (s0-s) by XCMPLX_1:37; then abs(r0-s0 - (r-s)) <= abs(r0-r) + abs(s0-s) by ABSVALUE:19; hence abs(abs(r0-s0)-abs(r-s)) <= abs(r0-r) + abs(s0-s) by A1,AXIOMS:22; end; theorem t in ].r,s.[ implies abs(t) < max(abs(r),abs(s)) proof assume A1: t in ].r,s.[; reconsider r,t,s as Real by XREAL_0:def 1; A2: r < t & t < s by A1,JORDAN6:45; per cases; suppose A3: t >= 0; then A4: t = abs(t) by ABSVALUE:def 1; s > 0 by A1,A3,JORDAN6:45; then abs(t) < abs(s) by A2,A4,ABSVALUE:def 1; hence thesis by SQUARE_1:50; suppose A5: t < 0; then A6: -t = abs(t) by ABSVALUE:def 1; r < 0 by A2,A5,AXIOMS:22; then -r =abs(r) by ABSVALUE:def 1; then abs(t) < abs(r) by A2,A6,REAL_1:50; hence thesis by SQUARE_1:50; end; definition let A,B,C be non empty set; let f be Function of A, [:B,C:]; redefine func pr1 f -> Function of A,B means :Def1: for x being Element of A holds it.x = (f.x)`1; coherence proof A1: dom pr1 f = dom f by DTCONSTR:def 2; then A2: dom pr1 f = A by FUNCT_2:def 1; rng pr1 f c= B proof let x be set; assume x in rng pr1 f; then consider y being set such that A3: y in dom pr1 f and A4: x = (pr1 f).y by FUNCT_1:def 5; A5: x = (f.y)`1 by A1,A3,A4,DTCONSTR:def 2; f.y in [:B,C:] by A1,A3,FUNCT_2:7; hence x in B by A5,MCART_1:10; end; hence pr1 f is Function of A,B by A2,FUNCT_2:4; end; compatibility proof let IT be Function of A,B; A6: dom pr1 f = dom f by DTCONSTR:def 2; then A7: dom pr1 f = A by FUNCT_2:def 1; hence IT = pr1 f implies for x being Element of A holds IT.x = (f.x)`1 by A6,DTCONSTR:def 2; assume for x being Element of A holds IT.x = (f.x)`1; then A8: for x being set st x in dom f holds IT.x = (f.x)`1; dom IT = dom f by A6,A7,FUNCT_2:def 1; hence IT = pr1 f by A8,DTCONSTR:def 2; end; func pr2 f -> Function of A,C means :Def2: for x being Element of A holds it.x = (f.x)`2; coherence proof A9: dom pr2 f = dom f by DTCONSTR:def 3; then A10: dom pr2 f = A by FUNCT_2:def 1; rng pr2 f c= C proof let x be set; assume x in rng pr2 f; then consider y being set such that A11: y in dom pr2 f and A12: x = (pr2 f).y by FUNCT_1:def 5; A13: x = (f.y)`2 by A9,A11,A12,DTCONSTR:def 3; f.y in [:B,C:] by A9,A11,FUNCT_2:7; hence x in C by A13,MCART_1:10; end; hence pr2 f is Function of A,C by A10,FUNCT_2:4; end; compatibility proof let IT be Function of A,C; A14: dom pr2 f = dom f by DTCONSTR:def 3; then A15: dom pr2 f = A by FUNCT_2:def 1; hence IT = pr2 f implies for x being Element of A holds IT.x = (f.x)`2 by A14,DTCONSTR:def 3; assume for x being Element of A holds IT.x = (f.x)`2; then A16: for x being set st x in dom f holds IT.x = (f.x)`2; dom IT = dom f by A14,A15,FUNCT_2:def 1; hence IT = pr2 f by A16,DTCONSTR:def 3; end; end; scheme DoubleChoice{ A,B,C() -> non empty set, P[set,set,set]}: ex a being Function of A(), B(), b being Function of A(), C() st for i being Element of A() holds P[i,a.i,b.i] provided A1: for i being Element of A() ex ai being Element of B(), bi being Element of C() st P[i,ai,bi] proof defpred P1[set,set] means P[$1,($2)`1,($2)`2]; A2: for e being Element of A() ex u being Element of [:B(),C():] st P1[e,u] proof let e be Element of A(); consider ai being Element of B(), bi being Element of C() such that A3: P[e,ai,bi] by A1; take [ai,bi]; thus [ai,bi] is Element of [:B(),C():] by ZFMISC_1:106; [ai,bi]`1 = ai & [ai,bi]`2 = bi by MCART_1:7; hence P[e,[ai,bi]`1,[ai,bi]`2] by A3; end; consider f being Function of A(), [:B(),C():] such that A4: for e being Element of A() holds P1[e,f.e] from FuncExD(A2); take pr1 f, pr2 f; let i be Element of A(); (f.i)`1 = (pr1 f).i & (f.i)`2 = (pr2 f).i by Def1,Def2; hence P[i,(pr1 f).i,(pr2 f).i] by A4; end; theorem Th13: for S,T being non empty TopSpace, G being Subset of [:S,T:] st for x being Point of [:S,T:] st x in G ex GS being Subset of S, GT being Subset of T st GS is open & GT is open & x in [:GS,GT:] & [:GS,GT:] c= G holds G is open proof let S,T be non empty TopSpace, G being Subset of [:S,T:] such that A1: for x being Point of [:S,T:] st x in G ex GS being Subset of S, GT being Subset of T st GS is open & GT is open & x in [:GS,GT:] & [:GS,GT:] c= G; set A = {[:GS,GT:] where GS is Subset of S, GT is Subset of T : GS is open & GT is open & [:GS,GT:] c= G }; A c= bool the carrier of [:S,T:] proof let e be set; assume e in A; then consider GS being Subset of S, GT being Subset of T such that A2: e = [:GS,GT:] and GS is open & GT is open & [:GS,GT:] c= G; thus e in bool the carrier of [:S,T:] by A2; end; then reconsider A as Subset-Family of [:S,T:] by SETFAM_1:def 7; reconsider A as Subset-Family of [:S,T:]; for x being set holds x in G iff ex Y being set st x in Y & Y in A proof let x be set; thus x in G implies ex Y being set st x in Y & Y in A proof assume x in G; then consider GS being Subset of S, GT being Subset of T such that A3: GS is open & GT is open & x in [:GS,GT:] & [:GS,GT:] c= G by A1; take Y = [:GS,GT:]; thus x in Y & Y in A by A3; end; given Y being set such that A4: x in Y and A5: Y in A; ex GS being Subset of S, GT being Subset of T st Y = [:GS,GT:] & GS is open & GT is open & [:GS,GT:] c= G by A5; hence x in G by A4; end; then A6: G = union A by TARSKI:def 4; for e being set st e in A ex X1 being Subset of S, Y1 being Subset of T st e = [:X1,Y1:] & X1 is open & Y1 is open proof let e be set; assume e in A; then ex GS being Subset of S, GT being Subset of T st e = [:GS,GT:] & GS is open & GT is open & [:GS,GT:] c= G; hence ex GS being Subset of S, GT being Subset of T st e = [:GS,GT:] & GS is open & GT is open; end; hence G is open by A6,BORSUK_1:45; end; begin :: topological properties of sets of real numbers theorem Th14: for A,B being compact Subset of REAL holds A /\ B is compact proof let A,B be compact Subset of REAL; let s1 be Real_Sequence such that A1: rng s1 c= A /\ B; A /\ B c= A by XBOOLE_1:17; then rng s1 c= A by A1,XBOOLE_1:1; then consider s2 being Real_Sequence such that A2: s2 is_subsequence_of s1 and A3: s2 is convergent and A4: lim s2 in A by RCOMP_1:def 3; rng s2 c= rng s1 by A2,RFUNCT_2:11; then A5: rng s2 c= A /\ B by A1,XBOOLE_1:1; A /\ B c= B by XBOOLE_1:17; then rng s2 c= B by A5,XBOOLE_1:1; then consider s3 being Real_Sequence such that A6: s3 is_subsequence_of s2 and A7: s3 is convergent and A8: lim s3 in B by RCOMP_1:def 3; take s3; thus s3 is_subsequence_of s1 by A2,A6,SEQM_3:48; thus s3 is convergent by A7; lim s3 = lim s2 by A3,A6,SEQ_4:30; hence lim s3 in A /\ B by A4,A8,XBOOLE_0:def 3; end; definition let A be Subset of REAL; attr A is connected means :Def3: for r,s being real number st r in A & s in A holds [.r,s.] c= A; end; theorem for T being non empty TopSpace for f being continuous RealMap of T for A being Subset of T st A is connected holds f.:A is connected proof let T be non empty TopSpace; let f be continuous RealMap of T; let A be Subset of T; assume A1: A is connected; let r,s; assume A2: r in f.:A; then consider p being Point of T such that A3: p in A and A4: r = f.p by FUNCT_2:116; assume A5: s in f.:A; then consider q being Point of T such that A6: q in A and A7: s = f.q by FUNCT_2:116; assume not [.r,s.] c= f.:A; then consider t being Real such that A8: t in [.r,s.] and A9: not t in f.:A by SUBSET_1:7; reconsider r,s,t as Real by XREAL_0:def 1; set P1 = f"left_open_halfline t, Q1 = f"right_open_halfline t, P = P1 /\ A, Q = Q1 /\ A, X = left_open_halfline t \/ right_open_halfline t; reconsider Y = {t} as Subset of REAL; Y` = REAL \ {t} by SUBSET_1:def 5 .= REAL \ [.t,t.] by RCOMP_1:14 .= X by LIMFUNC1:25; then A10: (f"Y)` = f"X by Th6 .= P1 \/ Q1 by RELAT_1:175; A11: A c= f"(f.:A) by FUNCT_2:50; {t} misses f.:A by A9,ZFMISC_1:56; then f"{t} misses f"(f.:A) by Th4; then f"{t} misses A by A11,XBOOLE_1:63; then A c= P1 \/ Q1 by A10,PRE_TOPC:21; then A12: A = A /\ (P1 \/ Q1) by XBOOLE_1:28 .= P \/ Q by XBOOLE_1:23; A13: left_open_halfline t = {r1 where r1 is Real: r1 < t} by PROB_1:def 15; A14: right_open_halfline t = {r1 where r1 is Real: t < r1} by LIMFUNC1:def 3; r <= t & r <> t by A2,A8,A9,TOPREAL5:1; then r < t by AXIOMS:21; then r in left_open_halfline t by A13; then p in P1 by A4,FUNCT_2:46; then A15: P <> {}T by A3,XBOOLE_0:def 3; t <= s & s <> t by A5,A8,A9,TOPREAL5:1; then t < s by AXIOMS:21; then s in right_open_halfline t by A14; then q in Q1 by A7,FUNCT_2:46; then A16: Q <> {}T by A6,XBOOLE_0:def 3; left_open_halfline t is open by FCONT_3:8; then A17: P1 is open by PSCOMP_1:54; right_open_halfline t is open by FCONT_3:7; then A18: Q1 is open by PSCOMP_1:54; A19: P c= P1 by XBOOLE_1:17; A20: Q c= Q1 by XBOOLE_1:17; left_open_halfline t /\ right_open_halfline t = ].t,t.[ by LIMFUNC1:18 .= {} by RCOMP_1:12; then left_open_halfline t misses right_open_halfline t by XBOOLE_0:def 7; then P1 misses Q1 by Th4; then P1 /\ Q1 = {} by XBOOLE_0:def 7; then P1 /\ Q1 misses P \/ Q by XBOOLE_1:65; then P,Q are_separated by A17,A18,A19,A20,TSEP_1:49; hence contradiction by A1,A12,A15,A16,CONNSP_1:16; end; definition let A,B be Subset of REAL; set Y = {abs(r - s) where r is Element of REAL, s is Element of REAL : r in A & s in B}; Y c= REAL proof let e be set; assume e in Y; then ex r,s being Element of REAL st e = abs(r - s) & r in A & s in B; hence thesis; end; then reconsider Y0 = Y as Subset of REAL; func dist(A,B) -> real number means :Def4: ex X being Subset of REAL st X = {abs(r - s) where r is Element of REAL, s is Element of REAL : r in A & s in B} & it = lower_bound X; existence proof take lower_bound Y0; thus thesis; end; uniqueness; commutativity proof let IT be real number, A,B be Subset of REAL; given X0 being Subset of REAL such that A1: X0 = {abs(r - s) where r is Element of REAL, s is Element of REAL : r in A & s in B} and A2: IT = lower_bound X0; set Y = {abs(r - s) where r is Element of REAL, s is Element of REAL : r in B & s in A}; Y c= REAL proof let e be set; assume e in Y; then ex r,s being Element of REAL st e = abs(r - s) & r in B & s in A; hence thesis; end; then reconsider Y0 = Y as Subset of REAL; take Y0; thus Y0 = {abs(r - s) where r is Element of REAL, s is Element of REAL : r in B & s in A}; X0 = Y0 proof thus X0 c= Y0 proof let x be set; assume x in X0; then consider r,s being Element of REAL such that A3: x = abs(r - s) & r in A & s in B by A1; x = abs(s - r) by A3,UNIFORM1:13; hence x in Y0 by A3; end; let x be set; assume x in Y0; then consider r,s being Element of REAL such that A4: x = abs(r - s) & r in B & s in A; x = abs(s - r) by A4,UNIFORM1:13; hence x in X0 by A1,A4; end; hence IT = lower_bound Y0 by A2; end; end; theorem Th16: for A,B being Subset of REAL, r, s st r in A & s in B holds abs(r-s) >= dist(A,B) proof let A,B be Subset of REAL; set Y = {abs(r - s) where r is Element of REAL, s is Element of REAL : r in A & s in B}; Y c= REAL proof let e be set; assume e in Y; then ex r,s being Real st e = abs(r - s) & r in A & s in B; hence thesis; end; then reconsider Y0 = Y as Subset of REAL; A1: dist(A,B) = lower_bound Y0 by Def4; A2: Y0 is bounded_below proof take 0; let r0; assume r0 in Y0; then ex r,s being Real st r0 = abs(r - s) & r in A & s in B; hence 0<=r0 by ABSVALUE:5; end; let r,s; assume r in A & s in B; then abs(r-s) in Y0; hence abs(r-s) >= dist(A,B) by A1,A2,SEQ_4:def 5; end; theorem Th17: for A,B being Subset of REAL, C,D being non empty Subset of REAL st C c= A & D c= B holds dist(A,B) <= dist(C,D) proof let A,B be Subset of REAL, C,D be non empty Subset of REAL such that A1: C c= A and A2: D c= B; set X = {abs(r - s) where r is Element of REAL, s is Element of REAL : r in A & s in B}; X c= REAL proof let e be set; assume e in X; then ex r,s being Real st e = abs(r - s) & r in A & s in B; hence thesis; end; then reconsider X as Subset of REAL; A3: dist(A,B) = lower_bound X by Def4; A4: X is bounded_below proof take 0; let r0; assume r0 in X; then ex r,s being Real st r0 = abs(r - s) & r in A & s in B; hence 0<=r0 by ABSVALUE:5; end; consider r0 being set such that A5: r0 in C by XBOOLE_0:def 1; consider s0 being set such that A6: s0 in D by XBOOLE_0:def 1; set Y = {abs(r - s) where r is Element of REAL, s is Element of REAL : r in C & s in D}; r0 is Real & s0 is Real by A5,A6; then reconsider r0,s0 as real number; A7: abs(r0 - s0) in Y by A5,A6; Y c= REAL proof let e be set; assume e in Y; then ex r,s being Real st e = abs(r - s) & r in C & s in D; hence thesis; end; then reconsider Y as non empty Subset of REAL by A7; A8: dist(C,D) = lower_bound Y by Def4; Y c= X proof let x be set; assume x in Y; then ex r,s being Real st x = abs(r - s) & r in C & s in D; hence x in X by A1,A2; end; hence dist(A,B) <= dist(C,D) by A3,A4,A8,PSCOMP_1:12; end; theorem Th18: for A, B being non empty compact Subset of REAL ex r,s being real number st r in A & s in B & dist(A,B) = abs(r - s) proof let A, B be non empty compact Subset of REAL; reconsider At = A, Bt = B as non empty compact Subset of R^1 by TOPMETR:24,TOPREAL6:81; A1: the carrier of R^1|At = At & the carrier of R^1|Bt = Bt by JORDAN1:1; reconsider AB = [:R^1|At, R^1|Bt:] as compact (non empty TopSpace); defpred P[set,set] means ex r,s being Real st $1 = [r,s] & $2 = abs(r-s); A2: now let x be set; assume x in the carrier of AB; then x in [:A,B:] by A1,BORSUK_1:def 5; then consider r,s being set such that A3: r in REAL & s in REAL and A4: x = [r,s] by ZFMISC_1:103; reconsider r,s as Real by A3; take t = abs(r-s); thus P[x,t] by A4; end; consider f being RealMap of AB such that A5: for x being Element of AB holds P[x,f.x] from NonUniqExRF(A2); for Y being Subset of REAL st Y is open holds f"Y is open proof let Y be Subset of REAL such that A6: Y is open; for x being Point of AB st x in f"Y ex YS being Subset of R^1|At, YT being Subset of R^1|Bt st YS is open & YT is open & x in [:YS,YT:] & [:YS,YT:] c= f"Y proof let x be Point of AB; assume x in f"Y; then f.x in Y by FUNCT_1:def 13; then consider N being Neighbourhood of f.x such that A7: N c= Y by A6,RCOMP_1:39; consider g being real number such that A8: 0 < g and A9: N = ].f.x-g,f.x+g.[ by RCOMP_1:def 7; consider r,s being Real such that A10: x = [r,s] and A11: f.x = abs(r-s) by A5; reconsider a=r-g/2, b=r+g/2, c =s-g/2, d=s+g/2 as Real by XREAL_0:def 1; reconsider S = ].a,b.[, T = ].c,d.[ as Subset of R^1 by TOPMETR:24; S /\ A c= A by XBOOLE_1:17; then reconsider YS = S /\ A as Subset of R^1|At by A1; T /\ B c= B by XBOOLE_1:17; then reconsider YT = T /\ B as Subset of R^1|Bt by A1; take YS, YT; S is open & T is open by JORDAN6:46; hence YS is open & YT is open by A1,TSP_1:def 1; 0 < g/2 by A8,SEQ_2:3; then A12: r in S & s in T by TOPREAL6:20; x in the carrier of AB; then x in [:A,B:] by A1,BORSUK_1:def 5; then r in A & s in B by A10,ZFMISC_1:106; then r in YS & s in YT by A12,XBOOLE_0:def 3; hence x in [:YS,YT:] by A10,ZFMISC_1:106; A13: dom f = the carrier of AB by FUNCT_2:def 1; f.:[:YS,YT:] c= N proof let e be set; assume e in f.:[:YS,YT:]; then consider y being Element of AB such that A14: y in [:YS,YT:] and A15: e = f.y by FUNCT_2:116; consider r1,s1 being Real such that A16: y = [r1,s1] and A17: f.y = abs(r1-s1) by A5; r1 in YS by A14,A16,ZFMISC_1:106; then r1 in ].r-g/2,r+g/2.[ by XBOOLE_0:def 3; then A18: abs(r1-r) < g/2 by RCOMP_1:8; s1 in YT by A14,A16,ZFMISC_1:106; then s1 in ].s-g/2,s+g/2.[ by XBOOLE_0:def 3; then A19: abs(s1-s) < g/2 by RCOMP_1:8; g = g/2 + g/2 by XCMPLX_1:66; then A20: abs(r1-r) + abs(s1-s) < g by A18,A19,REAL_1:67; abs(abs(r1-s1)-abs(r-s)) <= abs(r1-r) + abs(s1-s) by Th11; then abs(abs(r1-s1)-abs(r-s)) < g by A20,AXIOMS:22; hence e in N by A9,A11,A15,A17,RCOMP_1:8; end; then f.:[:YS,YT:] c= Y by A7,XBOOLE_1:1; hence [:YS,YT:] c= f"Y by A13,Th3; end; hence f"Y is open by Th13; end; then reconsider f as continuous RealMap of AB by PSCOMP_1:54; f.:the carrier of AB is with_min by PSCOMP_1:def 15; then inf(f.:the carrier of AB) in f.:the carrier of AB by PSCOMP_1:def 4; then consider x being Element of AB such that A21: x in the carrier of AB and A22: inf(f.:the carrier of AB) = f.x by FUNCT_2:116; A23: x in [:A,B:] by A1,A21,BORSUK_1:def 5; then consider r1,s1 being set such that A24: r1 in REAL & s1 in REAL and A25: x = [r1,s1] by ZFMISC_1:103; r1 is Real & s1 is Real by A24; then reconsider r1,s1 as real number; take r1,s1; thus r1 in A & s1 in B by A23,A25,ZFMISC_1:106; A26: f.:the carrier of AB = {abs(r - s) where r is Element of REAL, s is Element of REAL : r in A & s in B} proof hereby let x be set; assume x in f.:the carrier of AB; then consider y being Element of AB such that A27: y in the carrier of AB and A28: x = f.y by FUNCT_2:116; consider r1,s1 being Real such that A29: y = [r1,s1] and A30: f.y = abs(r1-s1) by A5; [r1,s1] in [:A,B:] by A1,A27,A29,BORSUK_1:def 5; then r1 in A & s1 in B by ZFMISC_1:106; hence x in {abs(r - s) where r is Element of REAL, s is Element of REAL : r in A & s in B} by A28,A30; end; let x be set; assume x in {abs(r - s) where r is Element of REAL, s is Element of REAL : r in A & s in B}; then consider r,s being Real such that A31: x = abs(r - s) and A32: r in A & s in B; [r,s] in [:A,B:] by A32,ZFMISC_1:106; then reconsider y = [r,s] as Element of AB by A1,BORSUK_1:def 5; consider r1,s1 being Real such that A33: y = [r1,s1] and A34: f.y = abs(r1-s1) by A5; r1 = r & s1 = s by A33,ZFMISC_1:33; hence x in f.:the carrier of AB by A31,A34,FUNCT_2:43; end; consider r,s being Real such that A35: x = [r,s] and A36: f.x = abs(r-s) by A5; r1 = r & s1 = s by A25,A35,ZFMISC_1:33; hence dist(A,B) = abs(r1 - s1) by A22,A26,A36,Def4; end; theorem Th19: for A, B being non empty compact Subset of REAL holds dist(A,B) >= 0 proof let A, B be non empty compact Subset of REAL; set X = {abs(r - s) where r is Element of REAL, s is Element of REAL : r in A & s in B}; consider r0 being set such that A1: r0 in A by XBOOLE_0:def 1; consider s0 being set such that A2: s0 in B by XBOOLE_0:def 1; r0 is Real & s0 is Real by A1,A2; then reconsider r0,s0 as real number; A3: abs(r0 - s0) in X by A1,A2; X c= REAL proof let e be set; assume e in X; then ex r,s being Real st e = abs(r - s) & r in A & s in B; hence thesis; end; then reconsider X as non empty Subset of REAL by A3; A4: dist(A,B) = lower_bound X by Def4; for t being real number st t in X holds t >= 0 proof let t be real number; assume t in X; then ex r,s being Real st t = abs(r - s) & r in A & s in B; hence t >= 0 by ABSVALUE:5; end; hence dist(A,B) >= 0 by A4,PSCOMP_1:8; end; theorem Th20: for A,B being non empty compact Subset of REAL st A misses B holds dist(A,B) > 0 proof let A,B being non empty compact Subset of REAL such that A1: A misses B; consider r0,s0 such that A2: r0 in A and A3: s0 in B and A4: dist(A,B) = abs(r0 - s0) by Th18; reconsider r0,s0 as Real by XREAL_0:def 1; assume dist(A,B) <= 0; then abs(r0 - s0) = 0 by A4,Th19; then r0 = s0 by GOBOARD7:2; hence contradiction by A1,A2,A3,XBOOLE_0:3; end; theorem for e,f being real number, A,B being compact Subset of REAL st A misses B & A c= [.e,f.] & B c= [.e,f.] for S being Function of NAT, bool REAL st for i being Nat holds S.i is connected & S.i meets A & S.i meets B ex r being real number st r in [.e,f.] & not r in A \/ B & for i being Nat ex k being Nat st i <= k & r in S.k proof let e,f be real number, A,B be compact Subset of REAL such that A1: A misses B and A2: A c= [.e,f.] and A3: B c= [.e,f.]; let S be Function of NAT, bool REAL such that A4: for i being Nat holds S.i is connected & S.i meets A & S.i meets B; defpred P[set,Element of bool REAL] means $2 is closed-interval & $2 meets A & $2 meets B & $2 c= S.$1; A5: for i being Nat ex u being Element of bool REAL st P[i,u] proof let i be Nat; S.i meets A by A4; then consider x being set such that A6: x in S.i and A7: x in A by XBOOLE_0:3; reconsider x as Real by A7; S.i meets B by A4; then consider y being set such that A8: y in S.i and A9: y in B by XBOOLE_0:3; reconsider y as Real by A9; A10: S.i is connected by A4; per cases; suppose A11: x <= y; take [.x,y.]; thus [.x,y.] is closed-interval by A11,INTEGRA1:def 1; x in [.x,y.] by A11,RCOMP_1:15; hence [.x,y.] meets A by A7,XBOOLE_0:3; y in [.x,y.] by A11,RCOMP_1:15; hence [.x,y.] meets B by A9,XBOOLE_0:3; thus [.x,y.] c= S.i by A6,A8,A10,Def3; suppose A12: y <= x; take [.y,x.]; thus [.y,x.] is closed-interval by A12,INTEGRA1:def 1; x in [.y,x.] by A12,RCOMP_1:15; hence [.y,x.] meets A by A7,XBOOLE_0:3; y in [.y,x.] by A12,RCOMP_1:15; hence [.y,x.] meets B by A9,XBOOLE_0:3; thus [.y,x.] c= S.i by A6,A8,A10,Def3; end; consider T be Function of NAT, bool REAL such that A13: for i being Nat holds P[i,T.i] from FuncExD(A5); deffunc F(Nat)=T.$1 /\ A; consider SA being Function of NAT, bool REAL such that A14: for i being Nat holds SA.i = F(i) from LambdaD; deffunc G(Nat)=T.$1 /\ B; consider SB being Function of NAT, bool REAL such that A15: for i being Nat holds SB.i = G(i) from LambdaD; defpred P[Nat,Real,Real] means $2 in SA.$1 & $3 in SB.$1 & dist(SA.$1,SB.$1) = abs($2 - $3); A16: for i being Nat ex ai,bi being Real st P[i,ai,bi] proof let i be Nat; reconsider Si = T.i as closed-interval Subset of REAL by A13; A17: T.i meets A & T.i meets B by A13; SA.i = Si /\ A & SB.i = Si /\ B by A14,A15; then reconsider SAi = SA.i, SBi = SB.i as non empty compact Subset of REAL by A17,Th14,XBOOLE_0:def 7; consider ai,bi being real number such that A18: ai in SAi & bi in SBi & dist(SAi,SBi) = abs(ai - bi) by Th18; reconsider ai,bi as Real by XREAL_0:def 1; take ai,bi; thus P[i,ai,bi] by A18; end; consider sa,sb being Real_Sequence such that A19: for i being Nat holds P[i,sa.i,sb.i] from DoubleChoice(A16); rng sa c= [.e,f.] proof let u be set; assume u in rng sa; then consider x being set such that A20: x in dom sa and A21: u = sa.x by FUNCT_1:def 5; reconsider n = x as Nat by A20; sa.n in SA.n by A19; then u in T.n /\ A by A14,A21; then u in A by XBOOLE_0:def 3; hence u in [.e,f.] by A2; end; then consider ga being Real_Sequence such that A22: ga is_subsequence_of sa and A23: ga is convergent and A24: lim ga in [.e,f.] by RCOMP_1:def 3; consider Nseq being increasing Seq_of_Nat such that A25: ga = sa*Nseq by A22,SEQM_3:def 10; set gb = sb*Nseq; rng gb c= [.e,f.] proof let u be set; assume u in rng gb; then consider x being set such that A26: x in dom gb and A27: u = gb.x by FUNCT_1:def 5; reconsider n = x as Nat by A26; gb.n = sb.(Nseq.n) by SEQM_3:31; then gb.n in SB.(Nseq.n) by A19; then u in T.(Nseq.n) /\ B by A15,A27; then u in B by XBOOLE_0:def 3; hence u in [.e,f.] by A3; end; then consider fb being Real_Sequence such that A28: fb is_subsequence_of gb and A29: fb is convergent and A30: lim fb in [.e,f.] by RCOMP_1:def 3; consider Nseq1 being increasing Seq_of_Nat such that A31: fb = gb*Nseq1 by A28,SEQM_3:def 10; set fa = ga*Nseq1, r = (lim fa + lim fb)/2; fa is_subsequence_of ga by SEQM_3:def 10; then A32: lim fa = lim ga by A23,SEQ_4:30; set d0 = dist(A,B), ff = (1/2)(#)(fa+fb); fa is_subsequence_of ga by SEQM_3:def 10; then A33: fa is convergent by A23,SEQ_4:29; then A34: fa+fb is convergent by A29,SEQ_2:19; then A35: ff is convergent by SEQ_2:21; A36: r = (1/2)*(lim fa + lim fb) by XCMPLX_1:100 .= (1/2)*lim(fa+fb) by A29,A33,SEQ_2:20 .= lim ff by A34,SEQ_2:22; T.0 meets A & T.0 meets B by A13; then A is non empty & B is non empty by XBOOLE_1:65; then d0 > 0 by A1,Th20; then d0/2 > 0 by REAL_2:127; then consider k0 being Nat such that A37: for i being Nat st k0 <= i holds abs(ff.i - r) < d0/2 by A35,A36,SEQ_2:def 7; A38: now assume A39: r in A \/ B; ff.k0 = (1/2)*((fa+fb).k0) by SEQ_1:13 .= ((fa+fb).k0)/2 by XCMPLX_1:100 .= (fa.k0+fb.k0)/2 by SEQ_1:11; then A40: abs((fa.k0+fb.k0)/2 - r) < d0/2 by A37; set i = Nseq.(Nseq1.k0), di = dist(SA.i,SB.i); T.i meets A & T.i meets B by A13; then T.i /\ A <> {} & T.i /\ B <> {} by XBOOLE_0:def 7; then A41: SA.i is non empty & SB.i is non empty by A14,A15; A42: SA.i = T.i /\ A & SB.i = T.i /\ B by A14,A15; then SA.i c= A & SB.i c= B by XBOOLE_1:17; then A43: d0 <= di by A41,Th17; then d0/2 <= di/2 by REAL_1:73; then di/2 + d0/2 <= di/2 + di/2 by AXIOMS:24; then A44: di/2 + d0/2 <= di by XCMPLX_1:66; A45: fa.k0 = ga.(Nseq1.k0) by SEQM_3:31 .= sa.i by A25,SEQM_3:31; A46: fb.k0 = gb.(Nseq1.k0) by A31,SEQM_3:31 .= sb.i by SEQM_3:31; T.i is closed-interval by A13; then consider a,b being Real such that a <= b and A47: T.i = [.a,b.] by INTEGRA1:def 1; 2*(d0/2) = d0 by XCMPLX_1:88; then A48: 2*abs((sa.i+sb.i)/2 - r) < d0 by A40,A45,A46,REAL_1:70; A49: 2*abs((sa.i+sb.i)/2 - r) = abs(2)*abs((sa.i+sb.i)/2 - r) by ABSVALUE:def 1 .= abs(2*((sa.i+sb.i)/2 - r)) by ABSVALUE:10 .= abs(2*((sa.i+sb.i)/2) - 2*r) by XCMPLX_1:40 .= abs(sa.i+sb.i-2*r) by XCMPLX_1:88; A50: sa.i in SA.i & sb.i in SB.i by A19; A51: SA.i c= T.i & SB.i c= T.i by A42,XBOOLE_1:17; A52: di <= abs(sb.i-sa.i) by A50,Th16; A53: now per cases; suppose sa.i <= sb.i; then sb.i - sa.i >= 0 by SQUARE_1:12; then di <= sb.i-sa.i by A52,ABSVALUE:def 1; then d0 <= sb.i-sa.i by A43,AXIOMS:22; then abs(sa.i+sb.i-2*r) <= sb.i-sa.i by A48,A49,AXIOMS:22; then A54: r in [.sa.i,sb.i.] by RCOMP_1:9; [.sa.i,sb.i.] c= T.i by A47,A50,A51,RCOMP_1:16; hence r in T.i by A54; suppose sb.i <= sa.i; then A55: sa.i - sb.i >= 0 by SQUARE_1:12; abs(sb.i-sa.i) = abs(sa.i-sb.i) by UNIFORM1:13; then di <= sa.i-sb.i by A52,A55,ABSVALUE:def 1; then d0 <= sa.i-sb.i by A43,AXIOMS:22; then abs(sb.i+sa.i-2*r) <= sa.i-sb.i by A48,A49,AXIOMS:22; then A56: r in [.sb.i,sa.i.] by RCOMP_1:9; [.sb.i,sa.i.] c= T.i by A47,A50,A51,RCOMP_1:16; hence r in T.i by A56; end; per cases by A39,XBOOLE_0:def 2; suppose A57: r in B; fa.k0 - (fa.k0+fb.k0)/2 = (fa.k0 + fa.k0)/2 - (fa.k0+fb.k0)/2 by XCMPLX_1: 65 .= (fa.k0 + fa.k0 - (fa.k0+fb.k0))/2 by XCMPLX_1:121 .= (fa.k0 + fa.k0 - fa.k0 - fb.k0)/2 by XCMPLX_1:36 .= (fa.k0 - fb.k0)/2 by XCMPLX_1:26; then fa.k0 - r = (fa.k0-fb.k0)/2 + (fa.k0+fb.k0)/2 - r by XCMPLX_1:27 .= (fa.k0-fb.k0)/2 + ((fa.k0+fb.k0)/2 - r) by XCMPLX_1:29; then A58: abs(fa.k0 - r) <= abs((fa.k0-fb.k0)/2) + abs((fa.k0+fb.k0)/2 - r) by ABSVALUE:13; A59: abs((fa.k0-fb.k0)/2) = abs((fa.k0-fb.k0))/abs(2) by ABSVALUE:16 .= abs((fa.k0-fb.k0))/2 by ABSVALUE:def 1; abs((fa.k0-fb.k0)/2) + abs((fa.k0+fb.k0)/2 - r) < abs((fa.k0-fb.k0)/2) + d0/2 by A40,REAL_1:53; then A60: abs(fa.k0 - r) < abs((fa.k0-fb.k0))/2 + d0/2 by A58,A59,AXIOMS:22 ; A61: fa.k0 in SA.i by A19,A45; SB.i = T.i /\ B by A15; then A62: r in SB.i by A53,A57,XBOOLE_0:def 3; abs(fa.k0 - r) < di/2 + d0/2 by A19,A45,A46,A60; then abs(fa.k0 - r) < di by A44,AXIOMS:22; hence contradiction by A61,A62,Th16; suppose A63: r in A; fb.k0 - (fb.k0+fa.k0)/2 = (fb.k0 + fb.k0)/2 - (fb.k0+fa.k0)/2 by XCMPLX_1: 65 .= (fb.k0 + fb.k0 - (fb.k0+fa.k0))/2 by XCMPLX_1:121 .= (fb.k0 + fb.k0 - fb.k0 - fa.k0)/2 by XCMPLX_1:36 .= (fb.k0 - fa.k0)/2 by XCMPLX_1:26; then fb.k0 - r = (fb.k0-fa.k0)/2 + (fb.k0+fa.k0)/2 - r by XCMPLX_1:27 .= (fb.k0-fa.k0)/2 + ((fb.k0+fa.k0)/2 - r) by XCMPLX_1:29; then A64: abs(fb.k0 - r) <= abs((fb.k0-fa.k0)/2) + abs((fb.k0+fa.k0)/2 - r) by ABSVALUE:13; A65: abs((fb.k0-fa.k0)/2) = abs((fb.k0-fa.k0))/abs(2) by ABSVALUE:16 .= abs((fb.k0-fa.k0))/2 by ABSVALUE:def 1; abs((fb.k0-fa.k0)/2) + abs((fb.k0+fa.k0)/2 - r) < abs((fb.k0-fa.k0)/2) + d0/2 by A40,REAL_1:53; then A66: abs(fb.k0 - r) < abs((fb.k0-fa.k0))/2 + d0/2 by A64,A65,AXIOMS:22 ; A67: fb.k0 in SB.i by A19,A46; SA.i = T.i /\ A by A14; then A68: r in SA.i by A53,A63,XBOOLE_0:def 3; abs(fb.k0-fa.k0) = abs(fa.k0-fb.k0) by UNIFORM1:13 .= di by A19,A45,A46; then abs(fb.k0 - r) < di by A44,A66,AXIOMS:22; hence contradiction by A67,A68,Th16; end; take r; thus r in [.e,f.] by A24,A30,A32,Th9; thus not r in A \/ B by A38; let i being Nat; A69: i <= Nseq.i by SEQM_3:33; i <= Nseq1.i by SEQM_3:33; then Nseq.i <= Nseq.(Nseq1.i) by Th10; then A70: i <= Nseq.(Nseq1.i) by A69,AXIOMS:22; set k = max(k0,i); A71: k0 <= k by SQUARE_1:46; take j = Nseq.(Nseq1.k); i <= k by SQUARE_1:46; then Nseq1.i <= Nseq1.k by Th10; then Nseq.(Nseq1.i) <= j by Th10; hence i <= j by A70,AXIOMS:22; ff.k = (1/2)*((fa+fb).k) by SEQ_1:13 .= ((fa+fb).k)/2 by XCMPLX_1:100 .= (fa.k+fb.k)/2 by SEQ_1:11; then A72: abs((fa.k+fb.k)/2 - r) < d0/2 by A37,A71; set di = dist(SA.j,SB.j); T.j meets A & T.j meets B by A13; then T.j /\ A <> {} & T.j /\ B <> {} by XBOOLE_0:def 7; then A73: SA.j is non empty & SB.j is non empty by A14,A15; A74: SA.j = T.j /\ A & SB.j = T.j /\ B by A14,A15; then SA.j c= A & SB.j c= B by XBOOLE_1:17; then A75: d0 <= di by A73,Th17; A76: fa.k = ga.(Nseq1.k) by SEQM_3:31 .= sa.j by A25,SEQM_3:31; A77: fb.k = gb.(Nseq1.k) by A31,SEQM_3:31 .= sb.j by SEQM_3:31; T.j is closed-interval by A13; then consider a,b be Real such that a <= b and A78: T.j = [.a,b.] by INTEGRA1:def 1; 2*(d0/2) = d0 by XCMPLX_1:88; then A79: 2*abs((sa.j+sb.j)/2 - r) < d0 by A72,A76,A77,REAL_1:70; A80: 2*abs((sa.j+sb.j)/2 - r) = abs(2)*abs((sa.j+sb.j)/2 - r) by ABSVALUE:def 1 .= abs(2*((sa.j+sb.j)/2 - r)) by ABSVALUE:10 .= abs(2*((sa.j+sb.j)/2) - 2*r) by XCMPLX_1:40 .= abs(sa.j+sb.j-2*r) by XCMPLX_1:88; A81: sa.j in SA.j & sb.j in SB.j by A19; A82: SA.j c= T.j & SB.j c= T.j by A74,XBOOLE_1:17; A83: di <= abs(sb.j-sa.j) by A81,Th16; A84: now per cases; suppose sa.j <= sb.j; then sb.j - sa.j >= 0 by SQUARE_1:12; then di <= sb.j-sa.j by A83,ABSVALUE:def 1; then d0 <= sb.j-sa.j by A75,AXIOMS:22; then abs(sa.j+sb.j-2*r) <= sb.j-sa.j by A79,A80,AXIOMS:22; then A85: r in [.sa.j,sb.j.] by RCOMP_1:9; [.sa.j,sb.j.] c= T.j by A78,A81,A82,RCOMP_1:16; hence r in T.j by A85; suppose sb.j <= sa.j; then A86: sa.j - sb.j >= 0 by SQUARE_1:12; abs(sb.j-sa.j) = abs(sa.j-sb.j) by UNIFORM1:13; then di <= sa.j-sb.j by A83,A86,ABSVALUE:def 1; then d0 <= sa.j-sb.j by A75,AXIOMS:22; then abs(sb.j+sa.j-2*r) <= sa.j-sb.j by A79,A80,AXIOMS:22; then A87: r in [.sb.j,sa.j.] by RCOMP_1:9; [.sb.j,sa.j.] c= T.j by A78,A81,A82,RCOMP_1:16; hence r in T.j by A87; end; T.j c= S.j by A13; hence r in S.j by A84; end;

Back to top