Copyright (c) 1999 Association of Mizar Users
environ vocabulary RELAT_1, SEQ_1, ORDERS_1, YELLOW_0, FUNCT_1, CAT_1, RELAT_2, WAYBEL_0, SEQM_3, PRE_TOPC, FUNCOP_1, QUANTAL1, ORDINAL2, BINOP_1, BOOLE, GROUP_6, LATTICES, FUNCT_3, BORSUK_1, WAYBEL_1, WELLORD1, BHSP_3, YELLOW_1, WAYBEL_3, GROUP_1, CARD_3, PBOOLE, LATTICE3, FUNCT_4, RLVECT_2, SUBSET_1, WAYBEL18, YELLOW_9, T_0TOPSP, TOPS_2, YELLOW16; notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_3, FUNCT_7, STRUCT_0, CARD_3, ZF_FUND1, PBOOLE, PRALG_1, PRE_CIRC, FUNCT_4, WELLORD1, ORDERS_1, LATTICE3, GRCAT_1, PRE_TOPC, TOPS_2, T_0TOPSP, BORSUK_1, QUANTAL1, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, YELLOW_9, WAYBEL_3, WAYBEL18; constructors PRE_CIRC, FUNCT_7, ENUMSET1, ORDERS_3, WAYBEL_1, T_0TOPSP, ZF_FUND1, QUANTAL1, GRCAT_1, TOPS_2, YELLOW_9, NATTRA_1, TOLER_1, WAYBEL18, BORSUK_1; clusters STRUCT_0, WAYBEL_0, WAYBEL_3, RELSET_1, YELLOW_1, LATTICE3, BORSUK_2, WAYBEL10, WAYBEL17, YELLOW_0, FUNCT_1, SUBSET_1, PRE_TOPC, TOPS_1, YELLOW_2, WAYBEL18, XBOOLE_0; requirements SUBSET, BOOLE; definitions TARSKI, RELAT_1, LATTICE3, YELLOW_0, BORSUK_1, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_3, T_0TOPSP, WAYBEL25, XBOOLE_0; theorems STRUCT_0, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, PRE_TOPC, BORSUK_1, TOPMETR, ORDERS_1, YELLOW12, ZF_FUND1, RELAT_1, FUNCT_2, FUNCT_1, ENUMSET1, WAYBEL_3, PBOOLE, FUNCOP_1, LATTICE3, CARD_3, TARSKI, ZFMISC_1, WELLORD1, GRCAT_1, QUANTAL1, FUNCT_4, YELLOW_9, WAYBEL20, FUNCT_7, TOPS_2, FUNCT_3, WAYBEL10, T_0TOPSP, WAYBEL15, YELLOW_6, PRALG_1, WAYBEL18, WAYBEL13, WAYBEL21, XBOOLE_0, XBOOLE_1, AMI_1; schemes PRALG_2; begin :: Poset retracts theorem for a,b being Relation holds a*b = a(#)b proof let a,b be Relation; thus a*b c= a(#)b proof let x be set; assume A1: x in a*b; then consider x1,x2 being set such that A2: x = [x1,x2] by RELAT_1:def 1; ex y being set st [x1,y] in a & [y,x2] in b by A1,A2,RELAT_1:def 8; hence thesis by A2,ZF_FUND1:def 1; end; let x be set; assume x in a(#)b; then ex u,v,w being set st x = [u,w] & [u,v] in a & [v,w] in b by ZF_FUND1:def 1; hence thesis by RELAT_1:def 8; end; theorem for X being set, L being non empty RelStr, S being non empty SubRelStr of L for f,g being Function of X, the carrier of S for f',g' being Function of X, the carrier of L st f' = f & g' = g & f <= g holds f' <= g' proof let X be set, L be non empty RelStr, S be non empty SubRelStr of L; let f,g be Function of X, the carrier of S; let f',g' be Function of X, the carrier of L such that A1: f' = f & g' = g & f <= g; let x be set; assume A2: x in X; then f.x in the carrier of S & g.x in the carrier of S by FUNCT_2:7; then reconsider a = f.x, b = g.x as Element of S; reconsider a' = a, b' = b as Element of L by YELLOW_0:59; take a', b'; thus a' = f'.x & b' = g'.x by A1; ex a,b being Element of S st a = f.x & b = g.x & a <= b by A1,A2,YELLOW_2:def 1; hence thesis by YELLOW_0:60; end; theorem for X being set, L being non empty RelStr for S being full non empty SubRelStr of L for f,g being Function of X, the carrier of S for f',g' being Function of X, the carrier of L st f' = f & g' = g & f' <= g' holds f <= g proof let X be set, L be non empty RelStr; let S be full non empty SubRelStr of L; let f,g be Function of X, the carrier of S; let f',g' be Function of X, the carrier of L such that A1: f' = f & g' = g & f' <= g'; let x be set; assume A2: x in X; then f.x in the carrier of S & g.x in the carrier of S by FUNCT_2:7; then reconsider a = f.x, b = g.x as Element of S; take a, b; thus a = f.x & b = g.x; ex a',b' being Element of L st a' = a & b' = b & a' <= b' by A1,A2,YELLOW_2:def 1; hence thesis by YELLOW_0:61; end; definition let S be non empty RelStr; let T be non empty reflexive antisymmetric RelStr; cluster directed-sups-preserving monotone map of S,T; existence proof consider x being Element of T; take f = S --> x; A1: f = (the carrier of S) --> x by BORSUK_1:def 3; thus f is directed-sups-preserving proof let X be Subset of S; assume A2: X is non empty directed; A3: f.:X = {x} proof thus f.:X c= {x} by A1,BORSUK_1:6; consider a being Element of X; A4: a in X by A2; then f.a = x & dom f = the carrier of S by A1,FUNCOP_1:13,19; then x in f.:X by A4,FUNCT_1:def 12; hence thesis by ZFMISC_1:37; end; assume ex_sup_of X,S; thus ex_sup_of f.:X, T by A3,YELLOW_0:38; thus sup (f.:X) = x by A3,YELLOW_0:39 .= f.sup X by A1,FUNCOP_1:13; end; let a,b be Element of S; f.a = x & f.b = x & x <= x by A1,FUNCOP_1:13; hence thesis; end; end; theorem for f,g being Function st f is idempotent & rng g c= rng f & rng g c= dom f holds f*g = g proof let f,g be Function; assume f is idempotent; then A1: f*f = f by QUANTAL1:def 9; assume A2: rng g c= rng f; assume rng g c= dom f; then A3: dom (f*g) = dom g by RELAT_1:46; now let x be set; assume x in dom g; then A4: (f*g).x = f.(g.x) & g.x in rng g by FUNCT_1:23,def 5; then consider a being set such that A5: a in dom f & g.x = f.a by A2,FUNCT_1:def 5; thus (f*g).x = g.x by A1,A4,A5,FUNCT_1:23; end; hence f*g = g by A3,FUNCT_1:9; end; definition let S be 1-sorted; cluster idempotent map of S,S; existence proof take f = id S; A1: the carrier of S = {} implies the carrier of S = {}; f = id the carrier of S by GRCAT_1:def 11; then f*f = f by A1,FUNCT_2:23; hence thesis by QUANTAL1:def 9; end; end; theorem Th5: for L being up-complete (non empty Poset) for S being directed-sups-inheriting full (non empty SubRelStr of L) holds S is up-complete proof let L be up-complete (non empty Poset); let S be directed-sups-inheriting full (non empty SubRelStr of L); now let X be non empty directed Subset of S; reconsider Y = X as non empty directed Subset of L by YELLOW_2:7; ex_sup_of Y,L by WAYBEL_0:75; hence ex_sup_of X,S by WAYBEL_0:7; end; hence S is up-complete by WAYBEL_0:75; end; theorem Th6: for L being up-complete (non empty Poset) for f being map of L, L st f is idempotent directed-sups-preserving holds Image f is directed-sups-inheriting proof let L be up-complete (non empty Poset); let f be map of L, L; assume A1: f is idempotent directed-sups-preserving; set S = subrelstr(rng f); consider a being Element of L; dom f = the carrier of L by FUNCT_2:def 1; then f.a in rng f by FUNCT_1:def 5; then the carrier of S is non empty by YELLOW_0:def 15; then reconsider S' = S as non empty full SubRelStr of L by STRUCT_0:def 1; S is directed-sups-inheriting proof let X be directed Subset of S; assume X <> {}; then X is non empty directed Subset of S'; then reconsider X'= X as non empty directed Subset of L by YELLOW_2:7; A2: f preserves_sup_of X' by A1,WAYBEL_0:def 37; assume ex_sup_of X,L; then A3: ex_sup_of f.:X',L & sup(f.:X') = f.sup X' by A2,WAYBEL_0:def 31; X c= the carrier of S; then X c= rng f by YELLOW_0:def 15; then sup X' = f.sup X' & the carrier of L <> {} by A1,A3,YELLOW_2:22; then "\/"(X, L) in rng f by FUNCT_2:6; hence "\/"(X, L) in the carrier of S by YELLOW_0:def 15; end; hence Image f is directed-sups-inheriting by YELLOW_2:def 2; end; canceled; theorem Th8: for S, T being non empty RelStr, f being map of T,S, g being map of S,T holds f*g = id S implies rng f = the carrier of S proof let S,T be non empty RelStr; let f be map of T,S, g be map of S,T such that A1: f*g = id S; id S = id the carrier of S & the carrier of T <> {} by GRCAT_1:def 11; hence rng f = the carrier of S by A1,FUNCT_2:29; end; theorem Th9: for T being non empty RelStr, S being non empty SubRelStr of T for f being map of T,S holds f*incl(S,T) = id S implies f is idempotent map of T, T proof let T be non empty RelStr, S be non empty SubRelStr of T; let f be map of T,S; assume A1: f*incl(S, T) = id S; then A2: rng f = the carrier of S by Th8; A3: the carrier of S c= the carrier of T by YELLOW_0:def 13; then incl(S, T) = id the carrier of S by YELLOW_9:def 1; then incl(S, T)*f = f by FUNCT_2:23; then A4: f*f = (id S)*f by A1,RELAT_1:55 .= (id the carrier of S)*f by GRCAT_1:def 11 .= f by FUNCT_2:23; dom f = the carrier of T by FUNCT_2:def 1; then f is Function of the carrier of T, the carrier of T by A2,A3,FUNCT_2:4 ; hence thesis by A4,QUANTAL1:def 9; end; definition let S,T be non empty Poset; let f be Function; pred f is_a_retraction_of T,S means:Def1: f is directed-sups-preserving map of T,S & f|the carrier of S = id S & S is directed-sups-inheriting full SubRelStr of T; pred f is_an_UPS_retraction_of T,S means:Def2: f is directed-sups-preserving map of T,S & ex g being directed-sups-preserving map of S,T st f*g = id S; end; definition let S,T be non empty Poset; pred S is_a_retract_of T means:Def3: ex f being map of T,S st f is_a_retraction_of T,S; pred S is_an_UPS_retract_of T means:Def4: ex f being map of T,S st f is_an_UPS_retraction_of T,S; end; theorem Th10: for S,T being non empty Poset, f being Function st f is_a_retraction_of T,S holds f*incl(S,T) = id S proof let S,T be non empty Poset, f be Function such that f is directed-sups-preserving map of T,S and A1: f|the carrier of S = id S and A2: S is directed-sups-inheriting full SubRelStr of T; the carrier of S c= the carrier of T by A2,YELLOW_0:def 13; hence f*incl(S, T) = f*id the carrier of S by YELLOW_9:def 1 .= id S by A1,RELAT_1:94; end; theorem Th11: for S being non empty Poset, T being up-complete (non empty Poset) for f being Function st f is_a_retraction_of T,S holds f is_an_UPS_retraction_of T,S proof let S be non empty Poset; let T be up-complete (non empty Poset), f be Function; assume A1: f is_a_retraction_of T,S; hence f is directed-sups-preserving map of T,S by Def1; S is directed-sups-inheriting full SubRelStr of T by A1,Def1; then reconsider g = incl(S,T) as directed-sups-preserving map of S,T by WAYBEL21:10; take g; thus f*g = id S by A1,Th10; end; theorem Th12: for S,T being non empty Poset, f being Function st f is_a_retraction_of T,S holds rng f = the carrier of S proof let S,T be non empty Poset, f be Function; assume f is_a_retraction_of T,S; then f*incl(S,T) = id S & f is map of T,S by Def1,Th10; hence thesis by Th8; end; theorem Th13: for S,T being non empty Poset, f being Function st f is_an_UPS_retraction_of T,S holds rng f = the carrier of S proof let S,T be non empty Poset, f be Function; assume f is directed-sups-preserving map of T,S & ex g being directed-sups-preserving map of S,T st f*g = id S; hence thesis by Th8; end; theorem Th14: for S,T being non empty Poset, f being Function st f is_a_retraction_of T,S holds f is idempotent map of T,T proof let S,T be non empty Poset, f be Function; assume f is_a_retraction_of T,S; then f*incl(S,T) = id S & f is map of T,S & S is SubRelStr of T by Def1, Th10; hence thesis by Th9; end; theorem Th15: for T,S being non empty Poset, f being map of T,T st f is_a_retraction_of T,S holds Image f = the RelStr of S proof let T,S be non empty Poset, f be map of T,T; assume f is_a_retraction_of T,S; then A1: rng f = the carrier of S & S is full SubRelStr of T by Def1,Th12; Image f = subrelstr rng f by YELLOW_2:def 2; then the carrier of Image f = rng f by YELLOW_0:def 15; hence thesis by A1,YELLOW_0:58; end; theorem Th16: for T being up-complete (non empty Poset) for S being non empty Poset, f being map of T,T st f is_a_retraction_of T,S holds f is directed-sups-preserving projection proof let T be up-complete (non empty Poset); let S be non empty Poset, f be map of T,T; assume A1: f is_a_retraction_of T,S; then reconsider g = f as directed-sups-preserving map of T,S by Def1; A2: f is_an_UPS_retraction_of T,S by A1,Th11; f is idempotent by A1,Th14; then A3: f = f*f by QUANTAL1:def 9 .= (f|rng f)*f by FUNCT_4:2 .= (f|the carrier of S)*f by A2,Th13 .= (id S)*f by A1,Def1 .= (id the carrier of S)*g by GRCAT_1:def 11; A4: S is full directed-sups-inheriting non empty SubRelStr of T by A1,Def1; then A5: incl(S,T) is directed-sups-preserving by WAYBEL21:10; the carrier of S c= the carrier of T by A4,YELLOW_0:def 13; then A6: incl(S,T) = id the carrier of S by YELLOW_9:def 1; hence f is directed-sups-preserving by A3,A5,WAYBEL20:29; f is directed-sups-preserving idempotent map of T,T by A1,A3,A5,A6,Th14, WAYBEL20:29; hence thesis by WAYBEL_1:def 13; end; theorem Th17: for S,T being non empty reflexive transitive RelStr for f being map of S,T holds f is isomorphic iff f is monotone & ex g being monotone map of T,S st f*g = id T & g*f = id S proof let S,T be non empty reflexive transitive RelStr, f be map of S,T; A1: id S = id the carrier of S & id T = id the carrier of T by GRCAT_1:def 11; hereby assume A2: f is isomorphic; hence f is monotone by WAYBEL_0:def 38; consider g being map of T,S such that A3: g = f qua Function" & g is monotone by A2,WAYBEL_0:def 38; reconsider g as monotone map of T,S by A3; take g; f is one-to-one & rng f = the carrier of T by A2,WAYBEL_0:66; hence f*g = id T & g*f = id S by A1,A3,FUNCT_2:35; end; assume A4: f is monotone; given g being monotone map of T,S such that A5: f*g = id T & g*f = id S; A6: f is one-to-one & rng f = the carrier of T by A1,A5,FUNCT_2:29; then g = f qua Function" by A1,A5,FUNCT_2:36; hence f is isomorphic by A4,A6,WAYBEL_0:def 38; end; theorem Th18: for S,T being non empty Poset holds S,T are_isomorphic iff ex f being monotone map of S,T, g being monotone map of T,S st f*g = id T & g*f = id S proof let S,T be non empty Poset; A1: id S = id the carrier of S & id T = id the carrier of T by GRCAT_1:def 11; hereby assume S,T are_isomorphic; then consider f being map of S,T such that A2: f is isomorphic by WAYBEL_1:def 8; reconsider f as monotone map of S,T by A2,WAYBEL_0:def 38; take f; consider g being map of T,S such that A3: g = f qua Function" & g is monotone by A2,WAYBEL_0:def 38; reconsider g as monotone map of T,S by A3; take g; f is one-to-one & rng f = the carrier of T by A2,WAYBEL_0:66; hence f*g = id T & g*f = id S by A1,A3,FUNCT_2:35; end; given f being monotone map of S,T, g being monotone map of T,S such that A4: f*g = id T & g*f = id S; take f; A5: f is one-to-one & rng f = the carrier of T by A1,A4,FUNCT_2:29; then g = f qua Function" by A1,A4,FUNCT_2:36; hence f is isomorphic by A5,WAYBEL_0:def 38; end; theorem for S,T being up-complete (non empty Poset) st S,T are_isomorphic holds S is_an_UPS_retract_of T & T is_an_UPS_retract_of S proof let S,T be up-complete (non empty Poset); assume S,T are_isomorphic; then consider f be monotone map of S,T, g be monotone map of T,S such that A1: f*g = id T & g*f = id S by Th18; f is isomorphic & g is isomorphic by A1,Th17; then f is sups-preserving & g is sups-preserving by WAYBEL13:20; then (for X being Subset of S st X is non empty directed holds f preserves_sup_of X) & for X being Subset of T st X is non empty directed holds g preserves_sup_of X by WAYBEL_0:def 33; then f is directed-sups-preserving & g is directed-sups-preserving by WAYBEL_0:def 37; then g is_an_UPS_retraction_of T,S & f is_an_UPS_retraction_of S,T by A1,Def2; hence thesis by Def4; end; theorem Th20: for T,S being non empty Poset for f being monotone map of T,S, g being monotone map of S,T st f*g = id S ex h being projection map of T,T st h = g*f & h|the carrier of Image h = id Image h & S, Image h are_isomorphic proof let T,S be non empty Poset; let f be monotone map of T,S, g be monotone map of S,T such that A1: f*g = id S; set h = g*f; A2: id S = id the carrier of S by GRCAT_1:def 11; h*h = h*g*f by RELAT_1:55 .= g*(id S)*f by A1,RELAT_1:55 .= h by A2,FUNCT_2:23; then h is idempotent monotone map of T,T by QUANTAL1:def 9,YELLOW_2:14; then reconsider h as projection map of T,T by WAYBEL_1:def 13; take h; thus h = g*f; id the carrier of Image h = id Image h by GRCAT_1:def 11; hence h|the carrier of Image h = h*id Image h by RELAT_1:94 .= h*(inclusion h) by WAYBEL_1:def 17 .= (corestr h)*(inclusion h) by WAYBEL_1:32 .= id Image h by WAYBEL_1:36; rng f = the carrier of S & dom g = the carrier of S by A1,Th8,FUNCT_2:def 1; then A4: rng h = rng g by RELAT_1:47; A5: Image h = subrelstr rng h & Image g = subrelstr rng g by YELLOW_2:def 2; then reconsider gg = corestr g as map of S, Image h by A4; take gg; A6: gg = g by WAYBEL_1:32; then A7: gg is one-to-one by A1,A2,FUNCT_2:29; A8: rng gg = the carrier of Image h by A4,A5,A6,YELLOW_0:def 15; now let x,y be Element of S; x <= y implies g.x <= g.y & gg.x in the carrier of Image h by WAYBEL_1:def 2; hence x <= y implies gg.x <= gg.y by A6,YELLOW_0:61; assume gg.x <= gg.y; then A9: g.x <= g.y by A6,YELLOW_0:60; (id S).x = x & (id S).y = y by GRCAT_1:11; then x = f.(g.x) & y = f.(g.y) by A1,FUNCT_2:21; hence x <= y by A9,WAYBEL_1:def 2; end; hence gg is isomorphic by A7,A8,WAYBEL_0:66; end; theorem Th21: for T being up-complete (non empty Poset), S being non empty Poset for f being Function st f is_an_UPS_retraction_of T,S ex h being directed-sups-preserving projection map of T,T st h is_a_retraction_of T, Image h & S, Image h are_isomorphic proof let T be up-complete (non empty Poset); let S be non empty Poset, f be Function such that A1: f is directed-sups-preserving map of T,S; given g being directed-sups-preserving map of S,T such that A2: f*g = id S; reconsider f as directed-sups-preserving map of T,S by A1; consider h being projection map of T,T such that A3: h = g*f and A4: h|the carrier of Image h = id Image h and A5: S, Image h are_isomorphic by A2,Th20; reconsider h as directed-sups-preserving projection map of T,T by A3,WAYBEL20:29; take h; reconsider R = Image h as non empty Poset; h = corestr h by WAYBEL_1:32; then A6: h is directed-sups-preserving map of T, R by WAYBEL20:22; R is directed-sups-inheriting full SubRelStr of T by Th6; hence h is_a_retraction_of T, Image h by A4,A6,Def1; thus thesis by A5; end; theorem Th22: for L being up-complete (non empty Poset) for S being non empty Poset st S is_a_retract_of L holds S is up-complete proof let L be up-complete (non empty Poset); let S be non empty Poset; given f being map of L,S such that A1: f is_a_retraction_of L,S; S is full directed-sups-inheriting (non empty SubRelStr of L) by A1,Def1; hence thesis by Th5; end; theorem Th23: for L being complete (non empty Poset) for S being non empty Poset st S is_a_retract_of L holds S is complete proof let L be complete (non empty Poset); let S be non empty Poset; given f being map of L, S such that A1: f is_a_retraction_of L,S; reconsider f as directed-sups-preserving projection map of L,L by A1,Th14,Th16; the RelStr of S = Image f & Image f is complete by A1,Th15,YELLOW_2:37; hence thesis by YELLOW_0:3; end; theorem Th24: for L being continuous complete LATTICE for S being non empty Poset st S is_a_retract_of L holds S is continuous proof let L be continuous complete LATTICE; let S be non empty Poset; given f being map of L,S such that A1: f is_a_retraction_of L,S; reconsider g = f as directed-sups-preserving projection map of L,L by A1,Th14,Th16; A2: Image g is continuous LATTICE by WAYBEL15:17; Image g = the RelStr of S by A1,Th15; hence S is continuous by A2,YELLOW12:15; end; theorem for L being up-complete (non empty Poset) for S being non empty Poset st S is_an_UPS_retract_of L holds S is up-complete proof let L be up-complete (non empty Poset); let S be non empty Poset; given f being map of L,S such that A1: f is_an_UPS_retraction_of L,S; consider h being directed-sups-preserving projection map of L,L such that A2: h is_a_retraction_of L, Image h & S, Image h are_isomorphic by A1,Th21; h = corestr h by WAYBEL_1:32; then Image h is_a_retract_of L by A2,Def3; then Image h is up-complete & Image h, S are_isomorphic by A2,Th22,WAYBEL_1 :7; hence thesis by WAYBEL13:30; end; theorem for L being complete (non empty Poset) for S being non empty Poset st S is_an_UPS_retract_of L holds S is complete proof let L be complete (non empty Poset), S be non empty Poset; given f being map of L, S such that A1: f is_an_UPS_retraction_of L,S; consider h being directed-sups-preserving projection map of L,L such that A2: h is_a_retraction_of L, Image h & S, Image h are_isomorphic by A1,Th21; h = corestr h by WAYBEL_1:32; then Image h is_a_retract_of L by A2,Def3; then Image h is complete & Image h, S are_isomorphic by A2,Th23,WAYBEL_1:7 ; hence thesis by WAYBEL20:18; end; theorem for L being continuous complete LATTICE for S being non empty Poset st S is_an_UPS_retract_of L holds S is continuous proof let L be continuous complete LATTICE; let S be non empty Poset; given f being map of L,S such that A1: f is_an_UPS_retraction_of L,S; consider h being directed-sups-preserving projection map of L,L such that A2: h is_a_retraction_of L, Image h & S, Image h are_isomorphic by A1,Th21; h = corestr h by WAYBEL_1:32; then Image h is_a_retract_of L by A2,Def3; then Image h is continuous & Image h, S are_isomorphic by A2,Th24,WAYBEL_1: 7; hence thesis by WAYBEL15:11; end; theorem Th28: for L being RelStr for S being full SubRelStr of L for R being SubRelStr of S holds R is full iff R is full SubRelStr of L proof let L be RelStr, S be full SubRelStr of L, R be SubRelStr of S; reconsider R' = R as SubRelStr of L by YELLOW_6:16; A1: the carrier of R c= the carrier of S by YELLOW_0:def 13; hereby assume R is full; then the InternalRel of R = (the InternalRel of S)|_2 the carrier of R by YELLOW_0:def 14 .= ((the InternalRel of L)|_2 the carrier of S)|_2 the carrier of R by YELLOW_0:def 14 .= (the InternalRel of L)|_2 the carrier of R' by A1,WELLORD1:29; hence R is full SubRelStr of L by YELLOW_0:def 14; end; assume A2: R is full SubRelStr of L; ((the InternalRel of L)|_2 the carrier of S)|_2 the carrier of R = (the InternalRel of L)|_2 the carrier of R by A1,WELLORD1:29 .= the InternalRel of R by A2,YELLOW_0:def 14; hence the InternalRel of R = (the InternalRel of S)|_2 the carrier of R by YELLOW_0:def 14; end; theorem for L being non empty transitive RelStr for S being directed-sups-inheriting non empty full SubRelStr of L for R being directed-sups-inheriting non empty SubRelStr of S holds R is directed-sups-inheriting SubRelStr of L proof let L be non empty transitive RelStr; let S be directed-sups-inheriting non empty full SubRelStr of L; let R be directed-sups-inheriting non empty SubRelStr of S; reconsider T = R as SubRelStr of L by YELLOW_6:16; T is directed-sups-inheriting proof let X be directed Subset of T; reconsider Y = X as directed Subset of S by YELLOW_2:7; assume A1: X <> {}; assume ex_sup_of X,L; then sup Y = "\/"(X,L) & ex_sup_of Y, S by A1,WAYBEL_0:7; hence "\/"(X,L) in the carrier of T by A1,WAYBEL_0:def 4; end; hence thesis; end; theorem for L being up-complete (non empty Poset) for S1,S2 being directed-sups-inheriting full non empty SubRelStr of L st S1 is SubRelStr of S2 holds S1 is directed-sups-inheriting full SubRelStr of S2 proof let L be up-complete (non empty Poset); let S1,S2 be directed-sups-inheriting full non empty SubRelStr of L; assume S1 is SubRelStr of S2; then reconsider S = S1 as SubRelStr of S2; S is directed-sups-inheriting proof let X be directed Subset of S; assume X <> {}; then reconsider Y1 = X as non empty directed Subset of S1; reconsider Y = Y1 as non empty directed Subset of L by YELLOW_2:7; reconsider Y2 = Y1 as non empty directed Subset of S2 by YELLOW_2:7; ex_sup_of Y, L by WAYBEL_0:75; then sup Y2 = sup Y & sup Y = sup Y1 by WAYBEL_0:7; then sup Y2 in the carrier of S1; hence thesis; end; hence thesis by Th28; end; begin :: Products definition let R be Relation; attr R is Poset-yielding means:Def5: for x being set st x in rng R holds x is Poset; end; definition cluster Poset-yielding -> RelStr-yielding reflexive-yielding Relation; coherence proof let R be Relation; assume A1: for x being set st x in rng R holds x is Poset; hence for x being set st x in rng R holds x is RelStr; thus for S being RelStr st S in rng R holds S is reflexive by A1; end; end; definition let X be non empty set; let L be non empty RelStr; let i be Element of X; let Y be Subset of L|^X; redefine func pi(Y,i) -> Subset of L; coherence proof reconsider Y' = Y as Subset of product (X --> L) by YELLOW_1:def 5; pi(Y',i) is Subset of (X --> L).i; hence thesis by FUNCOP_1:13; end; end; definition let X be set; let S be Poset; cluster X --> S -> Poset-yielding; coherence proof A1: rng (X --> S) c= {S} by FUNCOP_1:19; let x be set; assume x in rng (X --> S); hence thesis by A1,TARSKI:def 1; end; end; definition let I be set; cluster Poset-yielding non-Empty ManySortedSet of I; existence proof consider P being non empty Poset; take I --> P; thus thesis; end; end; definition let I be non empty set; let J be Poset-yielding non-Empty ManySortedSet of I; cluster product J -> transitive antisymmetric; coherence proof A1: now let i be Element of I; dom J = I by PBOOLE:def 3; then J.i in rng J by FUNCT_1:def 5; hence J.i is Poset by Def5; end; then for i being Element of I holds J.i is transitive; hence product J is transitive by WAYBEL_3:29; for i being Element of I holds J.i is antisymmetric by A1; hence thesis by WAYBEL_3:30; end; end; definition let I be non empty set; let J be Poset-yielding non-Empty ManySortedSet of I; let i be Element of I; redefine func J.i -> non empty Poset; coherence proof dom J = I by PBOOLE:def 3; then J.i in rng J by FUNCT_1:def 5; hence thesis by Def5; end; end; Lm1: now let I be non empty set; let J be Poset-yielding non-Empty ManySortedSet of I; let X be Subset of product J; deffunc F(Element of I) = sup pi(X,$1); consider f being ManySortedSet of I such that A1: for i being Element of I holds f.i = F(i) from LambdaDMS; A2: dom f = I by PBOOLE:def 3; now let i be Element of I; f.i = sup pi(X,i) by A1; hence f.i is Element of J.i; end; then reconsider f as Element of product J by A2,WAYBEL_3:27; assume A3: for i being Element of I holds ex_sup_of pi(X,i), J.i; take f; thus for i being Element of I holds f.i = sup pi(X,i) by A1; thus f is_>=_than X proof let x be Element of product J such that A4: x in X; now let i be Element of I; ex_sup_of pi(X,i), J.i & f.i = sup pi(X,i) by A1,A3; then f.i is_>=_than pi(X,i) & x.i in pi(X,i) by A4,CARD_3:def 6,YELLOW_0:30; hence x.i <= f.i by LATTICE3:def 9; end; hence thesis by WAYBEL_3:28; end; let g be Element of product J; assume A5: X is_<=_than g; now let i be Element of I; A6: f.i = sup pi(X,i) & ex_sup_of pi(X,i), J.i by A1,A3; g.i is_>=_than pi(X,i) proof let a be Element of J.i; assume a in pi(X,i); then consider h being Function such that A7: h in X & a = h.i by CARD_3:def 6; reconsider h as Element of product J by A7; h <= g by A5,A7,LATTICE3:def 9; hence a <= g.i by A7,WAYBEL_3:28; end; hence f.i <= g.i by A6,YELLOW_0:30; end; hence f <= g by WAYBEL_3:28; end; Lm2: now let I be non empty set; let J be Poset-yielding non-Empty ManySortedSet of I; let X be Subset of product J; deffunc F(Element of I) = inf pi(X,$1); consider f being ManySortedSet of I such that A1: for i being Element of I holds f.i = F(i) from LambdaDMS; A2: dom f = I by PBOOLE:def 3; now let i be Element of I; f.i = inf pi(X,i) by A1; hence f.i is Element of J.i; end; then reconsider f as Element of product J by A2,WAYBEL_3:27; assume A3: for i being Element of I holds ex_inf_of pi(X,i), J.i; take f; thus for i being Element of I holds f.i = inf pi(X,i) by A1; thus f is_<=_than X proof let x be Element of product J such that A4: x in X; now let i be Element of I; ex_inf_of pi(X,i), J.i & f.i = inf pi(X,i) by A1,A3; then f.i is_<=_than pi(X,i) & x.i in pi(X,i) by A4,CARD_3:def 6,YELLOW_0:31; hence x.i >= f.i by LATTICE3:def 8; end; hence thesis by WAYBEL_3:28; end; let g be Element of product J; assume A5: X is_>=_than g; now let i be Element of I; A6: f.i = inf pi(X,i) & ex_inf_of pi(X,i), J.i by A1,A3; g.i is_<=_than pi(X,i) proof let a be Element of J.i; assume a in pi(X,i); then consider h being Function such that A7: h in X & a = h.i by CARD_3:def 6; reconsider h as Element of product J by A7; h >= g by A5,A7,LATTICE3:def 8; hence a >= g.i by A7,WAYBEL_3:28; end; hence f.i >= g.i by A6,YELLOW_0:31; end; hence f >= g by WAYBEL_3:28; end; theorem Th31: for I being non empty set for J being Poset-yielding non-Empty ManySortedSet of I for f being Element of product J, X being Subset of product J holds f is_>=_than X iff for i being Element of I holds f.i is_>=_than pi(X,i) proof let I be non empty set; let J be Poset-yielding non-Empty ManySortedSet of I; let f be Element of product J, X be Subset of product J; hereby assume A1: f is_>=_than X; let i be Element of I; thus f.i is_>=_than pi(X, i) proof let x be Element of J.i; assume x in pi(X, i); then consider g being Function such that A2: g in X & x = g.i by CARD_3:def 6; reconsider g as Element of product J by A2; g <= f by A1,A2,LATTICE3:def 9; hence thesis by A2,WAYBEL_3:28; end; end; assume A3: for i being Element of I holds f.i is_>=_than pi(X,i); let g be Element of product J; assume A4: g in X; now let i be Element of I; g.i in pi(X,i) & f.i is_>=_than pi(X,i) by A3,A4,CARD_3:def 6; hence g.i <= f.i by LATTICE3:def 9; end; hence thesis by WAYBEL_3:28; end; theorem Th32: for I being non empty set for J being Poset-yielding non-Empty ManySortedSet of I for f being Element of product J, X being Subset of product J holds f is_<=_than X iff for i being Element of I holds f.i is_<=_than pi(X,i) proof let I be non empty set; let J be Poset-yielding non-Empty ManySortedSet of I; let f be Element of product J, X be Subset of product J; hereby assume A1: f is_<=_than X; let i be Element of I; thus f.i is_<=_than pi(X, i) proof let x be Element of J.i; assume x in pi(X, i); then consider g being Function such that A2: g in X & x = g.i by CARD_3:def 6; reconsider g as Element of product J by A2; g >= f by A1,A2,LATTICE3:def 8; hence thesis by A2,WAYBEL_3:28; end; end; assume A3: for i being Element of I holds f.i is_<=_than pi(X,i); let g be Element of product J; assume A4: g in X; now let i be Element of I; g.i in pi(X,i) & f.i is_<=_than pi(X,i) by A3,A4,CARD_3:def 6; hence g.i >= f.i by LATTICE3:def 8; end; hence thesis by WAYBEL_3:28; end; theorem Th33: for I being non empty set for J being Poset-yielding non-Empty ManySortedSet of I for X being Subset of product J holds ex_sup_of X, product J iff for i being Element of I holds ex_sup_of pi(X,i), J.i proof let I be non empty set; let J be Poset-yielding non-Empty ManySortedSet of I; let X be Subset of product J; hereby assume A1: ex_sup_of X, product J; let i be Element of I; set f = sup X; f is_>=_than X by A1,YELLOW_0:30; then A2: f.i is_>=_than pi(X, i) by Th31; now let x be Element of J.i; assume A3: pi(X,i) is_<=_than x; set g = f+*(i,x); A4: dom g = dom f & dom f = I by FUNCT_7:32,WAYBEL_3:27; then A5: g.i = x by FUNCT_7:33; now let j be Element of I; g.j = f.j or g.j = x & j = i by A5,FUNCT_7:34; hence g.j is Element of J.j; end; then reconsider g as Element of product J by A4,WAYBEL_3:27; A6: X is_<=_than f by A1,YELLOW_0:30; X is_<=_than g proof let h be Element of product J; assume h in X; then A7: h <= f & h.i in pi(X, i) by A6,CARD_3:def 6,LATTICE3:def 9; now let j be Element of I; g.j = f.j or g.j = x & j = i by A5,FUNCT_7:34; hence h.j <= g.j by A3,A7,LATTICE3:def 9,WAYBEL_3:28; end; hence h <= g by WAYBEL_3:28; end; then f <= g by A1,YELLOW_0:30; hence f.i <= x by A5,WAYBEL_3:28; end; hence ex_sup_of pi(X, i), J.i by A2,YELLOW_0:30; end; assume for i being Element of I holds ex_sup_of pi(X,i), J.i; then consider f being Element of product J such that for i being Element of I holds f.i = sup pi(X,i) and A8: f is_>=_than X and A9: for g being Element of product J st X is_<=_than g holds f <= g by Lm1; thus ex_sup_of X, product J by A8,A9,YELLOW_0:30; end; theorem Th34: for I being non empty set for J being Poset-yielding non-Empty ManySortedSet of I for X being Subset of product J holds ex_inf_of X, product J iff for i being Element of I holds ex_inf_of pi(X,i), J.i proof let I be non empty set; let J be Poset-yielding non-Empty ManySortedSet of I; let X be Subset of product J; hereby assume A1: ex_inf_of X, product J; let i be Element of I; set f = inf X; A2: f is_<=_than X by A1,YELLOW_0:31; then A3: f.i is_<=_than pi(X, i) by Th32; now let x be Element of J.i; assume A4: pi(X,i) is_>=_than x; set g = f+*(i,x); A5: dom g = dom f & dom f = I by FUNCT_7:32,WAYBEL_3:27; then A6: g.i = x by FUNCT_7:33; now let j be Element of I; g.j = f.j or g.j = x & j = i by A6,FUNCT_7:34; hence g.j is Element of J.j; end; then reconsider g as Element of product J by A5,WAYBEL_3:27; X is_>=_than g proof let h be Element of product J; assume h in X; then A7: h >= f & h.i in pi(X, i) by A2,CARD_3:def 6,LATTICE3:def 8; now let j be Element of I; g.j = f.j or g.j = x & j = i by A6,FUNCT_7:34; hence h.j >= g.j by A4,A7,LATTICE3:def 8,WAYBEL_3:28; end; hence h >= g by WAYBEL_3:28; end; then f >= g by A1,YELLOW_0:31; hence f.i >= x by A6,WAYBEL_3:28; end; hence ex_inf_of pi(X, i), J.i by A3,YELLOW_0:31; end; assume for i being Element of I holds ex_inf_of pi(X,i), J.i; then consider f being Element of product J such that for i being Element of I holds f.i = inf pi(X,i) and A8: f is_<=_than X and A9: for g being Element of product J st X is_>=_than g holds f >= g by Lm2; thus ex_inf_of X, product J by A8,A9,YELLOW_0:31; end; theorem Th35: for I being non empty set for J being Poset-yielding non-Empty ManySortedSet of I for X being Subset of product J st ex_sup_of X, product J for i being Element of I holds (sup X).i = sup pi(X,i) proof let I be non empty set; let J be Poset-yielding non-Empty ManySortedSet of I; let X be Subset of product J; assume ex_sup_of X, product J; then for i being Element of I holds ex_sup_of pi(X,i), J.i by Th33; then consider f being Element of product J such that A1: for i being Element of I holds f.i = sup pi(X,i) and A2: f is_>=_than X and A3: for g being Element of product J st X is_<=_than g holds f <= g by Lm1; sup X = f by A2,A3,YELLOW_0:30; hence thesis by A1; end; theorem Th36: for I being non empty set for J being Poset-yielding non-Empty ManySortedSet of I for X being Subset of product J st ex_inf_of X, product J for i being Element of I holds (inf X).i = inf pi(X,i) proof let I be non empty set; let J be Poset-yielding non-Empty ManySortedSet of I; let X be Subset of product J; assume ex_inf_of X, product J; then for i being Element of I holds ex_inf_of pi(X,i), J.i by Th34; then consider f being Element of product J such that A1: for i being Element of I holds f.i = inf pi(X,i) and A2: f is_<=_than X and A3: for g being Element of product J st X is_>=_than g holds f >= g by Lm2; inf X = f by A2,A3,YELLOW_0:31; hence thesis by A1; end; theorem Th37: for I being non empty set for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I for X being directed Subset of product J for i being Element of I holds pi(X,i) is directed proof let I be non empty set; let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; let X be directed Subset of product J; let i be Element of I; let x,y be Element of J.i; assume x in pi(X,i); then consider f being Function such that A1: f in X & x = f.i by CARD_3:def 6; assume y in pi(X,i); then consider g being Function such that A2: g in X & y = g.i by CARD_3:def 6; reconsider f,g as Element of product J by A1,A2; consider h being Element of product J such that A3: h in X & f <= h & g <= h by A1,A2,WAYBEL_0:def 1; take h.i; thus h.i in pi(X,i) by A3,CARD_3:def 6; thus thesis by A1,A2,A3,WAYBEL_3:28; end; theorem Th38: for I being non empty set for J,K being RelStr-yielding non-Empty ManySortedSet of I st for i being Element of I holds K.i is SubRelStr of J.i holds product K is SubRelStr of product J proof let I be non empty set; let J,K be RelStr-yielding non-Empty ManySortedSet of I such that A1: for i being Element of I holds K.i is SubRelStr of J.i; A2: the carrier of product K = product Carrier K by YELLOW_1:def 4; A3: the carrier of product J = product Carrier J by YELLOW_1:def 4; A4: dom Carrier J = I & dom Carrier K = I by PBOOLE:def 3; now let i be set; assume i in I; then reconsider j = i as Element of I; A5: (ex R being 1-sorted st R = J.j & (Carrier J).j = the carrier of R) & (ex R being 1-sorted st R = K.j & (Carrier K).j = the carrier of R) by PRALG_1:def 13; K.j is SubRelStr of J.j by A1; hence (Carrier K).i c= (Carrier J).i by A5,YELLOW_0:def 13; end; hence A6: the carrier of product K c= the carrier of product J by A2,A3,A4,CARD_3:38; let x,y be set; assume A7: [x,y] in the InternalRel of product K; then A8: x in the carrier of product K & y in the carrier of product K by ZFMISC_1:106; then reconsider x,y as Element of product K; reconsider f = x, g = y as Element of product J by A6,A8; A9: x <= y by A7,ORDERS_1:def 9; now let i be Element of I; K.i is SubRelStr of J.i & x.i <= y.i by A1,A9,WAYBEL_3:28; hence f.i <= g.i by YELLOW_0:60; end; then f <= g by WAYBEL_3:28; hence thesis by ORDERS_1:def 9; end; theorem Th39: for I being non empty set for J,K being RelStr-yielding non-Empty ManySortedSet of I st for i being Element of I holds K.i is full SubRelStr of J.i holds product K is full SubRelStr of product J proof let I be non empty set; let J,K be RelStr-yielding non-Empty ManySortedSet of I; assume A1: for i being Element of I holds K.i is full SubRelStr of J.i; then for i being Element of I holds K.i is SubRelStr of J.i; then reconsider S = product K as non empty SubRelStr of product J by Th38; A2: (the InternalRel of product J)|_2 the carrier of S = (the InternalRel of product J)/\[:the carrier of S,the carrier of S:] by WELLORD1:def 6; S is full proof the InternalRel of S c= the InternalRel of product J by YELLOW_0:def 13; hence the InternalRel of S c= (the InternalRel of product J)|_2 the carrier of S by A2,XBOOLE_1:19; let x,y be set; assume [x,y] in (the InternalRel of product J)|_2 the carrier of S; then A3: [x,y] in the InternalRel of product J & [x,y] in [:the carrier of S, the carrier of S:] by A2,XBOOLE_0:def 3 ; then x in the carrier of S & y in the carrier of S by ZFMISC_1:106; then reconsider x, y as Element of S; reconsider a = x, b = y as Element of product J by YELLOW_0:59; reconsider x, y as Element of product K; A4: a <= b by A3,ORDERS_1:def 9; now let i be Element of I; a.i <= b.i & K.i is full SubRelStr of J.i & x.i in the carrier of K. i by A1,A4,WAYBEL_3:28; hence x.i <= y.i by YELLOW_0:61; end; then x <= y by WAYBEL_3:28; hence thesis by ORDERS_1:def 9; end; hence thesis; end; theorem for L being non empty RelStr, S being non empty SubRelStr of L, X being set holds S|^X is SubRelStr of L|^X proof let L be non empty RelStr, S be non empty SubRelStr of L, X be set; A1: S|^X = product (X --> S) & L|^X = product (X --> L) by YELLOW_1:def 5; per cases; suppose X = {}; then S|^X = RelStr (#{{}}, id {{}}#) & L|^X = RelStr (#{{}}, id { {}}#) by YELLOW_1:27; hence thesis by YELLOW_6:15; suppose X <> {}; then reconsider X as non empty set; now let i be Element of X; (X --> L).i = L & (X --> S).i = S by FUNCOP_1:13; hence (X --> S).i is SubRelStr of (X --> L).i; end; hence thesis by A1,Th38; end; theorem Th41: for L being non empty RelStr, S be full non empty SubRelStr of L, X be set holds S|^X is full SubRelStr of L|^X proof let L be non empty RelStr, S be full non empty SubRelStr of L, X be set; A1: S|^X = product (X --> S) & L|^X = product (X --> L) by YELLOW_1:def 5; per cases; suppose X = {}; then S|^X = RelStr (#{{}}, id {{}}#) & L|^X = RelStr (#{{}},id {{}}#) by YELLOW_1:27; hence thesis by YELLOW_6:15; suppose X <> {}; then reconsider X as non empty set; now let i be Element of X; (X --> L).i = L & (X --> S).i = S by FUNCOP_1:13; hence (X --> S).i is full SubRelStr of (X --> L).i; end; hence thesis by A1,Th39; end; begin :: Inheritance definition let S,T be non empty RelStr, X be set; pred S inherits_sup_of X,T means:Def6: ex_sup_of X,T implies "\/"(X, T) in the carrier of S; pred S inherits_inf_of X,T means:Def7: ex_inf_of X,T implies "/\"(X, T) in the carrier of S; end; theorem Th42: for T being non empty transitive RelStr for S being full non empty SubRelStr of T for X being Subset of S holds S inherits_sup_of X,T iff (ex_sup_of X,T implies ex_sup_of X, S & sup X = "\/"(X, T)) proof let T be non empty transitive RelStr; let S be full non empty SubRelStr of T; let X be Subset of S; hereby assume that A1: S inherits_sup_of X,T and A2: ex_sup_of X,T; "\/"(X, T) in the carrier of S by A1,A2,Def6; hence ex_sup_of X, S & sup X = "\/"(X, T) by A2,YELLOW_0:65; end; assume A3: ex_sup_of X,T implies ex_sup_of X, S & sup X = "\/"(X, T); assume ex_sup_of X,T; hence thesis by A3; end; theorem for T being non empty transitive RelStr for S being full non empty SubRelStr of T for X being Subset of S holds S inherits_inf_of X,T iff (ex_inf_of X,T implies ex_inf_of X, S & inf X = "/\"(X, T)) proof let T be non empty transitive RelStr; let S be full non empty SubRelStr of T; let X be Subset of S; hereby assume that A1: S inherits_inf_of X,T and A2: ex_inf_of X,T; "/\"(X, T) in the carrier of S by A1,A2,Def7; hence ex_inf_of X, S & inf X = "/\"(X, T) by A2,YELLOW_0:64; end; assume A3: ex_inf_of X,T implies ex_inf_of X, S & inf X = "/\"(X, T); assume ex_inf_of X,T; hence thesis by A3; end; scheme ProductSupsInheriting { I() -> non empty set, J,K() -> Poset-yielding non-Empty ManySortedSet of I(), P[set, set] }: for X being Subset of product K() st P[X, product K()] holds product K() inherits_sup_of X, product J() provided A1: for X being Subset of product K() st P[X, product K()] for i being Element of I() holds P[pi(X, i), K().i] and A2: for i being Element of I() holds K().i is full SubRelStr of J().i and A3: for i being Element of I(), X being Subset of K().i st P[X, K().i] holds K().i inherits_sup_of X, J().i proof let X be Subset of product K() such that A4: P[X, product K()] and A5: ex_sup_of X, product J(); set f = "\/"(X, product J()); product K() is SubRelStr of product J() by A2,Th39; then the carrier of product K() c= the carrier of product J() by YELLOW_0:def 13; then X c= the carrier of product J() by XBOOLE_1:1; then reconsider Y = X as Subset of product J(); A6: dom f = I() by WAYBEL_3:27; now let i be Element of I(); P[pi(X, i), K().i] by A1,A4; then A7: K().i inherits_sup_of pi(X, i), J().i by A3; ex_sup_of pi(Y,i), J().i by A5,Th33; then sup pi(Y,i) in the carrier of K().i by A7,Def6; then f.i in the carrier of K().i by A5,Th35; hence f.i is Element of K().i; end; then "\/"(X, product J()) is Element of product K() by A6,WAYBEL_3:27; hence thesis; end; scheme PowerSupsInheriting { I() -> non empty set, L() -> non empty Poset, S() -> non empty full SubRelStr of L(), P[set, set] }: for X being Subset of S()|^I() st P[X, S()|^I()] holds S()|^I() inherits_sup_of X, L()|^I() provided A1: for X being Subset of S()|^I() st P[X, S()|^I()] for i being Element of I() holds P[pi(X, i), S()] and A2: for X being Subset of S() st P[X, S()] holds S() inherits_sup_of X, L() proof defpred p[set,set] means P[$1,$2]; reconsider K = I() --> S(), J = I() --> L() as Poset-yielding non-Empty ManySortedSet of I(); A3: S()|^I() = product K & L()|^I() = product J by YELLOW_1:def 5; A4: now let X be Subset of product K such that A5: p[X, product K]; let i be Element of I(); K.i = S() by FUNCOP_1:13; hence p[pi(X, i), K.i] by A1,A3,A5; end; A6: now let i be Element of I(); K.i = S() & J.i = L() by FUNCOP_1:13; hence K.i is full SubRelStr of J.i; end; A7: now let i be Element of I(), X be Subset of K.i such that A8: p[X, K.i]; K.i = S() & J.i = L() by FUNCOP_1:13; hence K.i inherits_sup_of X, J.i by A2,A8; end; for X being Subset of product K st p[X, product K] holds product K inherits_sup_of X, product J from ProductSupsInheriting(A4,A6,A7); hence thesis by A3; end; scheme ProductInfsInheriting { I() -> non empty set, J,K() -> Poset-yielding non-Empty ManySortedSet of I(), P[set, set] }: for X being Subset of product K() st P[X, product K()] holds product K() inherits_inf_of X, product J() provided A1: for X being Subset of product K() st P[X, product K()] for i being Element of I() holds P[pi(X, i), K().i] and A2: for i being Element of I() holds K().i is full SubRelStr of J().i and A3: for i being Element of I(), X being Subset of K().i st P[X, K().i] holds K().i inherits_inf_of X, J().i proof let X be Subset of product K() such that A4: P[X, product K()] and A5: ex_inf_of X, product J(); set f = "/\"(X, product J()); product K() is SubRelStr of product J() by A2,Th39; then the carrier of product K() c= the carrier of product J() by YELLOW_0:def 13; then X c= the carrier of product J() by XBOOLE_1:1; then reconsider Y = X as Subset of product J(); A6: dom f = I() by WAYBEL_3:27; now let i be Element of I(); P[pi(X, i), K().i] by A1,A4; then A7: K().i inherits_inf_of pi(X, i), J().i by A3; ex_inf_of pi(Y,i), J().i by A5,Th34; then inf pi(Y,i) in the carrier of K().i by A7,Def7; then f.i in the carrier of K().i by A5,Th36; hence f.i is Element of K().i; end; then "/\"(X, product J()) is Element of product K() by A6,WAYBEL_3:27; hence thesis; end; scheme PowerInfsInheriting { I() -> non empty set, L() -> non empty Poset, S() -> non empty full SubRelStr of L(), P[set, set] }: for X being Subset of S()|^I() st P[X, S()|^I()] holds S()|^I() inherits_inf_of X, L()|^I() provided A1: for X being Subset of S()|^I() st P[X, S()|^I()] for i being Element of I() holds P[pi(X, i), S()] and A2: for X being Subset of S() st P[X, S()] holds S() inherits_inf_of X, L() proof defpred p[set,set] means P[$1,$2]; reconsider K = I() --> S(), J = I() --> L() as Poset-yielding non-Empty ManySortedSet of I(); A3: S()|^I() = product K & L()|^I() = product J by YELLOW_1:def 5; A4: now let X be Subset of product K such that A5: p[X, product K]; let i be Element of I(); K.i = S() by FUNCOP_1:13; hence p[pi(X, i), K.i] by A1,A3,A5; end; A6: now let i be Element of I(); K.i = S() & J.i = L() by FUNCOP_1:13; hence K.i is full SubRelStr of J.i; end; A7: now let i be Element of I(), X be Subset of K.i such that A8: p[X, K.i]; K.i = S() & J.i = L() by FUNCOP_1:13; hence K.i inherits_inf_of X, J.i by A2,A8; end; for X being Subset of product K st p[X, product K] holds product K inherits_inf_of X, product J from ProductInfsInheriting(A4,A6,A7); hence thesis by A3; end; definition let I be set; let L be non empty RelStr; let X be non empty Subset of L|^I; let i be set; cluster pi(X,i) -> non empty; coherence proof L|^I = product (I --> L) by YELLOW_1:def 5; then reconsider Y = X as non empty Subset of product (I --> L); consider f being Element of Y; f in the carrier of product (I --> L); then f in product Carrier (I --> L) by YELLOW_1:def 4; then reconsider f as Function by AMI_1:22; f.i in pi(X,i) by CARD_3:def 6; hence thesis; end; end; theorem for L being non empty Poset for S being directed-sups-inheriting non empty full SubRelStr of L for X be non empty set holds S|^X is directed-sups-inheriting SubRelStr of L|^X proof let L be non empty Poset; let S be directed-sups-inheriting non empty full SubRelStr of L; let X be non empty set; reconsider SX = S|^X as full non empty SubRelStr of L|^X by Th41; defpred P[set, non empty reflexive RelStr] means $1 is directed non empty Subset of $2; A1: now let A be Subset of S|^X; assume P[A,S|^X]; then reconsider B = A as directed non empty Subset of S|^X; let i be Element of X; product (X --> S) = S|^X & (X --> S).i = S by FUNCOP_1:13,YELLOW_1:def 5; then pi(B, i) is directed non empty Subset of S by Th37; hence P[pi(A, i),S]; end; A2: now let X be Subset of S; assume P[X,S]; then ex_sup_of X,L implies ex_sup_of X, S & sup X = "\/"(X, L) by WAYBEL_0:7; hence S inherits_sup_of X, L by Th42; end; SX is directed-sups-inheriting proof let A be directed Subset of SX; for A being Subset of S|^X st P[A,S|^X] holds S|^X inherits_sup_of A, L|^X from PowerSupsInheriting(A1,A2); then A <> {} implies S|^X inherits_sup_of A, L|^X; hence thesis by Def6; end; hence thesis; end; definition let I be non empty set; let J be RelStr-yielding non-Empty ManySortedSet of I; let X be non empty Subset of product J; let i be set; cluster pi(X,i) -> non empty; coherence proof consider f being Element of X; f in the carrier of product J; then f in product Carrier J by YELLOW_1:def 4; then reconsider f as Function by AMI_1:22; f.i in pi(X,i) by CARD_3:def 6; hence thesis; end; end; theorem Th45: for X being non empty set for L being up-complete (non empty Poset) holds L|^X is up-complete proof let X be non empty set; let L be up-complete (non empty Poset); A1: L|^X = product (X --> L) by YELLOW_1:def 5; now let A be non empty directed Subset of L|^X; reconsider B = A as non empty directed Subset of product (X --> L) by A1; now let x be Element of X; A2: (X --> L).x = L by FUNCOP_1:13; pi(B,x) is directed non empty by Th37; hence ex_sup_of pi(A,x), (X --> L).x by A2,WAYBEL_0:75; end; hence ex_sup_of A,L|^X by A1,Th33; end; hence thesis by WAYBEL_0:75; end; definition let L be up-complete (non empty Poset); let X be non empty set; cluster L|^X -> up-complete; coherence by Th45; end; begin :: Topological retracts definition let T be TopSpace; cluster the topology of T -> non empty; coherence by PRE_TOPC:def 1; end; theorem Th46: for T being non empty TopSpace, S being non empty SubSpace of T for f being ::continuous map of T,S st f is_a_retraction holds rng f = the carrier of S proof let T be non empty TopSpace, S be non empty SubSpace of T; let f be map of T,S such that A1: for W being Point of T st W in the carrier of S holds f.W=W; thus rng f c= the carrier of S; [#]T = the carrier of T & [#]S = the carrier of S by PRE_TOPC:12; then A2: the carrier of S c= the carrier of T by PRE_TOPC:def 9; let x be set; assume A3: x in the carrier of S; then x in the carrier of T by A2; then f.x = x & x in dom f by A1,A3,FUNCT_2:def 1; hence thesis by FUNCT_1:def 5; end; theorem for T being non empty TopSpace, S being non empty SubSpace of T for f being continuous map of T,S st f is_a_retraction holds f is idempotent proof let T be non empty TopSpace, S be non empty SubSpace of T; let f be continuous map of T,S such that A1: f is_a_retraction; [#]T = the carrier of T & [#]S = the carrier of S by PRE_TOPC:12; then A2: the carrier of S c= the carrier of T by PRE_TOPC:def 9; A3: dom f = the carrier of T & rng f = the carrier of S by A1,Th46,FUNCT_2:def 1; then A4: dom (f*f) = the carrier of T by A2,RELAT_1:46; now let x be set; assume x in the carrier of T; then (f*f).x = f.(f.x) & f.x in rng f by A3,FUNCT_1:23,def 5; hence (f*f).x = f.x by A1,A2,A3,BORSUK_1:def 19; end; then f*f = f by A3,A4,FUNCT_1:9; hence thesis by QUANTAL1:def 9; end; theorem Th48: for T being non empty TopSpace, V being open Subset of T holds chi(V, the carrier of T) is continuous map of T, Sierpinski_Space proof let T be non empty TopSpace, V be open Subset of T; the carrier of Sierpinski_Space = {0,1} by WAYBEL18:def 9; then reconsider c = chi(V, the carrier of T) as map of T, Sierpinski_Space; c = chi(c"{1}, the carrier of T) by FUNCT_3:49; then A1: V = c"{1} by FUNCT_3:47; A2: c"{} = {}T by RELAT_1:171; A3: c"{0,1} = the carrier of T by FUNCT_2:48 .= [#]T by PRE_TOPC:12; now let W be Subset of Sierpinski_Space; assume W is open; then W in the topology of Sierpinski_Space by PRE_TOPC:def 5; then W in {{}, {1}, {0,1}} by WAYBEL18:def 9; hence c"W is open by A1,A2,A3,ENUMSET1:13; end; hence thesis by TOPS_2:55; end; theorem for T being non empty TopSpace, x,y being Element of T st for W being open Subset of T st y in W holds x in W holds (0,1) --> (y,x) is continuous map of Sierpinski_Space, T proof let T be non empty TopSpace; let x,y be Element of T such that A1: for W being open Subset of T st y in W holds x in W; A2: the carrier of Sierpinski_Space = {0,1} by WAYBEL18:def 9; then reconsider i = (0,1) --> (y,x) as map of Sierpinski_Space, T; A3: i.0 = y & i.1 = x by FUNCT_4:66; A4: 0 in {0,1} & 1 in {0,1} & 0 in {0} & not 1 in {0} by TARSKI:def 1,def 2; now let W be Subset of T; assume W is open; then A5: y in W & x in W or not y in W & x in W or not y in W & not x in W by A1; i"W = {} or i"W = {0} or i"W = {1} or i"W = {0,1} by A2,ZFMISC_1:42; then i"W in {{}, {1}, {0,1}} by A3,A4,A5,ENUMSET1:14,FUNCT_2:46; then i"W in the topology of Sierpinski_Space by WAYBEL18:def 9; hence i"W is open by PRE_TOPC:def 5; end; hence thesis by TOPS_2:55; end; theorem for T being non empty TopSpace, x,y being Element of T for V being open Subset of T st x in V & not y in V holds chi(V, the carrier of T)*((0,1) --> (y,x)) = id Sierpinski_Space proof let T be non empty TopSpace; let x,y be Element of T, V be open Subset of T such that A1: x in V & not y in V; A2: the carrier of Sierpinski_Space = {0,1} by WAYBEL18:def 9; then reconsider i = (0,1) --> (y,x) as map of Sierpinski_Space, T; reconsider c = chi(V, the carrier of T) as map of T, Sierpinski_Space by Th48; A3: i.0 = y & i.1 = x by FUNCT_4:66; A4: c.x = 1 & c.y = 0 by A1,FUNCT_3:def 3; now thus c*i is map of Sierpinski_Space, Sierpinski_Space; let a be Element of Sierpinski_Space; a = 0 or a = 1 by A2,TARSKI:def 2; hence (c*i).a = a by A3,A4,FUNCT_2:21 .= (id Sierpinski_Space).a by GRCAT_1:11; end; hence thesis by YELLOW_2:9; end; theorem for T being non empty 1-sorted, V,W being Subset of T for S being TopAugmentation of BoolePoset 1 for f, g being map of T, S st f = chi(V, the carrier of T) & g = chi(W, the carrier of T) holds V c= W iff f <= g proof let T be non empty 1-sorted, V,W be Subset of T; let S be TopAugmentation of BoolePoset 1; A1: the RelStr of S = BoolePoset 1 by YELLOW_9:def 4; let c1, c2 be map of T, S such that A2: c1 = chi(V, the carrier of T) & c2 = chi(W, the carrier of T); hereby assume A3: V c= W; now let z be set; assume z in the carrier of T; then reconsider x = z as Element of T; reconsider a = c1.x, b = c2.x as Element of BoolePoset 1 by A1; x in V & x in W or not x in V by A3; then c1.x = 1 & c2.x = 1 or c1.x = 0 by A2,FUNCT_3:def 3; then c1.x c= c2.x by XBOOLE_1:2; then a <= b by YELLOW_1:2; then c1.x <= c2.x by A1,YELLOW_0:1; hence ex a,b being Element of S st a = c1.z & b = c2.z & a <= b; end; hence c1 <= c2 by YELLOW_2:def 1; end; assume A4: c1 <= c2; let x be set; assume A5: x in V & not x in W; then reconsider x as Element of T; reconsider a = c1.x, b = c2.x as Element of BoolePoset 1 by A1; ex a,b being Element of S st a = c1.x & b = c2.x & a <= b by A4,YELLOW_2: def 1; then c1.x = 1 & c2.x = 0 & a <= b by A1,A2,A5,FUNCT_3:def 3,YELLOW_0:1; then 1 c= 0 & 0 c= 1 & 0 <> 1 by XBOOLE_1:2,YELLOW_1:2; hence thesis by XBOOLE_0:def 10; end; theorem for L being non empty RelStr, X being non empty set for R being full non empty SubRelStr of L|^X st for a being set holds a is Element of R iff ex x being Element of L st a = X --> x holds L, R are_isomorphic proof let L be non empty RelStr, X be non empty set; let R be full non empty SubRelStr of L|^X such that A1: for a being set holds a is Element of R iff ex x being Element of L st a = X --> x; deffunc F(set) = X --> $1; consider f being ManySortedSet of the carrier of L such that A2: for i being Element of L holds f.i = F(i) from LambdaDMS; A3: dom f = the carrier of L by PBOOLE:def 3; rng f c= the carrier of R proof let y be set; assume y in rng f; then consider x being set such that A4: x in dom f & y = f.x by FUNCT_1:def 5; reconsider x as Element of L by A3,A4; y = X --> x by A2,A4; then y is Element of R by A1; hence thesis; end; then f is Function of the carrier of L, the carrier of R by A3,FUNCT_2:4; then reconsider f as map of L, R; take f; A5: rng f = the carrier of R proof thus rng f c= the carrier of R; let x be set; assume x in the carrier of R; then reconsider a = x as Element of R; consider i being Element of L such that A6: a = X --> i by A1; a = f.i by A2,A6; hence thesis by A3,FUNCT_1:def 5; end; A7: f is one-to-one proof let x,y be Element of L; f.x = X --> x & f.y = X --> y by A2; then f.x = [:X,{x}:] & f.y = [:X,{y}:] by FUNCOP_1:def 2; then f.x = f.y implies {x} = {y} by ZFMISC_1:134; hence thesis by ZFMISC_1:6; end; now let x,y be Element of L; A8: f.x = X --> x & f.y = X --> y by A2; reconsider a = f.x, b = f.y as Element of L|^X by YELLOW_0:59; hereby assume A9: x <= y; X --> x <= X --> y proof let i be set; assume i in X; then (X --> x).i = x & (X --> y).i = y by FUNCOP_1:13; hence ex p,q being Element of L st p = (X --> x).i & q = (X --> y).i & p <= q by A9; end; then a <= b & f.x in the carrier of R by A8,WAYBEL10:12; hence f.x <= f.y by YELLOW_0:61; end; A10: L|^X = product (X --> L) by YELLOW_1:def 5; reconsider a' = a, b' = b as Element of product (X --> L) by YELLOW_1:def 5; consider i being Element of X; A11: (X --> L).i = L by FUNCOP_1:13; assume f.x <= f.y; then a <= b by YELLOW_0:60; then a'.i <= b'.i by A10,WAYBEL_3:28; then x <= (X --> y).i by A8,A11,FUNCOP_1:13; hence x <= y by FUNCOP_1:13; end; hence f is isomorphic by A5,A7,WAYBEL_0:66; end; theorem for S,T being non empty TopSpace holds S, T are_homeomorphic iff ex f being continuous map of S,T, g being continuous map of T,S st f*g = id T & g*f = id S proof let S,T be non empty TopSpace; A1: id T = id the carrier of T & id S = id the carrier of S by GRCAT_1:def 11; A2: [#]T = the carrier of T & [#]S = the carrier of S by PRE_TOPC:12; hereby assume S, T are_homeomorphic; then consider f being map of S,T such that A3: f is_homeomorphism by T_0TOPSP:def 1; reconsider f as continuous map of S,T by A3,TOPS_2:def 5; reconsider g = f" as continuous map of T,S by A3,TOPS_2:def 5; take f,g; f is one-to-one & rng f = [#]T & dom f = [#]S by A3,TOPS_2:def 5; hence f*g = id T & g*f = id S by A1,A2,TOPS_2:65; end; given f being continuous map of S,T, g being continuous map of T,S such that A4: f*g = id T & g*f = id S; take f; A5: f is one-to-one & rng f = [#]T & dom f = [#]S by A1,A2,A4,FUNCT_2:29,def 1 ; then g = f qua Function" by A1,A2,A4,FUNCT_2:36 .= f" by A5,TOPS_2:def 4; hence f is_homeomorphism by A5,TOPS_2:def 5; end; theorem Th54: for T, S, R being non empty TopSpace for f being map of T,S, g being map of S,T, h being map of S, R st f*g = id S & h is_homeomorphism holds (h*f)*(g*(h")) = id R proof let T, S, R be non empty TopSpace; let f be map of T,S, g be map of S,T, h be map of S, R such that A1: f*g = id S and A2: h is_homeomorphism; A3: h is one-to-one & rng h = [#]R & dom h = [#]S by A2,TOPS_2:def 5; thus (h*f)*(g*(h")) = (h*f)*g*(h") by RELAT_1:55 .= h*(f*g)*(h") by RELAT_1:55 .= h*(id the carrier of S)*(h") by A1,GRCAT_1:def 11 .= h*(h") by FUNCT_2:23 .= id rng h by A3,TOPS_2:65 .= id the carrier of R by A3,PRE_TOPC:12 .= id R by GRCAT_1:def 11; end; theorem Th55: for T, S, R being non empty TopSpace st S is_Retract_of T & S, R are_homeomorphic holds R is_Retract_of T proof let T, S, R be non empty TopSpace; given f being continuous map of S,T, g being continuous map of T,S such that A1: g*f = id S; given h being map of S,R such that A2: h is_homeomorphism; A3: h is continuous & h" is continuous by A2,TOPS_2:def 5; then reconsider f' = f*(h") as continuous map of R,T by TOPS_2:58; reconsider g' = h*g as continuous map of T,R by A3,TOPS_2:58; take f',g'; thus thesis by A1,A2,Th54; end; theorem Th56: for T being non empty TopSpace, S being non empty SubSpace of T holds incl(S,T) is continuous proof let T be non empty TopSpace, S be non empty SubSpace of T; the carrier of S c= the carrier of T by BORSUK_1:35; then incl(S,T) = id the carrier of S by YELLOW_9:def 1 .= id S by GRCAT_1:def 11; hence thesis by TOPMETR:7; end; theorem Th57: for T being non empty TopSpace for S being non empty SubSpace of T, f being continuous map of T,S st f is_a_retraction holds f*incl(S,T) = id S proof let T be non empty TopSpace, S be non empty SubSpace of T; let f be continuous map of T,S such that A1: f is_a_retraction; [#]T = the carrier of T & [#]S = the carrier of S by PRE_TOPC:12; then A2: the carrier of S c= the carrier of T by PRE_TOPC:def 9; then A3: incl(S,T) = id the carrier of S by YELLOW_9:def 1; now let x be Element of S; x in the carrier of S; then reconsider y = x as Point of T by A2; thus (f*incl(S,T)).x = f.((incl(S,T)).x) by FUNCT_2:21 .= f.x by A3,FUNCT_1:35 .= y by A1,BORSUK_1:def 19 .= (id S).x by GRCAT_1:11; end; hence thesis by YELLOW_2:9; end; theorem Th58: for T being non empty TopSpace, S being non empty SubSpace of T st S is_a_retract_of T holds S is_Retract_of T proof let T be non empty TopSpace, S be non empty SubSpace of T; given f be continuous map of T,S such that A1: f is_a_retraction; reconsider g = incl(S,T) as continuous map of S,T by Th56; take g,f; thus thesis by A1,Th57; end; theorem for R,T being non empty TopSpace holds R is_Retract_of T iff ex S being non empty SubSpace of T st S is_a_retract_of T & S,R are_homeomorphic proof let R,T be non empty TopSpace; hereby assume R is_Retract_of T; then consider f being map of T,T such that A1: f is continuous & f*f = f & Image f, R are_homeomorphic by WAYBEL18:def 8; reconsider S = Image f as non empty SubSpace of T; take S; f = corestr f by WAYBEL18:def 7; then reconsider f as continuous map of T,S by A1,WAYBEL18:11; [#]S = the carrier of S & [#]T = the carrier of T by PRE_TOPC:12; then the carrier of S c= the carrier of T by PRE_TOPC:def 9; then rng f c= the carrier of T by XBOOLE_1:1; then reconsider rf = rng f as Subset of T; now let x be Point of T; assume x in the carrier of S; then x in the carrier of T|rf by WAYBEL18:def 6; then x in [#](T|rf) by PRE_TOPC:12; then x in rng f by PRE_TOPC:def 10; then ex y being set st y in dom f & x = f.y by FUNCT_1:def 5; hence f.x = x by A1,FUNCT_1:23; end; then f is_a_retraction by BORSUK_1:def 19; hence S is_a_retract_of T & S, R are_homeomorphic by A1,BORSUK_1:def 20; end; given S being non empty SubSpace of T such that A2: S is_a_retract_of T & S,R are_homeomorphic; S is_Retract_of T by A2,Th58; hence R is_Retract_of T by A2,Th55; end;