Copyright (c) 1991 Association of Mizar Users
environ vocabulary ARYTM, PRE_TOPC, SETFAM_1, TARSKI, SUBSET_1, COMPTS_1, BOOLE, RELAT_1, CONNSP_2, TOPS_1, ORDINAL2, FUNCT_1, METRIC_1, RCOMP_1, ABSVALUE, ARYTM_1, PCOMPS_1, EUCLID, FINSET_1, BORSUK_1, ARYTM_3, TOPMETR, PARTFUN1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1, REAL_1, DOMAIN_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSET_1, BINOP_1, STRUCT_0, METRIC_1, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, PCOMPS_1, CONNSP_2, RCOMP_1, ABSVALUE, BORSUK_1, EUCLID; constructors REAL_1, DOMAIN_1, TOPS_1, TOPS_2, COMPTS_1, RCOMP_1, ABSVALUE, BORSUK_1, EUCLID, MEMBERED, XBOOLE_0; clusters SUBSET_1, FUNCT_1, PRE_TOPC, PCOMPS_1, STRUCT_0, METRIC_3, METRIC_1, RELSET_1, EUCLID, TOPS_1, XREAL_0, MEMBERED, ZFMISC_1, XBOOLE_0; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; definitions STRUCT_0, PRE_TOPC, TARSKI, TOPS_2, XREAL_0; theorems ABSVALUE, AXIOMS, BINOP_1, BORSUK_1, COMPTS_1, CONNSP_2, EUCLID, FINSET_1, FUNCT_1, FUNCT_2, METRIC_1, PCOMPS_1, PRE_TOPC, RCOMP_1, REAL_1, REAL_2, TARSKI, TOPS_1, TOPS_2, ZFMISC_1, TBSP_1, RELAT_1, RELSET_1, XREAL_0, SETFAM_1, XBOOLE_0, XBOOLE_1, PARTFUN1, CARD_1, XCMPLX_1; schemes FUNCT_2; begin reserve r for Real, n for Nat; reserve a, b for real number; reserve T for non empty TopSpace; :: Topological spaces theorem Th1: for T being TopStruct, F being Subset-Family of T holds F is_a_cover_of T iff the carrier of T c= union F proof let T be TopStruct, F be Subset-Family of T; thus F is_a_cover_of T implies the carrier of T c= union F proof assume F is_a_cover_of T; then [#]T = union F by PRE_TOPC:def 8; hence the carrier of T c= union F by PRE_TOPC:12; end; assume the carrier of T c= union F; then the carrier of T = union F by XBOOLE_0:def 10; then [#] T = union F by PRE_TOPC:12; hence F is_a_cover_of T by PRE_TOPC:def 8; end; reserve A for non empty SubSpace of T; theorem Th2: for p being Point of A holds p is Point of T proof [#] A c= [#] T by PRE_TOPC:def 9; then the carrier of A c= [#] T by PRE_TOPC:12; then the carrier of A c= the carrier of T by PRE_TOPC:12; hence thesis by TARSKI:def 3; end; theorem T is_T2 implies A is_T2 proof assume A1: T is_T2; for p,q being Point of A st not p = q ex W,V being Subset of A st W is open & V is open & p in W & q in V & W misses V proof let p,q be Point of A such that A2: not p = q; reconsider p' = p, q' = q as Point of T by Th2; consider W,V being Subset of T such that A3: W is open & V is open & p' in W & q' in V & W misses V by A1,A2,COMPTS_1:def 4; A4: W /\ V = {} by A3,XBOOLE_0:def 7; W /\ [#] A c= [#] A & V /\ [#] A c= [#] A by XBOOLE_1:17; then reconsider W' = W /\ [#] A, V' = V /\ [#] A as Subset of A by PRE_TOPC:16; take W', V'; W in the topology of T & V in the topology of T by A3,PRE_TOPC:def 5; then W' in the topology of A & V' in the topology of A by PRE_TOPC:def 9; hence W' is open & V' is open by PRE_TOPC:def 5; the carrier of A = [#] A by PRE_TOPC:12; hence p in W' & q in V' by A3,XBOOLE_0:def 3; W' /\ V' = W /\ (V /\ [#] A) /\ [#] A by XBOOLE_1:16 .= {} /\ [#] A by A4,XBOOLE_1:16 .= {}; hence thesis by XBOOLE_0:def 7; end; hence A is_T2 by COMPTS_1:def 4; end; theorem Th4: for A,B being SubSpace of T st the carrier of A c= the carrier of B holds A is SubSpace of B proof let A,B be SubSpace of T; assume the carrier of A c= the carrier of B; then the carrier of A c= [#] B by PRE_TOPC:12; then A1: [#] A c= [#] B by PRE_TOPC:12; for P being Subset of A holds P in the topology of A iff ex Q being Subset of B st Q in the topology of B & P = Q /\ [#] A proof let P be Subset of A; thus P in the topology of A implies ex Q being Subset of B st Q in the topology of B & P = Q /\ [#] A proof assume P in the topology of A; then consider Q' being Subset of T such that A2: Q' in the topology of T & P = Q' /\ [#] A by PRE_TOPC:def 9; Q' /\ [#] B c= [#] B by XBOOLE_1:17; then reconsider Q = Q' /\ [#] B as Subset of B by PRE_TOPC:12; A3: Q in the topology of B by A2,PRE_TOPC:def 9; P = Q' /\ ([#] B /\ [#] A) by A1,A2,XBOOLE_1:28 .= Q /\ [#] A by XBOOLE_1:16; hence ex Q being Subset of B st Q in the topology of B & P = Q /\ [#] A by A3; end; given Q being Subset of B such that A4: Q in the topology of B & P = Q /\ [#] A; consider P' being Subset of T such that A5: P' in the topology of T & Q = P' /\ [#] B by A4,PRE_TOPC:def 9; P = P' /\ ([#] B /\ [#] A) by A4,A5,XBOOLE_1:16 .= P' /\ [#] A by A1, XBOOLE_1:28; hence P in the topology of A by A5,PRE_TOPC:def 9; end; hence A is SubSpace of B by A1,PRE_TOPC:def 9; end; reserve P,Q for Subset of T, p for Point of T; theorem T|P is SubSpace of T|(P \/ Q) & T|Q is SubSpace of T|(P \/ Q) proof thus T|P is SubSpace of T|(P \/ Q) proof [#](T|P) = P by PRE_TOPC:def 10; then A1: the carrier of T|P = P by PRE_TOPC:12; [#](T|(P \/ Q)) = P \/ Q by PRE_TOPC:def 10; then the carrier of T|(P \/ Q) = P \/ Q & P c= P \/ Q by PRE_TOPC:12,XBOOLE_1:7; hence T|P is SubSpace of T|(P \/ Q) by A1,Th4; end; [#](T|Q) = Q by PRE_TOPC:def 10; then A2: the carrier of T|Q = Q by PRE_TOPC:12; [#](T|(P \/ Q)) = P \/ Q by PRE_TOPC:def 10; then the carrier of T|(P \/ Q) = P \/ Q & Q c= P \/ Q by PRE_TOPC:12,XBOOLE_1:7; hence T|Q is SubSpace of T|(P \/ Q) by A2,Th4; end; theorem for P being non empty Subset of T st p in P for Q being a_neighborhood of p holds for p' being Point of T|P, Q' being Subset of T|P st Q' = Q /\ P & p'= p holds Q' is a_neighborhood of p' proof let P be non empty Subset of T; assume A1: p in P; let Q be a_neighborhood of p; p in Int Q by CONNSP_2:def 1; then consider S being Subset of T such that A2: S is open & S c= Q & p in S by TOPS_1:54; let p' be Point of T|P, Q' be Subset of T|P such that A3: Q' = Q /\ P & p'= p; reconsider R = S /\ P as Subset of T|P by TOPS_2:38; S /\ [#](T|P) = S /\ P by PRE_TOPC:def 10; then A4: R is open by A2,TOPS_2:32; R c= Q' & p' in R by A1,A2,A3,XBOOLE_0:def 3,XBOOLE_1:26; then p' in Int Q' by A4,TOPS_1:54; hence Q' is a_neighborhood of p' by CONNSP_2:def 1; end; theorem for A,B,C being TopSpace for f being map of A,C holds f is continuous & C is SubSpace of B implies for h being map of A,B st h = f holds h is continuous proof let A,B,C be TopSpace, f be map of A,C; assume that A1: f is continuous and A2: C is SubSpace of B; let h be map of A,B such that A3: h = f; for P being Subset of B holds P is closed implies h"P is closed proof let P be Subset of B such that A4: P is closed; rng h c= the carrier of C by A3,RELSET_1:12; then A5: rng h c= [#] C by PRE_TOPC:12; A6: h"P = h"(rng h /\ P) by RELAT_1:168 .= h"(rng h /\ [#] C /\ P) by A5,XBOOLE_1:28 .= h"(rng h /\ ([#] C /\ P)) by XBOOLE_1:16 .= h"(P /\ [#] C) by RELAT_1:168; reconsider C as SubSpace of B by A2; P /\ [#] C c= [#] C & [#] C = the carrier of C by PRE_TOPC:12,XBOOLE_1:17 ; then reconsider Q = P /\ [#] C as Subset of C; Q is closed by A4,PRE_TOPC:43; hence h"P is closed by A1,A3,A6,PRE_TOPC:def 12; end; hence h is continuous by PRE_TOPC:def 12; end; theorem for A being TopSpace, B being non empty TopSpace for f being map of A,B for C being SubSpace of B holds f is continuous implies for h being map of A,C st h = f holds h is continuous proof let A be TopSpace, B be non empty TopSpace, f be map of A,B, C be SubSpace of B; assume that A1: f is continuous; let h be map of A,C such that A2: h = f; rng f c= the carrier of C by A2,RELSET_1:12; then A3: rng f c= [#] C by PRE_TOPC:12; for P being Subset of C holds P is closed implies h"P is closed proof let P be Subset of C; assume P is closed; then consider Q being Subset of B such that A4: Q is closed & Q /\ ([#] C) = P by PRE_TOPC:43; A5: f"Q c= dom f & the carrier of A = [#] A & dom f = the carrier of A by FUNCT_2:def 1,PRE_TOPC:12,RELAT_1:167; h"P = f"Q /\ f"([#] C) by A2,A4,FUNCT_1:137 .= f"Q /\ f"(rng f /\ [#] C) by RELAT_1:168 .= f"Q /\ f"(rng f) by A3,XBOOLE_1:28 .= f"Q /\ dom f by RELAT_1:169 .= f"Q by A5,XBOOLE_1:28; hence h"P is closed by A1,A4,PRE_TOPC:def 12; end; hence h is continuous by PRE_TOPC:def 12; end; theorem for A,B being TopSpace for f being map of A,B for C being Subset of B holds f is continuous implies for h being map of A,B|C st h = f holds h is continuous proof let A,B be TopSpace, f be map of A,B, C be Subset of B; assume that A1: f is continuous; let h be map of A,B|C such that A2: h = f; A3: the carrier of B|C = [#](B|C) by PRE_TOPC:12 .= C by PRE_TOPC:def 10; A4: rng f c= the carrier of B|C by A2,RELSET_1:12; for P being Subset of B|C holds P is closed implies h"P is closed proof let P be Subset of B|C; assume P is closed; then consider Q being Subset of B such that A5: Q is closed & Q /\ ([#](B|C)) = P by PRE_TOPC:43; A6: f"Q c= dom f by RELAT_1:167; h"P = f"(Q /\ C) by A2,A5,PRE_TOPC:def 10 .= f"Q /\ f"C by FUNCT_1:137 .= f"Q /\ f"(rng f /\ C) by RELAT_1:168 .= f"Q /\ f"(rng f) by A3,A4,XBOOLE_1:28 .= f"Q /\ dom f by RELAT_1:169 .= f"Q by A6,XBOOLE_1:28; hence h"P is closed by A1,A5,PRE_TOPC:def 12; end; hence h is continuous by PRE_TOPC:def 12; end; theorem for X being TopStruct, Y being non empty TopStruct, K0 being Subset of X, f being map of X,Y, g being map of X|K0,Y st f is continuous & g = f|K0 holds g is continuous proof let X be TopStruct,Y be non empty TopStruct, K0 be Subset of X, f be map of X,Y,g be map of X|K0,Y; assume A1:f is continuous & g=f|K0; for G being Subset of Y st G is open holds g"G is open proof let G be Subset of Y; assume G is open; then A2:f"G is open by A1,TOPS_2:55; [#](X|K0)=K0 by PRE_TOPC:def 10; then g"G= [#](X|K0) /\ f"G by A1,FUNCT_1:139; hence thesis by A2,TOPS_2:32; end; hence thesis by TOPS_2:55; end; :: Some definitions & theorems about metrical spaces reserve M for non empty MetrSpace, p for Point of M; Lm1: for r being real number st r > 0 holds p in Ball(p,r) proof let r be real number; reconsider r' = r as Element of REAL by XREAL_0:def 1; assume r > 0; then p in Ball(p,r') by TBSP_1:16; hence thesis; end; Lm2: for M be MetrSpace holds MetrStruct (#the carrier of M, the distance of M#) is MetrSpace proof let M be MetrSpace; now let a,b,c be Element of the carrier of MetrStruct (#the carrier of M, the distance of M#); reconsider a'=a, b'=b, c'=c as Element of M; A1: dist(a,b) = (the distance of M).(a,b) by METRIC_1:def 1 .= dist(a',b') by METRIC_1:def 1; hence dist(a,b) = 0 iff a=b by METRIC_1:1,2; dist(b,a) = (the distance of M).(b,a) by METRIC_1:def 1 .= dist(b',a') by METRIC_1:def 1; hence dist(a,b) = dist(b,a) by A1; A2: dist(b,c) = (the distance of M).(b,c) by METRIC_1:def 1 .= dist(b',c') by METRIC_1:def 1; dist(a,c) = (the distance of M).(a,c) by METRIC_1:def 1 .= dist(a',c') by METRIC_1:def 1; hence dist(a,c)<=dist(a,b)+dist(b,c) by A1,A2,METRIC_1:4; end; hence thesis by METRIC_1:6; end; definition let M be MetrSpace; mode SubSpace of M -> MetrSpace means :Def1: the carrier of it c= the carrier of M & for x,y being Point of it holds (the distance of it).(x,y) = (the distance of M).(x,y); existence proof reconsider MM = MetrStruct (#the carrier of M, the distance of M#) as MetrSpace by Lm2; take MM; thus the carrier of MM c= the carrier of M; let x,y be Point of MM; thus (the distance of MM).(x,y) = (the distance of M).(x,y); end; end; definition let M be MetrSpace; cluster strict SubSpace of M; existence proof reconsider MM = MetrStruct (#the carrier of M, the distance of M#) as MetrSpace by Lm2; the carrier of MM c= the carrier of M & for x,y being Point of MM holds (the distance of MM).(x,y) = (the distance of M).(x,y); then MM is SubSpace of M by Def1; hence thesis; end; end; definition let M be non empty MetrSpace; cluster strict non empty SubSpace of M; existence proof reconsider MM = MetrStruct (#the carrier of M, the distance of M#) as MetrSpace by Lm2; the carrier of MM c= the carrier of M & for x,y being Point of MM holds (the distance of MM).(x,y) = (the distance of M).(x,y); then MM is SubSpace of M by Def1; hence thesis; end; end; reserve A for non empty SubSpace of M; canceled; theorem Th12: for p being Point of A holds p is Point of M proof let p be Point of A; p in the carrier of A & the carrier of A c= the carrier of M by Def1; hence p is Point of M; end; theorem Th13: for r being real number for M being MetrSpace, A being SubSpace of M for x being Point of M, x' being Point of A st x = x' holds Ball(x',r) = Ball(x,r) /\ the carrier of A proof let r be real number; let M be MetrSpace, A be SubSpace of M; let x be Point of M, x' be Point of A; assume A1: x = x'; now let a be set; assume A2: a in Ball(x',r); then A3: a in the carrier of A; reconsider y' = a as Point of A by A2; A4: A is non empty proof thus the carrier of A is non empty by A2; end; A5: M is non empty proof the carrier of A c= the carrier of M by Def1; hence the carrier of M is non empty by A3; end; then reconsider y = y' as Point of M by A4,Th12; dist(x',y') < r by A2,METRIC_1:12; then (the distance of A).(x',y') < r by METRIC_1:def 1; then (the distance of M).(x,y) < r by A1,Def1; then dist(x,y) < r by METRIC_1:def 1; then a in Ball(x,r) by A5,METRIC_1:12; hence a in Ball(x,r) /\ the carrier of A by A2,XBOOLE_0:def 3; end; then A6: Ball(x',r) c= Ball(x,r) /\ the carrier of A by TARSKI:def 3; now let a be set; assume A7: a in Ball(x,r) /\ the carrier of A; then A8: a in Ball(x,r) & a in the carrier of A by XBOOLE_0:def 3; A9: A is non empty proof thus the carrier of A is non empty by A7; end; A10: M is non empty proof thus the carrier of M is non empty by A8; end; reconsider y' = a as Point of A by A7,XBOOLE_0:def 3; reconsider y = y' as Point of M by A9,A10,Th12; dist(x,y) < r by A8,METRIC_1:12; then (the distance of M).(x,y) < r by METRIC_1:def 1; then (the distance of A).(x',y') < r by A1,Def1; then dist(x',y') < r by METRIC_1:def 1; hence a in Ball(x',r) by A9,METRIC_1:12; end; then Ball(x,r) /\ the carrier of A c= Ball(x',r) by TARSKI:def 3; hence Ball(x',r) = Ball(x,r) /\ the carrier of A by A6,XBOOLE_0:def 10; end; definition let M be non empty MetrSpace, A be non empty Subset of M; func M|A -> strict SubSpace of M means :Def2: the carrier of it = A; existence proof set d = (the distance of M) | [:A,A:]; reconsider B=A as non empty set; A1: dom d = dom (the distance of M) /\ [:A,A:] by FUNCT_1:68 .= [:the carrier of M,the carrier of M:] /\ [:A,A:] by FUNCT_2:def 1 .= [: (the carrier of M) /\ A, (the carrier of M) /\ A:] by ZFMISC_1:123 .= [: (the carrier of M) /\ A, A:] by XBOOLE_1:28 .= [: A, A :] by XBOOLE_1:28; then dom d = [: A,A :] & rng d c= rng the distance of M & rng the distance of M c= REAL by FUNCT_1:76,RELSET_1:12; then dom d = [: A,A :] & rng d c= REAL by XBOOLE_1:1; then reconsider d as Function of [:B,B:],REAL by FUNCT_2:def 1,RELSET_1:11; set MM = MetrStruct (# B, d #); A2: now let a,b be Element of MM; thus dist(a,b) = (the distance of MM).(a,b) by METRIC_1:def 1 .= (the distance of MM) . [a,b] by BINOP_1:def 1 .= (the distance of M) . [a,b] by A1,FUNCT_1:70 .= (the distance of M).(a,b) by BINOP_1:def 1; end; now let a,b,c be Element of MM; reconsider a'=a, b'=b, c'=c as Point of M by TARSKI:def 3; dist(a,b) = (the distance of M).(a,b) by A2 .= dist(a',b') by METRIC_1:def 1; hence dist(a,b) = 0 iff a=b by METRIC_1:1,2; thus dist(a,b) = (the distance of M).(a',b') by A2 .= dist(b',a') by METRIC_1:def 1 .= (the distance of M).(b',a') by METRIC_1:def 1 .= dist(b,a) by A2; A3: dist(a,b) = (the distance of M).(a,b) by A2 .= dist(a',b') by METRIC_1:def 1; A4: dist(a,c) = (the distance of M).(a,c) by A2 .= dist(a',c') by METRIC_1:def 1; dist(b,c) = (the distance of M).(b,c) by A2 .= dist(b',c') by METRIC_1:def 1; hence dist(a,c)<=dist(a,b)+dist(b,c) by A3,A4,METRIC_1:4; end; then reconsider MM as MetrSpace by METRIC_1:6; now let x, y be Point of MM; thus (the distance of MM).(x,y) = dist(x,y) by METRIC_1:def 1 .= (the distance of M).(x,y) by A2; end; then reconsider MM as strict SubSpace of M by Def1; take MM; thus the carrier of MM = A; end; uniqueness proof let S1,S2 be strict SubSpace of M; assume A5: the carrier of S1 = A & the carrier of S2 = A; now let a,b be Element of A; thus (the distance of S1).(a,b) = (the distance of M).(a,b) by A5,Def1 .= (the distance of S2).(a,b) by A5,Def1; end; hence S1 = S2 by A5,BINOP_1:2; end; end; definition let M be non empty MetrSpace, A be non empty Subset of M; cluster M|A -> non empty; coherence proof thus the carrier of (M|A) is non empty by Def2; end; end; definition let a,b be real number; assume A1: a <= b; func Closed-Interval-MSpace(a,b) -> strict non empty SubSpace of RealSpace means :Def3: for P being non empty Subset of RealSpace st P = [. a,b .] holds it = RealSpace | P; existence proof reconsider P = [. a,b .] as Subset of RealSpace by METRIC_1:def 14; reconsider P as non empty Subset of RealSpace by A1,RCOMP_1:15; take RealSpace | P; thus thesis; end; uniqueness proof let S1,S2 be strict non empty SubSpace of RealSpace; assume that A2: for P being non empty Subset of RealSpace st P = [. a,b .] holds S1 = RealSpace | P and A3: for P being non empty Subset of RealSpace st P = [. a,b .] holds S2 = RealSpace | P; reconsider P = [. a,b .] as Subset of RealSpace by METRIC_1:def 14; reconsider P as non empty Subset of RealSpace by A1,RCOMP_1:15; thus S1 = RealSpace | P by A2 .= S2 by A3; end; end; theorem Th14: a <= b implies the carrier of Closed-Interval-MSpace(a,b) = [. a,b .] proof assume A1: a <= b; then reconsider P = [. a,b .] as non empty Subset of RealSpace by METRIC_1:def 14,RCOMP_1:15; thus the carrier of Closed-Interval-MSpace(a,b) = the carrier of RealSpace | P by A1,Def3 .= [. a,b .] by Def2; end; reserve F,G for Subset-Family of M; definition let M be MetrStruct, F be Subset-Family of M; attr F is being_ball-family means :Def4: for P being set holds P in F implies ex p being Point of M, r st P = Ball(p,r); synonym F is_ball-family; pred F is_a_cover_of M means :Def5: the carrier of M c= union F; end; theorem Th15: for p,q being Point of RealSpace, x,y being real number holds x=p & y=q implies dist(p,q) = abs(x-y) proof let p,q be Point of RealSpace, x,y be real number; assume A1: x=p & y=q; A2: x is Real & y is Real by XREAL_0:def 1; thus dist(p,q) = real_dist.(x,y) by A1,METRIC_1:def 1,def 14 .= abs(x-y) by A2,METRIC_1:def 13; end; :: Metric spaces and topology theorem Th16: for M being MetrStruct holds the carrier of M = the carrier of TopSpaceMetr M & the topology of TopSpaceMetr M = Family_open_set M proof let M be MetrStruct; TopSpaceMetr M = TopStruct (#the carrier of M, Family_open_set(M)#) by PCOMPS_1:def 6; hence thesis; end; canceled 2; theorem Th19: TopSpaceMetr(A) is SubSpace of TopSpaceMetr(M) proof set T = TopSpaceMetr M, R = TopSpaceMetr A; [#] R = the carrier of R & [#] T = the carrier of T by PRE_TOPC:12; then A1: [#] R = the carrier of A & [#] T = the carrier of M by Th16; hence [#](R) c= [#](T) by Def1; let P be Subset of R; thus P in the topology of R implies ex Q being Subset of T st Q in the topology of T & P = Q /\ [#](R) proof assume P in the topology of R; then A2: P in Family_open_set A by Th16; set QQ = {Ball(x,r) where x is Point of M, r is Real : x in P & r > 0 & Ball(x,r) /\ the carrier of A c= P}; for X being set st X in QQ holds X c= the carrier of M proof let X be set; assume X in QQ; then ex x being Point of M, r being Real st X = Ball(x,r) & x in P & r > 0 & Ball(x,r) /\ the carrier of A c= P; hence X c= the carrier of M; end; then reconsider Q = union QQ as Subset of M by ZFMISC_1:94; for x being Point of M st x in Q ex r st r > 0 & Ball(x,r) c= Q proof let x be Point of M; assume x in Q; then consider Y being set such that A3: x in Y & Y in QQ by TARSKI:def 4; consider x' being Point of M, r being Real such that A4: Y = Ball(x',r) and x' in P & r > 0 & Ball(x',r) /\ the carrier of A c= P by A3; consider p being Real such that A5: p > 0 & Ball(x,p) c= Ball(x',r) by A3,A4,PCOMPS_1:30; take p; thus p > 0 by A5; Y c= Q by A3,ZFMISC_1:92; hence thesis by A4,A5,XBOOLE_1:1; end; then A6: Q in Family_open_set M by PCOMPS_1:def 5; reconsider Q' = Q as Subset of T by Th16; take Q'; thus Q' in the topology of T by A6,Th16; thus P = Q' /\ [#](R) proof A7: P c= Q' /\ [#](R) proof let a be set; assume A8: a in P; then a in the carrier of R; then A9: a in [#](R) by PRE_TOPC:12; reconsider x = a as Point of A by A8,Th16; reconsider P' = P as Subset of A by Th16; consider r such that A10: r > 0 & Ball(x,r) c= P' by A2,A8,PCOMPS_1:def 5; reconsider x' = x as Point of M by Th12; Ball(x,r) = Ball(x',r) /\ the carrier of A by Th13; then Ball(x',r) in QQ & x' in Ball(x',r) by A8,A10,Lm1; then a in Q' by TARSKI:def 4; hence thesis by A9,XBOOLE_0:def 3; end; Q' /\ [#](R) c= P proof let a be set; assume A11: a in Q' /\ [#](R); then a in Q' by XBOOLE_0:def 3; then consider Y being set such that A12: a in Y & Y in QQ by TARSKI:def 4; consider x being Point of M, r being Real such that A13: Y = Ball(x,r) and x in P and r > 0 and A14: Ball(x,r) /\ the carrier of A c= P by A12; a in the carrier of A by A1,A11,XBOOLE_0:def 3; then a in Ball(x,r) /\ the carrier of A by A12,A13,XBOOLE_0:def 3; hence a in P by A14; end; hence thesis by A7,XBOOLE_0:def 10; end; end; given Q being Subset of T such that A15: Q in the topology of T & P = Q /\ [#](R); reconsider Q' = Q as Subset of M by Th16; reconsider P' = P as Subset of A by Th16; for p being Point of A st p in P' ex r st r>0 & Ball(p,r) c= P' proof let p be Point of A; reconsider p' = p as Point of M by Th12; assume p in P'; then p' in Q' & Q' in Family_open_set M by A15,Th16,XBOOLE_0:def 3; then consider r such that A16: r>0 & Ball(p',r) c= Q' by PCOMPS_1:def 5; Ball(p,r) = Ball(p',r) /\ the carrier of A by Th13; then Ball(p,r) c= Q /\ the carrier of A by A16,XBOOLE_1:26; then Ball(p,r) c= Q /\ the carrier of R by Th16; then Ball(p,r) c= P' by A15,PRE_TOPC:12; hence thesis by A16; end; then P in Family_open_set A by PCOMPS_1:def 5; hence P in the topology of R by Th16; end; theorem for P being Subset of TOP-REAL n, Q being non empty Subset of Euclid n holds P = Q implies (TOP-REAL n)|P = TopSpaceMetr((Euclid n)|Q) proof let P be Subset of (TOP-REAL n), Q be non empty Subset of Euclid n; TOP-REAL n = TopSpaceMetr(Euclid n) by EUCLID:def 8; then reconsider M = TopSpaceMetr((Euclid n)|Q) as SubSpace of TOP-REAL n by Th19; assume A1: P = Q; the carrier of M = the carrier of (Euclid n)|Q & the carrier of (Euclid n)|Q = Q by Def2,Th16; then [#](M) = P & [#]((TOP-REAL n)|P) = P by A1,PRE_TOPC:12,def 10; hence thesis by PRE_TOPC:def 10; end; theorem Th21: for r being real number for M being triangle MetrStruct, p being Point of M for P being Subset of TopSpaceMetr(M) st P = Ball(p,r) holds P is open proof let r be real number; let M be triangle MetrStruct, p be Point of M; let P be Subset of TopSpaceMetr(M); assume P = Ball(p,r); then P in Family_open_set(M) & Family_open_set M = the topology of TopSpaceMetr M by Th16,PCOMPS_1:33; hence P is open by PRE_TOPC:def 5; end; theorem Th22: for P being Subset of TopSpaceMetr(M) holds P is open iff for p being Point of M st p in P ex r being real number st r>0 & Ball(p,r) c= P proof let P be Subset of TopSpaceMetr(M); reconsider P' = P as Subset of M by Th16; thus P is open implies for p being Point of M st p in P ex r being real number st r>0 & Ball(p,r) c= P proof assume A1: P is open; let p be Point of M such that A2: p in P; P in the topology of TopSpaceMetr M by A1,PRE_TOPC:def 5; then P' in Family_open_set M by Th16; then ex r being Real st r>0 & Ball(p,r) c= P by A2,PCOMPS_1:def 5; hence thesis; end; assume A3: for p being Point of M st p in P ex r being real number st r>0 & Ball(p,r) c= P; for p being Point of M st p in P ex r being Real st r>0 & Ball(p,r) c= P proof let p be Point of M; assume p in P; then consider r being real number such that A4: r>0 & Ball(p,r) c= P by A3; reconsider r as Element of REAL by XREAL_0:def 1; take r; thus thesis by A4; end; then P' in Family_open_set M by PCOMPS_1:def 5; hence P in the topology of TopSpaceMetr M by Th16; end; definition let M be MetrStruct; attr M is compact means :Def6: TopSpaceMetr(M) is compact; end; theorem M is compact iff for F st F is_ball-family & F is_a_cover_of M ex G st G c= F & G is_a_cover_of M & G is finite proof thus M is compact implies for F st F is_ball-family & F is_a_cover_of M ex G st G c= F & G is_a_cover_of M & G is finite proof assume M is compact; then A1: TopSpaceMetr(M) is compact by Def6; let F; assume that A2: F is_ball-family and A3: F is_a_cover_of M; set TM = TopSpaceMetr(M); F is Subset-Family of TM by Th16; then reconsider TF = F as Subset-Family of TM; the carrier of M c= union F by A3,Def5; then the carrier of TM c= union TF by Th16; then A4: TF is_a_cover_of TM by Th1; TF is open proof let P be Subset of TM; assume A5: P in TF; reconsider P' = P as Subset of M by Th16; ex p,r st P' = Ball(p,r) by A2,A5,Def4; hence P is open by Th21; end; then consider TG being Subset-Family of TM such that A6: TG c= TF & TG is_a_cover_of TM & TG is finite by A1,A4,COMPTS_1:def 3; TG is Subset-Family of M by Th16; then reconsider G = TG as Subset-Family of M; take G; the carrier of TM c= union TG by A6,Th1; then the carrier of M c= union G by Th16; hence G c= F & G is_a_cover_of M & G is finite by A6,Def5; end; thus (for F st F is_ball-family & F is_a_cover_of M ex G st G c= F & G is_a_cover_of M & G is finite) implies M is compact proof assume A7: for F st F is_ball-family & F is_a_cover_of M ex G st G c= F & G is_a_cover_of M & G is finite; set TM = TopSpaceMetr(M); now let F be Subset-Family of TM; assume that A8: F is_a_cover_of TM and A9: F is open; set Z = { Ball(p,r) where p is Point of M, r is Real: ex P being Subset of TM st P in F & Ball(p,r) c= P}; Z c= bool the carrier of M proof let a be set; assume a in Z; then ex p being Point of M, r being Real st a = Ball(p,r) & ex P being Subset of TM st P in F & Ball(p,r) c= P; hence a in bool the carrier of M; end; then Z is Subset-Family of M by SETFAM_1:def 7; then reconsider Z as Subset-Family of M; A10: Z is_ball-family proof let P be set; assume P in Z; then ex p being Point of M, r being Real st P = Ball(p,r) & ex P being Subset of TM st P in F & Ball(p,r) c= P; hence thesis; end; the carrier of M c= union Z proof let a be set; assume a in the carrier of M; then reconsider p = a as Point of M; the carrier of TM c= union F & the carrier of TM = the carrier of M by A8,Th1,Th16; then p in union F by TARSKI:def 3; then consider P being set such that A11: p in P and A12: P in F by TARSKI:def 4; reconsider P as Subset of TM by A12; P is open by A9,A12,TOPS_2:def 1; then consider r being real number such that A13: r>0 & Ball(p,r) c= P by A11,Th22; reconsider r' = r as Element of REAL by XREAL_0:def 1; A14: a in Ball(p,r) by A13,Lm1; Ball(p,r') in Z by A12,A13; hence a in union Z by A14,TARSKI:def 4; end; then Z is_a_cover_of M by Def5; then consider G being Subset-Family of M such that A15: G c= Z and A16: G is_a_cover_of M and A17: G is finite by A7,A10; reconsider F' = F as non empty Subset-Family of TM by A8,TOPS_2:5; defpred X[set,set] means $1 c= $2; A18: for a being set st a in G ex u being set st u in F' & X[a,u] proof let a be set; assume a in G; then a in Z by A15; then consider p being Point of M, r being Real such that A19: Ball(p,r) = a and A20: ex P being Subset of TM st P in F & Ball(p,r) c= P; consider P being Subset of TM such that A21: P in F & Ball(p,r) c= P by A20; take P; thus P in F' & a c= P by A19,A21; end; consider f being Function of G,F' such that A22: for a being set st a in G holds X[a,f.a] from FuncEx1(A18); rng f c= F by RELSET_1:12; then reconsider GG = rng f as Subset-Family of TM by TOPS_2:3; take GG; thus GG c= F by RELSET_1:12; the carrier of TM c= union GG proof let a be set such that A23: a in the carrier of TM; the carrier of TM = the carrier of M & the carrier of M c= union G by A16,Def5,Th16; then consider P being set such that A24: a in P & P in G by A23,TARSKI:def 4; dom f = G by FUNCT_2:def 1; then f.P in GG & P c= f.P by A22,A24,FUNCT_1:def 5; hence a in union GG by A24,TARSKI:def 4; end; hence GG is_a_cover_of TM by Th1; dom f = G by FUNCT_2:def 1; hence GG is finite by A17,FINSET_1:26; end; then TM is compact by COMPTS_1:def 3; hence thesis by Def6; end; end; :: REAL as topological space definition func R^1 -> strict TopSpace equals :Def7: TopSpaceMetr(RealSpace); correctness; end; definition cluster R^1 -> non empty; coherence by Def7; end; theorem Th24: the carrier of R^1 = REAL proof the carrier of R^1 = the carrier of TopStruct (# the carrier of RealSpace, Family_open_set(RealSpace) #) & the carrier of RealSpace = the carrier of MetrStruct(# REAL,real_dist #) by Def7,METRIC_1:def 14,PCOMPS_1:def 6; hence thesis; end; definition let C be set, f be PartFunc of C, the carrier of R^1, x be set; cluster f.x -> real; coherence proof per cases; suppose x in dom f; hence f.x in REAL by Th24,PARTFUN1:27; suppose not x in dom f; hence thesis by CARD_1:51,FUNCT_1:def 4; end; end; definition let a,b be real number; func Closed-Interval-TSpace(a,b) -> strict non empty SubSpace of R^1 equals :Def8: TopSpaceMetr(Closed-Interval-MSpace(a,b)); coherence by Def7,Th19; end; theorem Th25: a <= b implies the carrier of Closed-Interval-TSpace(a,b) = [. a,b .] proof assume A1: a <= b; thus the carrier of Closed-Interval-TSpace(a,b) = the carrier of TopSpaceMetr(Closed-Interval-MSpace(a,b)) by Def8 .= the carrier of Closed-Interval-MSpace(a,b) by Th16 .= [. a,b .] by A1,Th14; end; theorem Th26: a <= b implies for P being Subset of R^1 st P = [. a,b .] holds Closed-Interval-TSpace(a,b) = R^1|P proof assume A1: a <= b; let P be Subset of R^1; assume P = [. a,b .]; then the carrier of Closed-Interval-TSpace(a,b) = P by A1,Th25; then [#](Closed-Interval-TSpace(a,b)) = P & [#](R^1|P) = P by PRE_TOPC:12,def 10; hence Closed-Interval-TSpace(a,b) = R^1|P by PRE_TOPC:def 10; end; theorem Th27: Closed-Interval-TSpace(0,1) = I[01] proof set TR = TopSpaceMetr(RealSpace); reconsider P = [.0,1.] as Subset of R^1 by Th24; reconsider P' = P as Subset of TR by Th16,METRIC_1:def 14; thus Closed-Interval-TSpace(0,1) = TR|P' by Def7,Th26 .= I[01] by BORSUK_1: def 16; end; definition redefine func I[01] -> strict SubSpace of R^1; coherence by Th27; end; Lm3: for r be real number holds r >= 0 & a + r <= b implies a <= b proof let r be real number; assume A1: r >= 0 & a + r <= b; then a + r - r <= b - r by REAL_1:49; then a <= b - r & b - r <= b by A1,REAL_2:173,XCMPLX_1:26; hence thesis by AXIOMS:22; end; theorem for f being map of R^1,R^1 st ex a,b being Real st for x being Real holds f.x = a*x + b holds f is continuous proof let f be map of R^1,R^1; given a,b being Real such that A1: for x being Real holds f.x = a*x + b; for W being Point of R^1, G being a_neighborhood of f.W ex H being a_neighborhood of W st f.:H c= G proof let W be Point of R^1, G be a_neighborhood of f.W; A2: f.W in Int G by CONNSP_2:def 1; then consider Q being Subset of R^1 such that A3: Q is open & Q c= G & f.W in Q by TOPS_1:54; reconsider Y = f.W as Point of RealSpace by Th24,METRIC_1:def 14; consider r being real number such that A4: r>0 & Ball(Y,r) c= Q by A3,Def7,Th22; now per cases; suppose A5: a = 0; set H = [#](R^1); the carrier of R^1 = [#](R^1) by PRE_TOPC:12; then H is open & W in H; then W in Int H by TOPS_1:55; then reconsider H as a_neighborhood of W by CONNSP_2:def 1; for y being set holds y in {b} iff ex x being set st x in dom f & x in H & y = f.x proof let y be set; thus y in {b} implies ex x being set st x in dom f & x in H & y = f.x proof assume A6: y in {b}; take 0; dom f = the carrier of R^1 & the carrier of R^1 = [#](R^1) & the carrier of R^1 = REAL by Th24,FUNCT_2:def 1,PRE_TOPC:12; hence 0 in dom f & 0 in H; thus f.0 = 0 * 0 + b by A1,A5 .= y by A6,TARSKI:def 1; end; given x being set such that A7: x in dom f & x in H & y = f.x; reconsider x as Real by A7,Th24; y = 0 * x + b by A1,A5,A7 .= b; hence y in {b} by TARSKI:def 1; end; then A8: f.:H = {b} by FUNCT_1:def 12; A9: Int G c= G by TOPS_1:44; reconsider W' = W as Real by Th24; f.W = 0 * W' + b by A1,A5 .= b; then f.:H c= G by A2,A8,A9,ZFMISC_1:37; hence ex H being a_neighborhood of W st f.:H c= G; suppose A10: a <> 0; set d = r/(2* abs(a)); abs(a) > 0 & 2 > 0 by A10,ABSVALUE:6; then 2*abs(a) > 0 by REAL_2:122; then A11: d > 0 by A4,REAL_2:127; reconsider W' = W as Point of RealSpace by Th24,METRIC_1:def 14; reconsider H = Ball(W',d) as Subset of R^1 by Th24,METRIC_1:def 14 ; H is open by Def7,Th21; then Int H = H by TOPS_1:55; then W in Int H by A11,Lm1; then reconsider H as a_neighborhood of W by CONNSP_2:def 1; A12: f.:H c= Ball(Y,r) proof let y be set; assume y in f.:H; then consider x being set such that A13: x in dom f & x in H & y = f.x by FUNCT_1:def 12; reconsider y'=y as Real by A13,Th24,FUNCT_2:7; reconsider x'=x as Point of RealSpace by A13; reconsider Y' = Y as Real by METRIC_1:def 14; reconsider W'' = W' as Real by Th24; reconsider x'' = x' as Real by METRIC_1:def 14; dist(W',x') < d by A13,METRIC_1:12; then abs( W'' - x'' ) < d & abs(a) > 0 by A10,Th15,ABSVALUE:6; then abs(a)*abs( W'' - x'' ) < abs(a)*d by REAL_1:70; then abs(a*(W'' - x'')) < abs(a)*d by ABSVALUE:10; then abs(a*W'' - a*x'') < abs(a)*d by XCMPLX_1:40; then abs((a*W''+b) - (a*x''+b)) < abs(a)*d by XCMPLX_1:32; then abs(Y' - (a*x''+b)) < abs(a)*d by A1; then A14: abs(Y' - y') < abs(a)*d by A1,A13; abs(a) <> 0 & 2 <> 0 by A10,ABSVALUE:7; then A15: abs(a)*d = r/2 by XCMPLX_1:93; reconsider yy=y' as Point of RealSpace by METRIC_1:def 14; r/2+r/2 = r & r/2>=0 by A4,REAL_2:125,XCMPLX_1:66; then abs(Y'-y') < r by A14,A15,Lm3; then dist(Y,yy) < r by Th15; hence y in Ball(Y,r) by METRIC_1:12; end; Ball(Y,r) c= G by A3,A4,XBOOLE_1:1; then f.:H c= G by A12,XBOOLE_1:1; hence ex H being a_neighborhood of W st f.:H c= G; end; hence thesis; end; hence f is continuous by BORSUK_1:def 2; end;