:: TOPALG_2 semantic presentation begin registration let n be Element of NAT ; cluster non empty convex for Element of bool the carrier of (TOP-REAL n); existence ex b1 being Subset of (TOP-REAL n) st ( not b1 is empty & b1 is convex ) proof set a = the Point of (TOP-REAL n); take LSeg ( the Point of (TOP-REAL n), the Point of (TOP-REAL n)) ; ::_thesis: ( not LSeg ( the Point of (TOP-REAL n), the Point of (TOP-REAL n)) is empty & LSeg ( the Point of (TOP-REAL n), the Point of (TOP-REAL n)) is convex ) thus ( not LSeg ( the Point of (TOP-REAL n), the Point of (TOP-REAL n)) is empty & LSeg ( the Point of (TOP-REAL n), the Point of (TOP-REAL n)) is convex ) ; ::_thesis: verum end; end; definition let n be Element of NAT ; let T be SubSpace of TOP-REAL n; attrT is convex means :Def1: :: TOPALG_2:def 1 [#] T is convex Subset of (TOP-REAL n); end; :: deftheorem Def1 defines convex TOPALG_2:def_1_:_ for n being Element of NAT for T being SubSpace of TOP-REAL n holds ( T is convex iff [#] T is convex Subset of (TOP-REAL n) ); registration let n be Element of NAT ; cluster non empty convex -> non empty pathwise_connected for SubSpace of TOP-REAL n; coherence for b1 being non empty SubSpace of TOP-REAL n st b1 is convex holds b1 is pathwise_connected proof let T be non empty SubSpace of TOP-REAL n; ::_thesis: ( T is convex implies T is pathwise_connected ) assume A1: [#] T is convex Subset of (TOP-REAL n) ; :: according to TOPALG_2:def_1 ::_thesis: T is pathwise_connected let a, b be Point of T; :: according to BORSUK_2:def_3 ::_thesis: a,b are_connected A2: the carrier of T is Subset of (TOP-REAL n) by TSEP_1:1; ( a in the carrier of T & b in the carrier of T ) ; then reconsider a1 = a, b1 = b as Point of (TOP-REAL n) by A2; percases ( a1 <> b1 or a1 = b1 ) ; supposeA3: a1 <> b1 ; ::_thesis: a,b are_connected [#] ((TOP-REAL n) | (LSeg (a1,b1))) = LSeg (a1,b1) by PRE_TOPC:def_5; then A4: the carrier of ((TOP-REAL n) | (LSeg (a1,b1))) c= the carrier of T by A1, JORDAN1:def_1; then A5: (TOP-REAL n) | (LSeg (a1,b1)) is SubSpace of T by TSEP_1:4; LSeg (a1,b1) is_an_arc_of a1,b1 by A3, TOPREAL1:9; then consider h being Function of I[01],((TOP-REAL n) | (LSeg (a1,b1))) such that A6: h is being_homeomorphism and A7: ( h . 0 = a1 & h . 1 = b1 ) by TOPREAL1:def_1; reconsider f = h as Function of I[01],T by A4, FUNCT_2:7; take f ; :: according to BORSUK_2:def_1 ::_thesis: ( f is continuous & f . 0 = a & f . 1 = b ) h is continuous by A6, TOPS_2:def_5; hence f is continuous by A5, PRE_TOPC:26; ::_thesis: ( f . 0 = a & f . 1 = b ) thus ( f . 0 = a & f . 1 = b ) by A7; ::_thesis: verum end; suppose a1 = b1 ; ::_thesis: a,b are_connected hence a,b are_connected ; ::_thesis: verum end; end; end; end; registration let n be Element of NAT ; cluster non empty strict TopSpace-like convex for SubSpace of TOP-REAL n; existence ex b1 being SubSpace of TOP-REAL n st ( b1 is strict & not b1 is empty & b1 is convex ) proof TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is SubSpace of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by TSEP_1:2; then reconsider T = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) as SubSpace of TOP-REAL n by PRE_TOPC:35; take T ; ::_thesis: ( T is strict & not T is empty & T is convex ) thus ( T is strict & not T is empty ) ; ::_thesis: T is convex [#] (TOP-REAL n) = [#] TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) ; hence [#] T is convex Subset of (TOP-REAL n) ; :: according to TOPALG_2:def_1 ::_thesis: verum end; end; theorem :: TOPALG_2:1 for X being non empty TopSpace for Y being non empty SubSpace of X for x1, x2 being Point of X for y1, y2 being Point of Y for f being Path of y1,y2 st x1 = y1 & x2 = y2 & y1,y2 are_connected holds f is Path of x1,x2 proof let X be non empty TopSpace; ::_thesis: for Y being non empty SubSpace of X for x1, x2 being Point of X for y1, y2 being Point of Y for f being Path of y1,y2 st x1 = y1 & x2 = y2 & y1,y2 are_connected holds f is Path of x1,x2 let Y be non empty SubSpace of X; ::_thesis: for x1, x2 being Point of X for y1, y2 being Point of Y for f being Path of y1,y2 st x1 = y1 & x2 = y2 & y1,y2 are_connected holds f is Path of x1,x2 let x1, x2 be Point of X; ::_thesis: for y1, y2 being Point of Y for f being Path of y1,y2 st x1 = y1 & x2 = y2 & y1,y2 are_connected holds f is Path of x1,x2 let y1, y2 be Point of Y; ::_thesis: for f being Path of y1,y2 st x1 = y1 & x2 = y2 & y1,y2 are_connected holds f is Path of x1,x2 let f be Path of y1,y2; ::_thesis: ( x1 = y1 & x2 = y2 & y1,y2 are_connected implies f is Path of x1,x2 ) assume that A1: ( x1 = y1 & x2 = y2 ) and A2: y1,y2 are_connected ; ::_thesis: f is Path of x1,x2 the carrier of Y is Subset of X by TSEP_1:1; then reconsider g = f as Function of I[01],X by FUNCT_2:7; f is continuous by A2, BORSUK_2:def_2; then A3: g is continuous by PRE_TOPC:26; A4: ( g . 0 = x1 & g . 1 = x2 ) by A1, A2, BORSUK_2:def_2; then x1,x2 are_connected by A3, BORSUK_2:def_1; hence f is Path of x1,x2 by A4, A3, BORSUK_2:def_2; ::_thesis: verum end; set I = the carrier of I[01]; Lm1: the carrier of [:I[01],I[01]:] = [: the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def_2; Lm2: the carrier of [:(TOP-REAL 1),I[01]:] = [: the carrier of (TOP-REAL 1), the carrier of I[01]:] by BORSUK_1:def_2; Lm3: the carrier of [:R^1,I[01]:] = [: the carrier of R^1, the carrier of I[01]:] by BORSUK_1:def_2; Lm4: dom (id I[01]) = the carrier of I[01] by FUNCT_2:def_1; definition let n be Element of NAT ; let T be non empty convex SubSpace of TOP-REAL n; let P, Q be Function of I[01],T; func ConvexHomotopy (P,Q) -> Function of [:I[01],I[01]:],T means :Def2: :: TOPALG_2:def 2 for s, t being Element of I[01] for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds it . (s,t) = ((1 - t) * a1) + (t * b1); existence ex b1 being Function of [:I[01],I[01]:],T st for s, t being Element of I[01] for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds b1 . (s,t) = ((1 - t) * a1) + (t * b1) proof defpred S1[ Element of the carrier of I[01], Element of the carrier of I[01], set ] means ex a1, b1 being Point of (TOP-REAL n) st ( a1 = P . \$1 & b1 = Q . \$1 & \$3 = ((1 - \$2) * a1) + (\$2 * b1) ); A1: for x, y being Element of the carrier of I[01] ex z being Element of T st S1[x,y,z] proof let x, y be Element of the carrier of I[01]; ::_thesis: ex z being Element of T st S1[x,y,z] A2: the carrier of T is Subset of (TOP-REAL n) by TSEP_1:1; ( P . x in the carrier of T & Q . x in the carrier of T ) ; then reconsider a1 = P . x, b1 = Q . x as Point of (TOP-REAL n) by A2; set z = ((1 - y) * a1) + (y * b1); A3: y <= 1 by BORSUK_1:43; [#] T is convex Subset of (TOP-REAL n) by Def1; then A4: LSeg (a1,b1) c= [#] T by JORDAN1:def_1; ( y is Real & 0 <= y ) by BORSUK_1:43, XREAL_0:def_1; then ((1 - y) * a1) + (y * b1) in LSeg (a1,b1) by A3; hence ex z being Element of T st S1[x,y,z] by A4; ::_thesis: verum end; consider F being Function of [: the carrier of I[01], the carrier of I[01]:], the carrier of T such that A5: for x, y being Element of the carrier of I[01] holds S1[x,y,F . (x,y)] from BINOP_1:sch_3(A1); reconsider F = F as Function of [:I[01],I[01]:],T by Lm1; take F ; ::_thesis: for s, t being Element of I[01] for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds F . (s,t) = ((1 - t) * a1) + (t * b1) let x, y be Element of the carrier of I[01]; ::_thesis: for a1, b1 being Point of (TOP-REAL n) st a1 = P . x & b1 = Q . x holds F . (x,y) = ((1 - y) * a1) + (y * b1) ex a1, b1 being Point of (TOP-REAL n) st ( a1 = P . x & b1 = Q . x & F . (x,y) = ((1 - y) * a1) + (y * b1) ) by A5; hence for a1, b1 being Point of (TOP-REAL n) st a1 = P . x & b1 = Q . x holds F . (x,y) = ((1 - y) * a1) + (y * b1) ; ::_thesis: verum end; uniqueness for b1, b2 being Function of [:I[01],I[01]:],T st ( for s, t being Element of I[01] for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds b1 . (s,t) = ((1 - t) * a1) + (t * b1) ) & ( for s, t being Element of I[01] for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds b2 . (s,t) = ((1 - t) * a1) + (t * b1) ) holds b1 = b2 proof let f, g be Function of [:I[01],I[01]:],T; ::_thesis: ( ( for s, t being Element of I[01] for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds f . (s,t) = ((1 - t) * a1) + (t * b1) ) & ( for s, t being Element of I[01] for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds g . (s,t) = ((1 - t) * a1) + (t * b1) ) implies f = g ) assume that A6: for s, t being Element of I[01] for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds f . (s,t) = ((1 - t) * a1) + (t * b1) and A7: for s, t being Element of I[01] for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds g . (s,t) = ((1 - t) * a1) + (t * b1) ; ::_thesis: f = g for s, t being Element of the carrier of I[01] holds f . (s,t) = g . (s,t) proof let s, t be Element of the carrier of I[01]; ::_thesis: f . (s,t) = g . (s,t) reconsider a1 = P . s, b1 = Q . s as Point of (TOP-REAL n) by PRE_TOPC:25; f . (s,t) = ((1 - t) * a1) + (t * b1) by A6; hence f . (s,t) = g . (s,t) by A7; ::_thesis: verum end; hence f = g by Lm1, BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def2 defines ConvexHomotopy TOPALG_2:def_2_:_ for n being Element of NAT for T being non empty convex SubSpace of TOP-REAL n for P, Q being Function of I[01],T for b5 being Function of [:I[01],I[01]:],T holds ( b5 = ConvexHomotopy (P,Q) iff for s, t being Element of I[01] for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds b5 . (s,t) = ((1 - t) * a1) + (t * b1) ); Lm5: for n being Element of NAT for T being non empty convex SubSpace of TOP-REAL n for P, Q being continuous Function of I[01],T holds ConvexHomotopy (P,Q) is continuous proof let n be Element of NAT ; ::_thesis: for T being non empty convex SubSpace of TOP-REAL n for P, Q being continuous Function of I[01],T holds ConvexHomotopy (P,Q) is continuous let T be non empty convex SubSpace of TOP-REAL n; ::_thesis: for P, Q being continuous Function of I[01],T holds ConvexHomotopy (P,Q) is continuous let P, Q be continuous Function of I[01],T; ::_thesis: ConvexHomotopy (P,Q) is continuous set F = ConvexHomotopy (P,Q); A1: the carrier of T is Subset of (TOP-REAL n) by TSEP_1:1; then reconsider G = ConvexHomotopy (P,Q) as Function of [:I[01],I[01]:],(TOP-REAL n) by FUNCT_2:7; reconsider P1 = P, Q1 = Q as Function of I[01],(TOP-REAL n) by A1, FUNCT_2:7; set E = the carrier of (TOP-REAL n); set PI = [:P,(id I[01]):]; set QI = [:Q,(id I[01]):]; reconsider P1 = P1, Q1 = Q1 as continuous Function of I[01],(TOP-REAL n) by PRE_TOPC:26; set P1I = [:P1,(id I[01]):]; set Q1I = [:Q1,(id I[01]):]; deffunc H1( Element of the carrier of (TOP-REAL n), Element of the carrier of I[01]) -> Element of the carrier of (TOP-REAL n) = \$2 * \$1; deffunc H2( Element of the carrier of (TOP-REAL n), Element of the carrier of I[01]) -> Element of the carrier of (TOP-REAL n) = (1 - \$2) * \$1; consider Pa being Function of [: the carrier of (TOP-REAL n), the carrier of I[01]:], the carrier of (TOP-REAL n) such that A2: for x being Element of the carrier of (TOP-REAL n) for i being Element of the carrier of I[01] holds Pa . (x,i) = H2(x,i) from BINOP_1:sch_4(); consider Pb being Function of [: the carrier of (TOP-REAL n), the carrier of I[01]:], the carrier of (TOP-REAL n) such that A3: for x being Element of the carrier of (TOP-REAL n) for i being Element of the carrier of I[01] holds Pb . (x,i) = H1(x,i) from BINOP_1:sch_4(); the carrier of [:(TOP-REAL n),I[01]:] = [: the carrier of (TOP-REAL n), the carrier of I[01]:] by BORSUK_1:def_2; then reconsider Pa = Pa, Pb = Pb as Function of [:(TOP-REAL n),I[01]:],(TOP-REAL n) ; A4: Pb is continuous by A3, TOPALG_1:18; Pa is continuous by A2, TOPALG_1:17; then consider g being Function of [:I[01],I[01]:],(TOP-REAL n) such that A5: for r being Point of [:I[01],I[01]:] holds g . r = ((Pa * [:P1,(id I[01]):]) . r) + ((Pb * [:Q1,(id I[01]):]) . r) and A6: g is continuous by A4, JGRAPH_6:12; A7: for p being Point of [:I[01],I[01]:] holds G . p = ((Pa * [:P1,(id I[01]):]) . p) + ((Pb * [:Q1,(id I[01]):]) . p) proof A8: dom Q = the carrier of I[01] by FUNCT_2:def_1; A9: dom P = the carrier of I[01] by FUNCT_2:def_1; let p be Point of [:I[01],I[01]:]; ::_thesis: G . p = ((Pa * [:P1,(id I[01]):]) . p) + ((Pb * [:Q1,(id I[01]):]) . p) consider s, t being Point of I[01] such that A10: p = [s,t] by BORSUK_1:10; reconsider a1 = P . s, b1 = Q . s as Point of (TOP-REAL n) by PRE_TOPC:25; A11: (ConvexHomotopy (P,Q)) . (s,t) = ((1 - t) * a1) + (t * b1) by Def2; A12: (id I[01]) . t = t by FUNCT_1:18; A13: (Pb * [:Q,(id I[01]):]) . p = Pb . ([:Q,(id I[01]):] . (s,t)) by A10, FUNCT_2:15 .= Pb . ((Q . s),t) by A8, A12, Lm4, FUNCT_3:def_8 .= t * (Q1 . s) by A3 ; (Pa * [:P,(id I[01]):]) . p = Pa . ([:P,(id I[01]):] . (s,t)) by A10, FUNCT_2:15 .= Pa . ((P . s),t) by A9, A12, Lm4, FUNCT_3:def_8 .= (1 - t) * (P1 . s) by A2 ; hence G . p = ((Pa * [:P1,(id I[01]):]) . p) + ((Pb * [:Q1,(id I[01]):]) . p) by A10, A13, A11; ::_thesis: verum end; for p being Point of [:I[01],I[01]:] holds G . p = g . p proof let p be Point of [:I[01],I[01]:]; ::_thesis: G . p = g . p thus G . p = ((Pa * [:P1,(id I[01]):]) . p) + ((Pb * [:Q1,(id I[01]):]) . p) by A7 .= g . p by A5 ; ::_thesis: verum end; hence ConvexHomotopy (P,Q) is continuous by A6, FUNCT_2:63, PRE_TOPC:27; ::_thesis: verum end; Lm6: for n being Element of NAT for T being non empty convex SubSpace of TOP-REAL n for a, b being Point of T for P, Q being Path of a,b for s being Point of I[01] holds ( (ConvexHomotopy (P,Q)) . (s,0) = P . s & (ConvexHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds ( (ConvexHomotopy (P,Q)) . (0,t) = a & (ConvexHomotopy (P,Q)) . (1,t) = b ) ) ) proof let n be Element of NAT ; ::_thesis: for T being non empty convex SubSpace of TOP-REAL n for a, b being Point of T for P, Q being Path of a,b for s being Point of I[01] holds ( (ConvexHomotopy (P,Q)) . (s,0) = P . s & (ConvexHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds ( (ConvexHomotopy (P,Q)) . (0,t) = a & (ConvexHomotopy (P,Q)) . (1,t) = b ) ) ) reconsider x0 = 0 , x1 = 1 as Point of I[01] by BORSUK_1:def_14, BORSUK_1:def_15; let T be non empty convex SubSpace of TOP-REAL n; ::_thesis: for a, b being Point of T for P, Q being Path of a,b for s being Point of I[01] holds ( (ConvexHomotopy (P,Q)) . (s,0) = P . s & (ConvexHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds ( (ConvexHomotopy (P,Q)) . (0,t) = a & (ConvexHomotopy (P,Q)) . (1,t) = b ) ) ) let a, b be Point of T; ::_thesis: for P, Q being Path of a,b for s being Point of I[01] holds ( (ConvexHomotopy (P,Q)) . (s,0) = P . s & (ConvexHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds ( (ConvexHomotopy (P,Q)) . (0,t) = a & (ConvexHomotopy (P,Q)) . (1,t) = b ) ) ) let P, Q be Path of a,b; ::_thesis: for s being Point of I[01] holds ( (ConvexHomotopy (P,Q)) . (s,0) = P . s & (ConvexHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds ( (ConvexHomotopy (P,Q)) . (0,t) = a & (ConvexHomotopy (P,Q)) . (1,t) = b ) ) ) set F = ConvexHomotopy (P,Q); let s be Point of I[01]; ::_thesis: ( (ConvexHomotopy (P,Q)) . (s,0) = P . s & (ConvexHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds ( (ConvexHomotopy (P,Q)) . (0,t) = a & (ConvexHomotopy (P,Q)) . (1,t) = b ) ) ) reconsider a1 = P . s, b1 = Q . s as Point of (TOP-REAL n) by PRE_TOPC:25; A1: P . x0 = a by BORSUK_2:def_4; (ConvexHomotopy (P,Q)) . (s,x0) = ((1 - x0) * a1) + (x0 * b1) by Def2; hence (ConvexHomotopy (P,Q)) . (s,0) = a1 + (0 * b1) by EUCLID:29 .= a1 + (0. (TOP-REAL n)) by EUCLID:29 .= P . s by EUCLID:27 ; ::_thesis: ( (ConvexHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds ( (ConvexHomotopy (P,Q)) . (0,t) = a & (ConvexHomotopy (P,Q)) . (1,t) = b ) ) ) (ConvexHomotopy (P,Q)) . (s,x1) = ((1 - x1) * a1) + (x1 * b1) by Def2; hence (ConvexHomotopy (P,Q)) . (s,1) = (0. (TOP-REAL n)) + (1 * b1) by EUCLID:29 .= (0. (TOP-REAL n)) + b1 by EUCLID:29 .= Q . s by EUCLID:27 ; ::_thesis: for t being Point of I[01] holds ( (ConvexHomotopy (P,Q)) . (0,t) = a & (ConvexHomotopy (P,Q)) . (1,t) = b ) reconsider a1 = P . x0, b1 = Q . x0 as Point of (TOP-REAL n) by PRE_TOPC:25; let t be Point of I[01]; ::_thesis: ( (ConvexHomotopy (P,Q)) . (0,t) = a & (ConvexHomotopy (P,Q)) . (1,t) = b ) ( (ConvexHomotopy (P,Q)) . (0,t) = ((1 - t) * a1) + (t * b1) & Q . x0 = a ) by Def2, BORSUK_2:def_4; hence (ConvexHomotopy (P,Q)) . (0,t) = ((1 * a1) - (t * a1)) + (t * a1) by A1, EUCLID:50 .= 1 * a1 by EUCLID:48 .= a by A1, EUCLID:29 ; ::_thesis: (ConvexHomotopy (P,Q)) . (1,t) = b A2: Q . x1 = b by BORSUK_2:def_4; reconsider a1 = P . x1, b1 = Q . x1 as Point of (TOP-REAL n) by PRE_TOPC:25; A3: P . x1 = b by BORSUK_2:def_4; (ConvexHomotopy (P,Q)) . (1,t) = ((1 - t) * a1) + (t * b1) by Def2; hence (ConvexHomotopy (P,Q)) . (1,t) = ((1 * a1) - (t * b1)) + (t * a1) by A3, A2, EUCLID:50 .= 1 * b1 by A3, A2, EUCLID:48 .= b by A2, EUCLID:29 ; ::_thesis: verum end; theorem Th2: :: TOPALG_2:2 for n being Element of NAT for T being non empty convex SubSpace of TOP-REAL n for a, b being Point of T for P, Q being Path of a,b holds P,Q are_homotopic proof let n be Element of NAT ; ::_thesis: for T being non empty convex SubSpace of TOP-REAL n for a, b being Point of T for P, Q being Path of a,b holds P,Q are_homotopic let T be non empty convex SubSpace of TOP-REAL n; ::_thesis: for a, b being Point of T for P, Q being Path of a,b holds P,Q are_homotopic let a, b be Point of T; ::_thesis: for P, Q being Path of a,b holds P,Q are_homotopic let P, Q be Path of a,b; ::_thesis: P,Q are_homotopic take F = ConvexHomotopy (P,Q); :: according to BORSUK_2:def_7 ::_thesis: ( F is continuous & ( for b1 being Element of the carrier of I[01] holds ( F . (b1,0) = P . b1 & F . (b1,1) = Q . b1 & F . (0,b1) = a & F . (1,b1) = b ) ) ) thus F is continuous by Lm5; ::_thesis: for b1 being Element of the carrier of I[01] holds ( F . (b1,0) = P . b1 & F . (b1,1) = Q . b1 & F . (0,b1) = a & F . (1,b1) = b ) thus for b1 being Element of the carrier of I[01] holds ( F . (b1,0) = P . b1 & F . (b1,1) = Q . b1 & F . (0,b1) = a & F . (1,b1) = b ) by Lm6; ::_thesis: verum end; registration let n be Element of NAT ; let T be non empty convex SubSpace of TOP-REAL n; let a, b be Point of T; let P, Q be Path of a,b; cluster -> continuous for Homotopy of P,Q; coherence for b1 being Homotopy of P,Q holds b1 is continuous proof let F be Homotopy of P,Q; ::_thesis: F is continuous P,Q are_homotopic by Th2; hence F is continuous by BORSUK_6:def_11; ::_thesis: verum end; end; theorem Th3: :: TOPALG_2:3 for n being Element of NAT for T being non empty convex SubSpace of TOP-REAL n for a being Point of T for C being Loop of a holds the carrier of (pi_1 (T,a)) = {(Class ((EqRel (T,a)),C))} proof let n be Element of NAT ; ::_thesis: for T being non empty convex SubSpace of TOP-REAL n for a being Point of T for C being Loop of a holds the carrier of (pi_1 (T,a)) = {(Class ((EqRel (T,a)),C))} let T be non empty convex SubSpace of TOP-REAL n; ::_thesis: for a being Point of T for C being Loop of a holds the carrier of (pi_1 (T,a)) = {(Class ((EqRel (T,a)),C))} let a be Point of T; ::_thesis: for C being Loop of a holds the carrier of (pi_1 (T,a)) = {(Class ((EqRel (T,a)),C))} let C be Loop of a; ::_thesis: the carrier of (pi_1 (T,a)) = {(Class ((EqRel (T,a)),C))} set E = EqRel (T,a); hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {(Class ((EqRel (T,a)),C))} c= the carrier of (pi_1 (T,a)) let x be set ; ::_thesis: ( x in the carrier of (pi_1 (T,a)) implies x in {(Class ((EqRel (T,a)),C))} ) assume x in the carrier of (pi_1 (T,a)) ; ::_thesis: x in {(Class ((EqRel (T,a)),C))} then consider P being Loop of a such that A1: x = Class ((EqRel (T,a)),P) by TOPALG_1:47; P,C are_homotopic by Th2; then x = Class ((EqRel (T,a)),C) by A1, TOPALG_1:46; hence x in {(Class ((EqRel (T,a)),C))} by TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(Class ((EqRel (T,a)),C))} or x in the carrier of (pi_1 (T,a)) ) assume x in {(Class ((EqRel (T,a)),C))} ; ::_thesis: x in the carrier of (pi_1 (T,a)) then A2: x = Class ((EqRel (T,a)),C) by TARSKI:def_1; C in Loops a by TOPALG_1:def_1; then x in Class (EqRel (T,a)) by A2, EQREL_1:def_3; hence x in the carrier of (pi_1 (T,a)) by TOPALG_1:def_5; ::_thesis: verum end; registration let n be Element of NAT ; let T be non empty convex SubSpace of TOP-REAL n; let a be Point of T; cluster FundamentalGroup (T,a) -> trivial ; coherence pi_1 (T,a) is trivial proof set C = the constant Loop of a; set E = EqRel (T,a); the carrier of (pi_1 (T,a)) = Class (EqRel (T,a)) by TOPALG_1:def_5; then {(Class ((EqRel (T,a)), the constant Loop of a))} = Class (EqRel (T,a)) by Th3; hence pi_1 (T,a) is trivial by TOPALG_1:def_5; ::_thesis: verum end; end; begin theorem Th4: :: TOPALG_2:4 for a being real number holds |[a]| /. 1 = a proof let a be real number ; ::_thesis: |[a]| /. 1 = a reconsider y = a as Real by XREAL_0:def_1; thus |[a]| /. 1 = <*y*> /. 1 .= a by FINSEQ_4:16 ; ::_thesis: verum end; theorem :: TOPALG_2:5 for a, b being real number st a <= b holds [.a,b.] = { (((1 - l) * a) + (l * b)) where l is Real : ( 0 <= l & l <= 1 ) } proof let a, b be real number ; ::_thesis: ( a <= b implies [.a,b.] = { (((1 - l) * a) + (l * b)) where l is Real : ( 0 <= l & l <= 1 ) } ) set X = { (((1 - l) * a) + (l * b)) where l is Real : ( 0 <= l & l <= 1 ) } ; assume A1: a <= b ; ::_thesis: [.a,b.] = { (((1 - l) * a) + (l * b)) where l is Real : ( 0 <= l & l <= 1 ) } hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { (((1 - l) * a) + (l * b)) where l is Real : ( 0 <= l & l <= 1 ) } c= [.a,b.] let x be set ; ::_thesis: ( x in [.a,b.] implies b1 in { (((1 - b2) * a) + (b2 * b)) where l is Real : ( 0 <= b2 & b2 <= 1 ) } ) assume A2: x in [.a,b.] ; ::_thesis: b1 in { (((1 - b2) * a) + (b2 * b)) where l is Real : ( 0 <= b2 & b2 <= 1 ) } then reconsider y = x as Real ; A3: ( a <= y & y <= b ) by A2, XXREAL_1:1; percases ( a < b or a = b ) by A1, XXREAL_0:1; suppose a < b ; ::_thesis: b1 in { (((1 - b2) * a) + (b2 * b)) where l is Real : ( 0 <= b2 & b2 <= 1 ) } then A4: b - a > b - b by XREAL_1:15; reconsider l = (y - a) / (b - a) as Real ; l in the carrier of (Closed-Interval-TSpace (0,1)) by A3, BORSUK_6:2; then l in [.0,1.] by TOPMETR:18; then A5: ( 0 <= l & l <= 1 ) by XXREAL_1:1; ((1 - l) * a) + (l * b) = a + (l * (b - a)) .= a + (y - a) by A4, XCMPLX_1:87 .= y ; hence x in { (((1 - l) * a) + (l * b)) where l is Real : ( 0 <= l & l <= 1 ) } by A5; ::_thesis: verum end; suppose a = b ; ::_thesis: b1 in { (((1 - b2) * a) + (b2 * b)) where l is Real : ( 0 <= b2 & b2 <= 1 ) } then ((1 - 1) * a) + (1 * b) = y by A3, XXREAL_0:1; hence x in { (((1 - l) * a) + (l * b)) where l is Real : ( 0 <= l & l <= 1 ) } ; ::_thesis: verum end; end; end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (((1 - l) * a) + (l * b)) where l is Real : ( 0 <= l & l <= 1 ) } or x in [.a,b.] ) assume x in { (((1 - l) * a) + (l * b)) where l is Real : ( 0 <= l & l <= 1 ) } ; ::_thesis: x in [.a,b.] then consider l being Real such that A6: x = ((1 - l) * a) + (l * b) and A7: ( 0 <= l & l <= 1 ) ; ( a <= ((1 - l) * a) + (l * b) & ((1 - l) * a) + (l * b) <= b ) by A1, A7, XREAL_1:172, XREAL_1:173; hence x in [.a,b.] by A6, XXREAL_1:1; ::_thesis: verum end; theorem Th6: :: TOPALG_2:6 for F being Function of [:R^1,I[01]:],R^1 st ( for x being Point of R^1 for i being Point of I[01] holds F . (x,i) = (1 - i) * x ) holds F is continuous proof deffunc H1( Element of (TOP-REAL 1), Element of the carrier of I[01]) -> Element of the carrier of (TOP-REAL 1) = (1 - \$2) * \$1; consider G being Function of [: the carrier of (TOP-REAL 1), the carrier of I[01]:], the carrier of (TOP-REAL 1) such that A1: for x being Point of (TOP-REAL 1) for i being Point of I[01] holds G . (x,i) = H1(x,i) from BINOP_1:sch_4(); reconsider G = G as Function of [:(TOP-REAL 1),I[01]:],(TOP-REAL 1) by Lm2; consider f being Function of (TOP-REAL 1),R^1 such that A2: for p being Element of (TOP-REAL 1) holds f . p = p /. 1 by JORDAN2B:1; A3: f is being_homeomorphism by A2, JORDAN2B:28; then A4: f is continuous by TOPS_2:def_5; let F be Function of [:R^1,I[01]:],R^1; ::_thesis: ( ( for x being Point of R^1 for i being Point of I[01] holds F . (x,i) = (1 - i) * x ) implies F is continuous ) assume A5: for x being Point of R^1 for i being Point of I[01] holds F . (x,i) = (1 - i) * x ; ::_thesis: F is continuous A6: for x being Point of [:R^1,I[01]:] holds F . x = (f * (G * [:(f "),(id I[01]):])) . x proof reconsider ff = f as Function ; let x be Point of [:R^1,I[01]:]; ::_thesis: F . x = (f * (G * [:(f "),(id I[01]):])) . x consider a being Point of R^1, b being Point of I[01] such that A7: x = [a,b] by BORSUK_1:10; A8: dom (f ") = the carrier of R^1 by FUNCT_2:def_1; rng f = [#] R^1 by A3, TOPS_2:def_5; then A9: f is onto by FUNCT_2:def_3; A10: dom f = the carrier of (TOP-REAL 1) by FUNCT_2:def_1; set g = ff " ; consider z being Real such that A11: (1 - b) * ((f ") . a) = <*z*> by JORDAN2B:20; A12: <*a*> = |[a]| ; then reconsider w = <*a*> as Element of REAL 1 by EUCLID:22; A13: ff is one-to-one by A3, TOPS_2:def_5; f . <*a*> = |[a]| /. 1 by A2 .= a by Th4 ; then <*a*> = (ff ") . a by A10, A13, A12, FUNCT_1:32; then A14: w = (f /") . a by A9, A13, TOPS_2:def_4; A15: <*z*> = (1 - b) * ((f /") . a) by A11 .= (1 - b) * w by A14 .= <*((1 - b) * a)*> by RVSUM_1:47 ; thus (f * (G * [:(f "),(id I[01]):])) . x = f . ((G * [:(f "),(id I[01]):]) . x) by FUNCT_2:15 .= f . (G . ([:(f "),(id I[01]):] . (a,b))) by A7, FUNCT_2:15 .= f . (G . (((f ") . a),((id I[01]) . b))) by A8, Lm4, FUNCT_3:def_8 .= f . (G . (((f ") . a),b)) by FUNCT_1:18 .= f . ((1 - b) * ((f ") . a)) by A1 .= ((1 - b) * ((f ") . a)) /. 1 by A2 .= <*z*> /. 1 by A11 .= (1 - b) * a by A15, FINSEQ_4:16 .= F . (a,b) by A5 .= F . x by A7 ; ::_thesis: verum end; f " is continuous by A3, TOPS_2:def_5; then A16: [:(f "),(id I[01]):] is continuous ; G is continuous by A1, TOPALG_1:17; hence F is continuous by A4, A16, A6, FUNCT_2:63; ::_thesis: verum end; theorem Th7: :: TOPALG_2:7 for F being Function of [:R^1,I[01]:],R^1 st ( for x being Point of R^1 for i being Point of I[01] holds F . (x,i) = i * x ) holds F is continuous proof deffunc H1( Element of (TOP-REAL 1), Element of the carrier of I[01]) -> Element of the carrier of (TOP-REAL 1) = \$2 * \$1; consider G being Function of [: the carrier of (TOP-REAL 1), the carrier of I[01]:], the carrier of (TOP-REAL 1) such that A1: for x being Point of (TOP-REAL 1) for i being Point of I[01] holds G . (x,i) = H1(x,i) from BINOP_1:sch_4(); reconsider G = G as Function of [:(TOP-REAL 1),I[01]:],(TOP-REAL 1) by Lm2; consider f being Function of (TOP-REAL 1),R^1 such that A2: for p being Element of (TOP-REAL 1) holds f . p = p /. 1 by JORDAN2B:1; A3: f is being_homeomorphism by A2, JORDAN2B:28; then A4: f is continuous by TOPS_2:def_5; let F be Function of [:R^1,I[01]:],R^1; ::_thesis: ( ( for x being Point of R^1 for i being Point of I[01] holds F . (x,i) = i * x ) implies F is continuous ) assume A5: for x being Point of R^1 for i being Point of I[01] holds F . (x,i) = i * x ; ::_thesis: F is continuous A6: for x being Point of [:R^1,I[01]:] holds F . x = (f * (G * [:(f "),(id I[01]):])) . x proof reconsider ff = f as Function ; let x be Point of [:R^1,I[01]:]; ::_thesis: F . x = (f * (G * [:(f "),(id I[01]):])) . x consider a being Point of R^1, b being Point of I[01] such that A7: x = [a,b] by BORSUK_1:10; A8: dom (f ") = the carrier of R^1 by FUNCT_2:def_1; rng f = [#] R^1 by A3, TOPS_2:def_5; then A9: f is onto by FUNCT_2:def_3; A10: dom f = the carrier of (TOP-REAL 1) by FUNCT_2:def_1; set g = ff " ; consider z being Real such that A11: b * ((f ") . a) = <*z*> by JORDAN2B:20; A12: <*a*> = |[a]| ; then reconsider w = <*a*> as Element of REAL 1 by EUCLID:22; A13: ff is one-to-one by A3, TOPS_2:def_5; f . <*a*> = |[a]| /. 1 by A2 .= a by Th4 ; then <*a*> = (ff ") . a by A10, A13, A12, FUNCT_1:32; then A14: w = (f /") . a by A9, A13, TOPS_2:def_4; A15: <*z*> = b * ((f /") . a) by A11 .= b * w by A14 .= <*(b * a)*> by RVSUM_1:47 ; thus (f * (G * [:(f "),(id I[01]):])) . x = f . ((G * [:(f "),(id I[01]):]) . x) by FUNCT_2:15 .= f . (G . ([:(f "),(id I[01]):] . (a,b))) by A7, FUNCT_2:15 .= f . (G . (((f ") . a),((id I[01]) . b))) by A8, Lm4, FUNCT_3:def_8 .= f . (G . (((f ") . a),b)) by FUNCT_1:18 .= f . (b * ((f ") . a)) by A1 .= (b * ((f ") . a)) /. 1 by A2 .= <*z*> /. 1 by A11 .= z by FINSEQ_4:16 .= b * a by A15, FINSEQ_1:76 .= F . (a,b) by A5 .= F . x by A7 ; ::_thesis: verum end; f " is continuous by A3, TOPS_2:def_5; then A16: [:(f "),(id I[01]):] is continuous ; G is continuous by A1, TOPALG_1:18; hence F is continuous by A4, A16, A6, FUNCT_2:63; ::_thesis: verum end; registration cluster non empty V166() V167() V168() interval for Element of bool the carrier of R^1; existence ex b1 being Subset of R^1 st ( not b1 is empty & b1 is interval ) proof REAL c= the carrier of R^1 by TOPMETR:17; then reconsider P = REAL as non empty Subset of R^1 ; take P ; ::_thesis: ( not P is empty & P is interval ) thus not P is empty ; ::_thesis: P is interval let a, b be ext-real number ; :: according to XXREAL_2:def_12 ::_thesis: ( not a in P or not b in P or K58(a,b) c= P ) assume ( a in P & b in P ) ; ::_thesis: K58(a,b) c= P then reconsider a = a, b = b as Real ; [.a,b.] c= P ; hence K58(a,b) c= P ; ::_thesis: verum end; end; registration let T be real-membered TopStruct ; clusterV166() V167() V168() interval for Element of bool the carrier of T; existence ex b1 being Subset of T st b1 is interval proof take {} T ; ::_thesis: {} T is interval thus {} T is interval ; ::_thesis: verum end; end; definition let T be real-membered TopStruct ; attrT is interval means :Def3: :: TOPALG_2:def 3 [#] T is interval ; end; :: deftheorem Def3 defines interval TOPALG_2:def_3_:_ for T being real-membered TopStruct holds ( T is interval iff [#] T is interval ); Lm7: for T being SubSpace of R^1 st T = R^1 holds T is interval proof let T be SubSpace of R^1 ; ::_thesis: ( T = R^1 implies T is interval ) assume A1: T = R^1 ; ::_thesis: T is interval A2: [#] T = REAL by A1, TOPMETR:17; then reconsider P = [#] T as Subset of REAL ; P is interval by A2; hence [#] T is interval ; :: according to TOPALG_2:def_3 ::_thesis: verum end; registration cluster non empty strict TopSpace-like real-membered interval for SubSpace of R^1 ; existence ex b1 being SubSpace of R^1 st ( b1 is strict & not b1 is empty & b1 is interval ) proof reconsider T = R^1 as non empty strict SubSpace of R^1 by TSEP_1:2; take T ; ::_thesis: ( T is strict & not T is empty & T is interval ) thus ( T is strict & not T is empty & T is interval ) by Lm7; ::_thesis: verum end; end; definition :: original: R^1 redefine func R^1 -> interval SubSpace of R^1 ; coherence R^1 is interval SubSpace of R^1 by Lm7, TSEP_1:2; end; theorem Th8: :: TOPALG_2:8 for T being non empty interval SubSpace of R^1 for a, b being Point of T holds [.a,b.] c= the carrier of T proof let T be non empty interval SubSpace of R^1 ; ::_thesis: for a, b being Point of T holds [.a,b.] c= the carrier of T let a, b be Point of T; ::_thesis: [.a,b.] c= the carrier of T reconsider a1 = a, b1 = b as Point of R^1 by PRE_TOPC:25; [#] T is interval Subset of T by Def3; then [.a1,b1.] c= the carrier of T by XXREAL_2:def_12; hence [.a,b.] c= the carrier of T ; ::_thesis: verum end; registration cluster non empty interval -> non empty pathwise_connected for SubSpace of R^1 ; coherence for b1 being non empty SubSpace of R^1 st b1 is interval holds b1 is pathwise_connected proof let T be non empty SubSpace of R^1 ; ::_thesis: ( T is interval implies T is pathwise_connected ) assume A1: T is interval ; ::_thesis: T is pathwise_connected let a, b be Point of T; :: according to BORSUK_2:def_3 ::_thesis: a,b are_connected percases ( a <= b or b <= a ) ; supposeA2: a <= b ; ::_thesis: a,b are_connected set f = L[01] (((#) (a,b)),((a,b) (#))); set X = Closed-Interval-TSpace (a,b); A3: the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] by A2, TOPMETR:18; [.a,b.] c= the carrier of T by A1, Th8; then reconsider f = L[01] (((#) (a,b)),((a,b) (#))) as Function of I[01],T by A3, FUNCT_2:7, TOPMETR:20; take f ; :: according to BORSUK_2:def_1 ::_thesis: ( f is continuous & f . 0 = a & f . 1 = b ) the carrier of (Closed-Interval-TSpace (a,b)) is Subset of R^1 by TSEP_1:1; then reconsider g = f as Function of I[01],R^1 by FUNCT_2:7, TOPMETR:20; L[01] (((#) (a,b)),((a,b) (#))) is continuous by A2, TREAL_1:8; then g is continuous by PRE_TOPC:26, TOPMETR:20; hence f is continuous by PRE_TOPC:27; ::_thesis: ( f . 0 = a & f . 1 = b ) thus f . 0 = f . ((#) (0,1)) by TREAL_1:def_1 .= (#) (a,b) by A2, TREAL_1:9 .= a by A2, TREAL_1:def_1 ; ::_thesis: f . 1 = b thus f . 1 = f . ((0,1) (#)) by TREAL_1:def_2 .= (a,b) (#) by A2, TREAL_1:9 .= b by A2, TREAL_1:def_2 ; ::_thesis: verum end; supposeA4: b <= a ; ::_thesis: a,b are_connected set f = L[01] (((b,a) (#)),((#) (b,a))); set X = Closed-Interval-TSpace (b,a); A5: the carrier of (Closed-Interval-TSpace (b,a)) = [.b,a.] by A4, TOPMETR:18; [.b,a.] c= the carrier of T by A1, Th8; then reconsider f = L[01] (((b,a) (#)),((#) (b,a))) as Function of I[01],T by A5, FUNCT_2:7, TOPMETR:20; take f ; :: according to BORSUK_2:def_1 ::_thesis: ( f is continuous & f . 0 = a & f . 1 = b ) the carrier of (Closed-Interval-TSpace (b,a)) is Subset of R^1 by TSEP_1:1; then reconsider g = f as Function of I[01],R^1 by FUNCT_2:7, TOPMETR:20; L[01] (((b,a) (#)),((#) (b,a))) is continuous by A4, TREAL_1:8; then g is continuous by PRE_TOPC:26, TOPMETR:20; hence f is continuous by PRE_TOPC:27; ::_thesis: ( f . 0 = a & f . 1 = b ) thus f . 0 = f . ((#) (0,1)) by TREAL_1:def_1 .= (b,a) (#) by A4, TREAL_1:9 .= a by A4, TREAL_1:def_2 ; ::_thesis: f . 1 = b thus f . 1 = f . ((0,1) (#)) by TREAL_1:def_2 .= (#) (b,a) by A4, TREAL_1:9 .= b by A4, TREAL_1:def_1 ; ::_thesis: verum end; end; end; end; theorem Th9: :: TOPALG_2:9 for a, b being real number st a <= b holds Closed-Interval-TSpace (a,b) is interval proof let a, b be real number ; ::_thesis: ( a <= b implies Closed-Interval-TSpace (a,b) is interval ) set X = Closed-Interval-TSpace (a,b); assume a <= b ; ::_thesis: Closed-Interval-TSpace (a,b) is interval then [.a,b.] = [#] (Closed-Interval-TSpace (a,b)) by TOPMETR:18; hence [#] (Closed-Interval-TSpace (a,b)) is interval ; :: according to TOPALG_2:def_3 ::_thesis: verum end; theorem Th10: :: TOPALG_2:10 I[01] is interval by Th9, TOPMETR:20; theorem :: TOPALG_2:11 for a, b being real number st a <= b holds Closed-Interval-TSpace (a,b) is pathwise_connected proof let a, b be real number ; ::_thesis: ( a <= b implies Closed-Interval-TSpace (a,b) is pathwise_connected ) assume a <= b ; ::_thesis: Closed-Interval-TSpace (a,b) is pathwise_connected then reconsider X = Closed-Interval-TSpace (a,b) as non empty interval SubSpace of R^1 by Th9; X is pathwise_connected ; hence Closed-Interval-TSpace (a,b) is pathwise_connected ; ::_thesis: verum end; definition let T be non empty interval SubSpace of R^1 ; let P, Q be Function of I[01],T; func R1Homotopy (P,Q) -> Function of [:I[01],I[01]:],T means :Def4: :: TOPALG_2:def 4 for s, t being Element of I[01] holds it . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)); existence ex b1 being Function of [:I[01],I[01]:],T st for s, t being Element of I[01] holds b1 . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) proof defpred S1[ Element of the carrier of I[01], Element of the carrier of I[01], set ] means \$3 = ((1 - \$2) * (P . \$1)) + (\$2 * (Q . \$1)); A1: for m, n being Element of the carrier of I[01] ex z being Element of T st S1[m,n,z] proof let m, n be Element of the carrier of I[01]; ::_thesis: ex z being Element of T st S1[m,n,z] A2: 0 <= n by BORSUK_1:43; set z = ((1 - n) * (P . m)) + (n * (Q . m)); A3: n <= 1 by BORSUK_1:43; percases ( P . m <= Q . m or P . m > Q . m ) ; suppose P . m <= Q . m ; ::_thesis: ex z being Element of T st S1[m,n,z] then ( P . m <= ((1 - n) * (P . m)) + (n * (Q . m)) & ((1 - n) * (P . m)) + (n * (Q . m)) <= Q . m ) by A2, A3, XREAL_1:172, XREAL_1:173; then A4: ((1 - n) * (P . m)) + (n * (Q . m)) in [.(P . m),(Q . m).] by XXREAL_1:1; [.(P . m),(Q . m).] c= the carrier of T by Th8; hence ex z being Element of T st S1[m,n,z] by A4; ::_thesis: verum end; supposeA5: P . m > Q . m ; ::_thesis: ex z being Element of T st S1[m,n,z] 1 - 1 <= 1 - n by A3, XREAL_1:13; then (1 - n) * (Q . m) <= (1 - n) * (P . m) by A5, XREAL_1:64; then A6: ((1 - n) * (Q . m)) + (n * (Q . m)) <= ((1 - n) * (P . m)) + (n * (Q . m)) by XREAL_1:6; A7: [.(Q . m),(P . m).] c= the carrier of T by Th8; (Q . m) - (P . m) < (Q . m) - (Q . m) by A5, XREAL_1:15; then n * ((Q . m) - (P . m)) <= n * 0 by A2, XREAL_1:131; then (P . m) + (n * ((Q . m) - (P . m))) <= (P . m) + 0 by XREAL_1:6; then ((1 - n) * (P . m)) + (n * (Q . m)) in [.(Q . m),(P . m).] by A6, XXREAL_1:1; hence ex z being Element of T st S1[m,n,z] by A7; ::_thesis: verum end; end; end; consider F being Function of [: the carrier of I[01], the carrier of I[01]:], the carrier of T such that A8: for m, n being Element of the carrier of I[01] holds S1[m,n,F . (m,n)] from BINOP_1:sch_3(A1); reconsider F = F as Function of [:I[01],I[01]:],T by Lm1; take F ; ::_thesis: for s, t being Element of I[01] holds F . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) let s, t be Element of the carrier of I[01]; ::_thesis: F . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) thus F . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) by A8; ::_thesis: verum end; uniqueness for b1, b2 being Function of [:I[01],I[01]:],T st ( for s, t being Element of I[01] holds b1 . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) ) & ( for s, t being Element of I[01] holds b2 . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) ) holds b1 = b2 proof let f, g be Function of [:I[01],I[01]:],T; ::_thesis: ( ( for s, t being Element of I[01] holds f . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) ) & ( for s, t being Element of I[01] holds g . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) ) implies f = g ) assume that A9: for s, t being Element of I[01] holds f . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) and A10: for s, t being Element of I[01] holds g . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) ; ::_thesis: f = g for s, t being Element of the carrier of I[01] holds f . (s,t) = g . (s,t) proof let s, t be Element of the carrier of I[01]; ::_thesis: f . (s,t) = g . (s,t) thus f . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) by A9 .= g . (s,t) by A10 ; ::_thesis: verum end; hence f = g by Lm1, BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def4 defines R1Homotopy TOPALG_2:def_4_:_ for T being non empty interval SubSpace of R^1 for P, Q being Function of I[01],T for b4 being Function of [:I[01],I[01]:],T holds ( b4 = R1Homotopy (P,Q) iff for s, t being Element of I[01] holds b4 . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) ); Lm8: for T being non empty interval SubSpace of R^1 for P, Q being continuous Function of I[01],T holds R1Homotopy (P,Q) is continuous proof set E = the carrier of R^1; let T be non empty interval SubSpace of R^1 ; ::_thesis: for P, Q being continuous Function of I[01],T holds R1Homotopy (P,Q) is continuous let P, Q be continuous Function of I[01],T; ::_thesis: R1Homotopy (P,Q) is continuous set F = R1Homotopy (P,Q); set PI = [:P,(id I[01]):]; set QI = [:Q,(id I[01]):]; defpred S1[ Element of the carrier of R^1, Element of the carrier of I[01], set ] means \$3 = (1 - \$2) * \$1; defpred S2[ Element of the carrier of R^1, Element of the carrier of I[01], set ] means \$3 = \$2 * \$1; A1: the carrier of T is Subset of R^1 by TSEP_1:1; then reconsider G = R1Homotopy (P,Q) as Function of [:I[01],I[01]:],R^1 by FUNCT_2:7; reconsider P1 = P, Q1 = Q as Function of I[01],R^1 by A1, FUNCT_2:7; reconsider P1 = P1, Q1 = Q1 as continuous Function of I[01],R^1 by PRE_TOPC:26; set P1I = [:P1,(id I[01]):]; set Q1I = [:Q1,(id I[01]):]; A2: for x being Element of the carrier of R^1 for y being Element of the carrier of I[01] ex z being Element of the carrier of R^1 st S1[x,y,z] by TOPMETR:17; consider Pa being Function of [: the carrier of R^1, the carrier of I[01]:], the carrier of R^1 such that A3: for x being Element of the carrier of R^1 for i being Element of the carrier of I[01] holds S1[x,i,Pa . (x,i)] from BINOP_1:sch_3(A2); A4: for x being Element of the carrier of R^1 for y being Element of the carrier of I[01] ex z being Element of the carrier of R^1 st S2[x,y,z] proof let x be Element of the carrier of R^1; ::_thesis: for y being Element of the carrier of I[01] ex z being Element of the carrier of R^1 st S2[x,y,z] let y be Element of the carrier of I[01]; ::_thesis: ex z being Element of the carrier of R^1 st S2[x,y,z] y * x in REAL by XREAL_0:def_1; hence ex z being Element of the carrier of R^1 st S2[x,y,z] by TOPMETR:17; ::_thesis: verum end; consider Pb being Function of [: the carrier of R^1, the carrier of I[01]:], the carrier of R^1 such that A5: for x being Element of the carrier of R^1 for i being Element of the carrier of I[01] holds S2[x,i,Pb . (x,i)] from BINOP_1:sch_3(A4); reconsider Pa = Pa, Pb = Pb as Function of [:R^1,I[01]:],R^1 by Lm3; A6: Pb is continuous by A5, Th7; Pa is continuous by A3, Th6; then consider g being Function of [:I[01],I[01]:],R^1 such that A7: for p being Point of [:I[01],I[01]:] for r1, r2 being real number st (Pa * [:P1,(id I[01]):]) . p = r1 & (Pb * [:Q1,(id I[01]):]) . p = r2 holds g . p = r1 + r2 and A8: g is continuous by A6, JGRAPH_2:19; A9: for p being Point of [:I[01],I[01]:] holds G . p = ((Pa * [:P1,(id I[01]):]) . p) + ((Pb * [:Q1,(id I[01]):]) . p) proof A10: dom Q = the carrier of I[01] by FUNCT_2:def_1; A11: dom P = the carrier of I[01] by FUNCT_2:def_1; let p be Point of [:I[01],I[01]:]; ::_thesis: G . p = ((Pa * [:P1,(id I[01]):]) . p) + ((Pb * [:Q1,(id I[01]):]) . p) consider s, t being Point of I[01] such that A12: p = [s,t] by BORSUK_1:10; reconsider a1 = P . s, b1 = Q . s as Point of R^1 by PRE_TOPC:25; A13: P . s in the carrier of T ; A14: (R1Homotopy (P,Q)) . (s,t) = ((1 - t) * a1) + (t * b1) by Def4; A15: Q . s in the carrier of T ; A16: (id I[01]) . t = t by FUNCT_1:18; A17: (Pb * [:Q,(id I[01]):]) . p = Pb . ([:Q,(id I[01]):] . (s,t)) by A12, FUNCT_2:15 .= Pb . ((Q . s),t) by A10, A16, Lm4, FUNCT_3:def_8 .= t * (Q . s) by A1, A5, A15 ; (Pa * [:P,(id I[01]):]) . p = Pa . ([:P,(id I[01]):] . (s,t)) by A12, FUNCT_2:15 .= Pa . ((P . s),t) by A11, A16, Lm4, FUNCT_3:def_8 .= (1 - t) * (P . s) by A1, A3, A13 ; hence G . p = ((Pa * [:P1,(id I[01]):]) . p) + ((Pb * [:Q1,(id I[01]):]) . p) by A12, A17, A14; ::_thesis: verum end; for p being Point of [:I[01],I[01]:] holds G . p = g . p proof let p be Point of [:I[01],I[01]:]; ::_thesis: G . p = g . p thus G . p = ((Pa * [:P1,(id I[01]):]) . p) + ((Pb * [:Q1,(id I[01]):]) . p) by A9 .= g . p by A7 ; ::_thesis: verum end; hence R1Homotopy (P,Q) is continuous by A8, FUNCT_2:63, PRE_TOPC:27; ::_thesis: verum end; Lm9: for T being non empty interval SubSpace of R^1 for a, b being Point of T for P, Q being Path of a,b for s being Point of I[01] holds ( (R1Homotopy (P,Q)) . (s,0) = P . s & (R1Homotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds ( (R1Homotopy (P,Q)) . (0,t) = a & (R1Homotopy (P,Q)) . (1,t) = b ) ) ) proof let T be non empty interval SubSpace of R^1 ; ::_thesis: for a, b being Point of T for P, Q being Path of a,b for s being Point of I[01] holds ( (R1Homotopy (P,Q)) . (s,0) = P . s & (R1Homotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds ( (R1Homotopy (P,Q)) . (0,t) = a & (R1Homotopy (P,Q)) . (1,t) = b ) ) ) let a, b be Point of T; ::_thesis: for P, Q being Path of a,b for s being Point of I[01] holds ( (R1Homotopy (P,Q)) . (s,0) = P . s & (R1Homotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds ( (R1Homotopy (P,Q)) . (0,t) = a & (R1Homotopy (P,Q)) . (1,t) = b ) ) ) let P, Q be Path of a,b; ::_thesis: for s being Point of I[01] holds ( (R1Homotopy (P,Q)) . (s,0) = P . s & (R1Homotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds ( (R1Homotopy (P,Q)) . (0,t) = a & (R1Homotopy (P,Q)) . (1,t) = b ) ) ) set F = R1Homotopy (P,Q); let s be Point of I[01]; ::_thesis: ( (R1Homotopy (P,Q)) . (s,0) = P . s & (R1Homotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds ( (R1Homotopy (P,Q)) . (0,t) = a & (R1Homotopy (P,Q)) . (1,t) = b ) ) ) A1: ( P . 0[01] = a & Q . 0[01] = a ) by BORSUK_2:def_4; thus (R1Homotopy (P,Q)) . (s,0) = ((1 - 0) * (P . s)) + (0 * (Q . s)) by Def4, BORSUK_1:def_14 .= P . s ; ::_thesis: ( (R1Homotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds ( (R1Homotopy (P,Q)) . (0,t) = a & (R1Homotopy (P,Q)) . (1,t) = b ) ) ) thus (R1Homotopy (P,Q)) . (s,1) = ((1 - 1) * (P . s)) + (1 * (Q . s)) by Def4, BORSUK_1:def_15 .= Q . s ; ::_thesis: for t being Point of I[01] holds ( (R1Homotopy (P,Q)) . (0,t) = a & (R1Homotopy (P,Q)) . (1,t) = b ) let t be Point of I[01]; ::_thesis: ( (R1Homotopy (P,Q)) . (0,t) = a & (R1Homotopy (P,Q)) . (1,t) = b ) thus (R1Homotopy (P,Q)) . (0,t) = ((1 - t) * (P . 0[01])) + (t * (Q . 0[01])) by Def4 .= a by A1 ; ::_thesis: (R1Homotopy (P,Q)) . (1,t) = b A2: ( P . 1[01] = b & Q . 1[01] = b ) by BORSUK_2:def_4; thus (R1Homotopy (P,Q)) . (1,t) = ((1 - t) * (P . 1[01])) + (t * (Q . 1[01])) by Def4 .= b by A2 ; ::_thesis: verum end; theorem Th12: :: TOPALG_2:12 for T being non empty interval SubSpace of R^1 for a, b being Point of T for P, Q being Path of a,b holds P,Q are_homotopic proof let T be non empty interval SubSpace of R^1 ; ::_thesis: for a, b being Point of T for P, Q being Path of a,b holds P,Q are_homotopic let a, b be Point of T; ::_thesis: for P, Q being Path of a,b holds P,Q are_homotopic let P, Q be Path of a,b; ::_thesis: P,Q are_homotopic take F = R1Homotopy (P,Q); :: according to BORSUK_2:def_7 ::_thesis: ( F is continuous & ( for b1 being Element of the carrier of I[01] holds ( F . (b1,0) = P . b1 & F . (b1,1) = Q . b1 & F . (0,b1) = a & F . (1,b1) = b ) ) ) thus F is continuous by Lm8; ::_thesis: for b1 being Element of the carrier of I[01] holds ( F . (b1,0) = P . b1 & F . (b1,1) = Q . b1 & F . (0,b1) = a & F . (1,b1) = b ) thus for b1 being Element of the carrier of I[01] holds ( F . (b1,0) = P . b1 & F . (b1,1) = Q . b1 & F . (0,b1) = a & F . (1,b1) = b ) by Lm9; ::_thesis: verum end; registration let T be non empty interval SubSpace of R^1 ; let a, b be Point of T; let P, Q be Path of a,b; cluster -> continuous for Homotopy of P,Q; coherence for b1 being Homotopy of P,Q holds b1 is continuous proof let F be Homotopy of P,Q; ::_thesis: F is continuous P,Q are_homotopic by Th12; hence F is continuous by BORSUK_6:def_11; ::_thesis: verum end; end; theorem Th13: :: TOPALG_2:13 for T being non empty interval SubSpace of R^1 for a being Point of T for C being Loop of a holds the carrier of (pi_1 (T,a)) = {(Class ((EqRel (T,a)),C))} proof let T be non empty interval SubSpace of R^1 ; ::_thesis: for a being Point of T for C being Loop of a holds the carrier of (pi_1 (T,a)) = {(Class ((EqRel (T,a)),C))} let a be Point of T; ::_thesis: for C being Loop of a holds the carrier of (pi_1 (T,a)) = {(Class ((EqRel (T,a)),C))} let C be Loop of a; ::_thesis: the carrier of (pi_1 (T,a)) = {(Class ((EqRel (T,a)),C))} set E = EqRel (T,a); hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {(Class ((EqRel (T,a)),C))} c= the carrier of (pi_1 (T,a)) let x be set ; ::_thesis: ( x in the carrier of (pi_1 (T,a)) implies x in {(Class ((EqRel (T,a)),C))} ) assume x in the carrier of (pi_1 (T,a)) ; ::_thesis: x in {(Class ((EqRel (T,a)),C))} then consider P being Loop of a such that A1: x = Class ((EqRel (T,a)),P) by TOPALG_1:47; P,C are_homotopic by Th12; then x = Class ((EqRel (T,a)),C) by A1, TOPALG_1:46; hence x in {(Class ((EqRel (T,a)),C))} by TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(Class ((EqRel (T,a)),C))} or x in the carrier of (pi_1 (T,a)) ) assume x in {(Class ((EqRel (T,a)),C))} ; ::_thesis: x in the carrier of (pi_1 (T,a)) then A2: x = Class ((EqRel (T,a)),C) by TARSKI:def_1; C in Loops a by TOPALG_1:def_1; then x in Class (EqRel (T,a)) by A2, EQREL_1:def_3; hence x in the carrier of (pi_1 (T,a)) by TOPALG_1:def_5; ::_thesis: verum end; registration let T be non empty interval SubSpace of R^1 ; let a be Point of T; cluster FundamentalGroup (T,a) -> trivial ; coherence pi_1 (T,a) is trivial proof set C = the constant Loop of a; set E = EqRel (T,a); the carrier of (pi_1 (T,a)) = Class (EqRel (T,a)) by TOPALG_1:def_5; then {(Class ((EqRel (T,a)), the constant Loop of a))} = Class (EqRel (T,a)) by Th13; hence pi_1 (T,a) is trivial by TOPALG_1:def_5; ::_thesis: verum end; end; theorem :: TOPALG_2:14 for a, b being real number st a <= b holds for x, y being Point of (Closed-Interval-TSpace (a,b)) for P, Q being Path of x,y holds P,Q are_homotopic proof let a, b be real number ; ::_thesis: ( a <= b implies for x, y being Point of (Closed-Interval-TSpace (a,b)) for P, Q being Path of x,y holds P,Q are_homotopic ) assume A1: a <= b ; ::_thesis: for x, y being Point of (Closed-Interval-TSpace (a,b)) for P, Q being Path of x,y holds P,Q are_homotopic let x, y be Point of (Closed-Interval-TSpace (a,b)); ::_thesis: for P, Q being Path of x,y holds P,Q are_homotopic let P, Q be Path of x,y; ::_thesis: P,Q are_homotopic Closed-Interval-TSpace (a,b) is interval by A1, Th9; hence P,Q are_homotopic by Th12; ::_thesis: verum end; theorem :: TOPALG_2:15 for a, b being real number st a <= b holds for x being Point of (Closed-Interval-TSpace (a,b)) for C being Loop of x holds the carrier of (pi_1 ((Closed-Interval-TSpace (a,b)),x)) = {(Class ((EqRel ((Closed-Interval-TSpace (a,b)),x)),C))} proof let a, b be real number ; ::_thesis: ( a <= b implies for x being Point of (Closed-Interval-TSpace (a,b)) for C being Loop of x holds the carrier of (pi_1 ((Closed-Interval-TSpace (a,b)),x)) = {(Class ((EqRel ((Closed-Interval-TSpace (a,b)),x)),C))} ) assume A1: a <= b ; ::_thesis: for x being Point of (Closed-Interval-TSpace (a,b)) for C being Loop of x holds the carrier of (pi_1 ((Closed-Interval-TSpace (a,b)),x)) = {(Class ((EqRel ((Closed-Interval-TSpace (a,b)),x)),C))} let x be Point of (Closed-Interval-TSpace (a,b)); ::_thesis: for C being Loop of x holds the carrier of (pi_1 ((Closed-Interval-TSpace (a,b)),x)) = {(Class ((EqRel ((Closed-Interval-TSpace (a,b)),x)),C))} let C be Loop of x; ::_thesis: the carrier of (pi_1 ((Closed-Interval-TSpace (a,b)),x)) = {(Class ((EqRel ((Closed-Interval-TSpace (a,b)),x)),C))} Closed-Interval-TSpace (a,b) is interval by A1, Th9; hence the carrier of (pi_1 ((Closed-Interval-TSpace (a,b)),x)) = {(Class ((EqRel ((Closed-Interval-TSpace (a,b)),x)),C))} by Th13; ::_thesis: verum end; theorem :: TOPALG_2:16 for x, y being Point of I[01] for P, Q being Path of x,y holds P,Q are_homotopic by Th10, Th12; theorem :: TOPALG_2:17 for x being Point of I[01] for C being Loop of x holds the carrier of (pi_1 (I[01],x)) = {(Class ((EqRel (I[01],x)),C))} by Th10, Th13; registration let x be Point of I[01]; cluster FundamentalGroup (I[01],x) -> trivial ; coherence pi_1 (I[01],x) is trivial by Th10; end; registration let n be Element of NAT ; let T be non empty convex SubSpace of TOP-REAL n; let P, Q be continuous Function of I[01],T; cluster ConvexHomotopy (P,Q) -> continuous ; coherence ConvexHomotopy (P,Q) is continuous by Lm5; end; theorem :: TOPALG_2:18 for n being Element of NAT for T being non empty convex SubSpace of TOP-REAL n for a, b being Point of T for P, Q being Path of a,b holds ConvexHomotopy (P,Q) is Homotopy of P,Q proof let n be Element of NAT ; ::_thesis: for T being non empty convex SubSpace of TOP-REAL n for a, b being Point of T for P, Q being Path of a,b holds ConvexHomotopy (P,Q) is Homotopy of P,Q let T be non empty convex SubSpace of TOP-REAL n; ::_thesis: for a, b being Point of T for P, Q being Path of a,b holds ConvexHomotopy (P,Q) is Homotopy of P,Q let a, b be Point of T; ::_thesis: for P, Q being Path of a,b holds ConvexHomotopy (P,Q) is Homotopy of P,Q let P, Q be Path of a,b; ::_thesis: ConvexHomotopy (P,Q) is Homotopy of P,Q thus P,Q are_homotopic by Th2; :: according to BORSUK_6:def_11 ::_thesis: ( ConvexHomotopy (P,Q) is continuous & ( for b1 being Element of the carrier of I[01] holds ( (ConvexHomotopy (P,Q)) . (b1,0) = P . b1 & (ConvexHomotopy (P,Q)) . (b1,1) = Q . b1 & (ConvexHomotopy (P,Q)) . (0,b1) = a & (ConvexHomotopy (P,Q)) . (1,b1) = b ) ) ) thus ConvexHomotopy (P,Q) is continuous ; ::_thesis: for b1 being Element of the carrier of I[01] holds ( (ConvexHomotopy (P,Q)) . (b1,0) = P . b1 & (ConvexHomotopy (P,Q)) . (b1,1) = Q . b1 & (ConvexHomotopy (P,Q)) . (0,b1) = a & (ConvexHomotopy (P,Q)) . (1,b1) = b ) thus for b1 being Element of the carrier of I[01] holds ( (ConvexHomotopy (P,Q)) . (b1,0) = P . b1 & (ConvexHomotopy (P,Q)) . (b1,1) = Q . b1 & (ConvexHomotopy (P,Q)) . (0,b1) = a & (ConvexHomotopy (P,Q)) . (1,b1) = b ) by Lm6; ::_thesis: verum end; registration let T be non empty interval SubSpace of R^1 ; let P, Q be continuous Function of I[01],T; cluster R1Homotopy (P,Q) -> continuous ; coherence R1Homotopy (P,Q) is continuous by Lm8; end; theorem :: TOPALG_2:19 for T being non empty interval SubSpace of R^1 for a, b being Point of T for P, Q being Path of a,b holds R1Homotopy (P,Q) is Homotopy of P,Q proof let T be non empty interval SubSpace of R^1 ; ::_thesis: for a, b being Point of T for P, Q being Path of a,b holds R1Homotopy (P,Q) is Homotopy of P,Q let a, b be Point of T; ::_thesis: for P, Q being Path of a,b holds R1Homotopy (P,Q) is Homotopy of P,Q let P, Q be Path of a,b; ::_thesis: R1Homotopy (P,Q) is Homotopy of P,Q thus P,Q are_homotopic by Th12; :: according to BORSUK_6:def_11 ::_thesis: ( R1Homotopy (P,Q) is continuous & ( for b1 being Element of the carrier of I[01] holds ( (R1Homotopy (P,Q)) . (b1,0) = P . b1 & (R1Homotopy (P,Q)) . (b1,1) = Q . b1 & (R1Homotopy (P,Q)) . (0,b1) = a & (R1Homotopy (P,Q)) . (1,b1) = b ) ) ) thus R1Homotopy (P,Q) is continuous ; ::_thesis: for b1 being Element of the carrier of I[01] holds ( (R1Homotopy (P,Q)) . (b1,0) = P . b1 & (R1Homotopy (P,Q)) . (b1,1) = Q . b1 & (R1Homotopy (P,Q)) . (0,b1) = a & (R1Homotopy (P,Q)) . (1,b1) = b ) thus for b1 being Element of the carrier of I[01] holds ( (R1Homotopy (P,Q)) . (b1,0) = P . b1 & (R1Homotopy (P,Q)) . (b1,1) = Q . b1 & (R1Homotopy (P,Q)) . (0,b1) = a & (R1Homotopy (P,Q)) . (1,b1) = b ) by Lm9; ::_thesis: verum end;