:: WAYBEL21 semantic presentation begin definition let S, T be Semilattice; assume B1: ( S is upper-bounded implies T is upper-bounded ) ; mode SemilatticeHomomorphism of S,T -> Function of S,T means :Def1: :: WAYBEL21:def 1 for X being finite Subset of S holds it preserves_inf_of X; existence ex b1 being Function of S,T st for X being finite Subset of S holds b1 preserves_inf_of X proof reconsider f = the carrier of S --> (Top T) as Function of S,T ; take f ; ::_thesis: for X being finite Subset of S holds f preserves_inf_of X let X be finite Subset of S; ::_thesis: f preserves_inf_of X assume A1: ex_inf_of X,S ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of f .: X,T & "/\" ((f .: X),T) = f . ("/\" (X,S)) ) percases ( X = {} or X <> {} ) ; supposeA2: X = {} ; ::_thesis: ( ex_inf_of f .: X,T & "/\" ((f .: X),T) = f . ("/\" (X,S)) ) then A3: f .: X = {} ; hence ex_inf_of f .: X,T by B1, A1, A2, WAYBEL20:5, YELLOW_0:43; ::_thesis: "/\" ((f .: X),T) = f . ("/\" (X,S)) thus f . (inf X) = inf (f .: X) by A3, FUNCOP_1:7; ::_thesis: verum end; suppose X <> {} ; ::_thesis: ( ex_inf_of f .: X,T & "/\" ((f .: X),T) = f . ("/\" (X,S)) ) then reconsider A = X as non empty Subset of S ; set a = the Element of A; reconsider a = the Element of A as Element of S ; A4: dom f = the carrier of S by FUNCOP_1:13; f . a = Top T by FUNCOP_1:7; then Top T in f .: X by A4, FUNCT_1:def_6; then A5: {(Top T)} c= f .: X by ZFMISC_1:31; f .: X c= {(Top T)} by FUNCOP_1:81; then A6: {(Top T)} = f .: X by A5, XBOOLE_0:def_10; f . (inf X) = Top T by FUNCOP_1:7; hence ( ex_inf_of f .: X,T & "/\" ((f .: X),T) = f . ("/\" (X,S)) ) by A6, YELLOW_0:38, YELLOW_0:39; ::_thesis: verum end; end; end; end; :: deftheorem Def1 defines SemilatticeHomomorphism WAYBEL21:def_1_:_ for S, T being Semilattice st ( S is upper-bounded implies T is upper-bounded ) holds for b3 being Function of S,T holds ( b3 is SemilatticeHomomorphism of S,T iff for X being finite Subset of S holds b3 preserves_inf_of X ); registration let S, T be Semilattice; cluster Function-like V29( the carrier of S, the carrier of T) meet-preserving -> monotone for Element of K22(K23( the carrier of S, the carrier of T)); coherence for b1 being Function of S,T st b1 is meet-preserving holds b1 is monotone proof let f be Function of S,T; ::_thesis: ( f is meet-preserving implies f is monotone ) assume A1: f is meet-preserving ; ::_thesis: f is monotone let x, y be Element of S; :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or f . x <= f . y ) assume x <= y ; ::_thesis: f . x <= f . y then x = x "/\" y by YELLOW_0:25; then f . x = (f . x) "/\" (f . y) by A1, WAYBEL_6:1; hence f . x <= f . y by YELLOW_0:25; ::_thesis: verum end; end; registration let S be Semilattice; let T be upper-bounded Semilattice; cluster -> meet-preserving for SemilatticeHomomorphism of S,T; coherence for b1 being SemilatticeHomomorphism of S,T holds b1 is meet-preserving proof let f be SemilatticeHomomorphism of S,T; ::_thesis: f is meet-preserving let x, y be Element of S; :: according to WAYBEL_0:def_34 ::_thesis: f preserves_inf_of {x,y} thus f preserves_inf_of {x,y} by Def1; ::_thesis: verum end; end; theorem :: WAYBEL21:1 for S, T being upper-bounded Semilattice for f being SemilatticeHomomorphism of S,T holds f . (Top S) = Top T proof let S, T be upper-bounded Semilattice; ::_thesis: for f being SemilatticeHomomorphism of S,T holds f . (Top S) = Top T let f be SemilatticeHomomorphism of S,T; ::_thesis: f . (Top S) = Top T A1: f preserves_inf_of {} S by Def1; ex_inf_of {} S,S by YELLOW_0:43; then f . (inf ({} S)) = inf (f .: ({} S)) by A1, WAYBEL_0:def_30; hence f . (Top S) = Top T ; ::_thesis: verum end; theorem Th2: :: WAYBEL21:2 for S, T being Semilattice for f being Function of S,T st f is meet-preserving holds for X being non empty finite Subset of S holds f preserves_inf_of X proof let S, T be Semilattice; ::_thesis: for f being Function of S,T st f is meet-preserving holds for X being non empty finite Subset of S holds f preserves_inf_of X let f be Function of S,T; ::_thesis: ( f is meet-preserving implies for X being non empty finite Subset of S holds f preserves_inf_of X ) assume A1: f is meet-preserving ; ::_thesis: for X being non empty finite Subset of S holds f preserves_inf_of X let X be non empty finite Subset of S; ::_thesis: f preserves_inf_of X assume ex_inf_of X,S ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of f .: X,T & "/\" ((f .: X),T) = f . ("/\" (X,S)) ) A2: X is finite ; defpred S1[ set ] means ( \$1 <> {} implies ( ex_inf_of \$1,S & ex_inf_of f .: \$1,T & inf (f .: \$1) = f . ("/\" (\$1,S)) ) ); A3: S1[ {} ] ; A4: now__::_thesis:_for_y,_x_being_set_st_y_in_X_&_x_c=_X_&_S1[x]_holds_ S1[x_\/_{y}] let y, x be set ; ::_thesis: ( y in X & x c= X & S1[x] implies S1[x \/ {y}] ) assume that A5: y in X and x c= X and A6: S1[x] ; ::_thesis: S1[x \/ {y}] thus S1[x \/ {y}] ::_thesis: verum proof assume x \/ {y} <> {} ; ::_thesis: ( ex_inf_of x \/ {y},S & ex_inf_of f .: (x \/ {y}),T & inf (f .: (x \/ {y})) = f . ("/\" ((x \/ {y}),S)) ) reconsider y9 = y as Element of S by A5; set fy = f . y9; A7: ex_inf_of {(f . y9)},T by YELLOW_0:38; A8: inf {(f . y9)} = f . y9 by YELLOW_0:39; A9: ex_inf_of {y9},S by YELLOW_0:38; A10: inf {y9} = y by YELLOW_0:39; thus ex_inf_of x \/ {y},S by A6, A9, YELLOW_2:4; ::_thesis: ( ex_inf_of f .: (x \/ {y}),T & inf (f .: (x \/ {y})) = f . ("/\" ((x \/ {y}),S)) ) dom f = the carrier of S by FUNCT_2:def_1; then A11: Im (f,y) = {(f . y9)} by FUNCT_1:59; then A12: f .: (x \/ {y}) = (f .: x) \/ {(f . y9)} by RELAT_1:120; hence ex_inf_of f .: (x \/ {y}),T by A6, A7, A11, YELLOW_2:4; ::_thesis: inf (f .: (x \/ {y})) = f . ("/\" ((x \/ {y}),S)) percases ( x = {} or x <> {} ) ; suppose x = {} ; ::_thesis: inf (f .: (x \/ {y})) = f . ("/\" ((x \/ {y}),S)) hence inf (f .: (x \/ {y})) = f . ("/\" ((x \/ {y}),S)) by A8, A11, YELLOW_0:39; ::_thesis: verum end; supposeA13: x <> {} ; ::_thesis: inf (f .: (x \/ {y})) = f . ("/\" ((x \/ {y}),S)) hence "/\" ((f .: (x \/ {y})),T) = (f . ("/\" (x,S))) "/\" (f . y9) by A6, A7, A8, A12, YELLOW_2:4 .= f . (("/\" (x,S)) "/\" y9) by A1, WAYBEL_6:1 .= f . ("/\" ((x \/ {y}),S)) by A6, A9, A10, A13, YELLOW_2:4 ; ::_thesis: verum end; end; end; end; S1[X] from FINSET_1:sch_2(A2, A3, A4); hence ( ex_inf_of f .: X,T & "/\" ((f .: X),T) = f . ("/\" (X,S)) ) ; ::_thesis: verum end; theorem :: WAYBEL21:3 for S, T being upper-bounded Semilattice for f being meet-preserving Function of S,T st f . (Top S) = Top T holds f is SemilatticeHomomorphism of S,T proof let S, T be upper-bounded Semilattice; ::_thesis: for f being meet-preserving Function of S,T st f . (Top S) = Top T holds f is SemilatticeHomomorphism of S,T let f be meet-preserving Function of S,T; ::_thesis: ( f . (Top S) = Top T implies f is SemilatticeHomomorphism of S,T ) assume A1: f . (Top S) = Top T ; ::_thesis: f is SemilatticeHomomorphism of S,T thus ( S is upper-bounded implies T is upper-bounded ) ; :: according to WAYBEL21:def_1 ::_thesis: for X being finite Subset of S holds f preserves_inf_of X let X be finite Subset of S; ::_thesis: f preserves_inf_of X A2: ex_inf_of f .: {},T by YELLOW_0:43; ( X = {} or f preserves_inf_of X ) by Th2; hence f preserves_inf_of X by A1, A2, WAYBEL_0:def_30; ::_thesis: verum end; theorem Th4: :: WAYBEL21:4 for S, T being Semilattice for f being Function of S,T st f is meet-preserving & ( for X being non empty filtered Subset of S holds f preserves_inf_of X ) holds for X being non empty Subset of S holds f preserves_inf_of X proof let S, T be Semilattice; ::_thesis: for f being Function of S,T st f is meet-preserving & ( for X being non empty filtered Subset of S holds f preserves_inf_of X ) holds for X being non empty Subset of S holds f preserves_inf_of X let f be Function of S,T; ::_thesis: ( f is meet-preserving & ( for X being non empty filtered Subset of S holds f preserves_inf_of X ) implies for X being non empty Subset of S holds f preserves_inf_of X ) assume that A1: f is meet-preserving and A2: for X being non empty filtered Subset of S holds f preserves_inf_of X ; ::_thesis: for X being non empty Subset of S holds f preserves_inf_of X let X be non empty Subset of S; ::_thesis: f preserves_inf_of X assume A3: ex_inf_of X,S ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of f .: X,T & "/\" ((f .: X),T) = f . ("/\" (X,S)) ) defpred S1[ set ] means ex Y being non empty finite Subset of X st ( ex_inf_of Y,S & \$1 = "/\" (Y,S) ); consider Z being set such that A4: for x being set holds ( x in Z iff ( x in the carrier of S & S1[x] ) ) from XBOOLE_0:sch_1(); set a = the Element of X; reconsider a9 = the Element of X as Element of S ; A5: ex_inf_of { the Element of X},S by YELLOW_0:38; A6: inf {a9} = the Element of X by YELLOW_0:39; Z c= the carrier of S proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Z or x in the carrier of S ) thus ( not x in Z or x in the carrier of S ) by A4; ::_thesis: verum end; then reconsider Z = Z as non empty Subset of S by A4, A5, A6; A7: now__::_thesis:_for_Y_being_finite_Subset_of_X_st_Y_<>_{}_holds_ ex_inf_of_Y,S let Y be finite Subset of X; ::_thesis: ( Y <> {} implies ex_inf_of Y,S ) Y is Subset of S by XBOOLE_1:1; hence ( Y <> {} implies ex_inf_of Y,S ) by YELLOW_0:55; ::_thesis: verum end; A8: now__::_thesis:_for_Y_being_finite_Subset_of_X_st_Y_<>_{}_holds_ "/\"_(Y,S)_in_Z let Y be finite Subset of X; ::_thesis: ( Y <> {} implies "/\" (Y,S) in Z ) reconsider Y9 = Y as Subset of S by XBOOLE_1:1; assume A9: Y <> {} ; ::_thesis: "/\" (Y,S) in Z then ex_inf_of Y9,S by YELLOW_0:55; hence "/\" (Y,S) in Z by A4, A9; ::_thesis: verum end; A10: now__::_thesis:_for_x_being_Element_of_S_st_x_in_Z_holds_ ex_Y_being_finite_Subset_of_X_st_ (_ex_inf_of_Y,S_&_x_=_"/\"_(Y,S)_) let x be Element of S; ::_thesis: ( x in Z implies ex Y being finite Subset of X st ( ex_inf_of Y,S & x = "/\" (Y,S) ) ) assume x in Z ; ::_thesis: ex Y being finite Subset of X st ( ex_inf_of Y,S & x = "/\" (Y,S) ) then ex Y being non empty finite Subset of X st ( ex_inf_of Y,S & x = "/\" (Y,S) ) by A4; hence ex Y being finite Subset of X st ( ex_inf_of Y,S & x = "/\" (Y,S) ) ; ::_thesis: verum end; then A11: Z is filtered by A7, A8, WAYBEL_0:56; A12: ex_inf_of Z,S by A3, A7, A8, A10, WAYBEL_0:58; A13: f preserves_inf_of Z by A2, A11; then A14: ex_inf_of f .: Z,T by A12, WAYBEL_0:def_30; A15: inf (f .: Z) = f . (inf Z) by A12, A13, WAYBEL_0:def_30; A16: inf Z = inf X by A3, A7, A8, A10, WAYBEL_0:59; X c= Z proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Z ) assume A17: x in X ; ::_thesis: x in Z then reconsider Y = {x} as finite Subset of X by ZFMISC_1:31; reconsider x = x as Element of S by A17; Y is Subset of S by XBOOLE_1:1; then A18: ex_inf_of Y,S by YELLOW_0:55; x = "/\" (Y,S) by YELLOW_0:39; hence x in Z by A4, A18; ::_thesis: verum end; then A19: f .: X c= f .: Z by RELAT_1:123; A20: f .: Z is_>=_than f . (inf X) by A14, A15, A16, YELLOW_0:31; A21: f .: X is_>=_than f . (inf X) proof let x be Element of T; :: according to LATTICE3:def_8 ::_thesis: ( not x in f .: X or f . (inf X) <= x ) assume x in f .: X ; ::_thesis: f . (inf X) <= x hence f . (inf X) <= x by A19, A20, LATTICE3:def_8; ::_thesis: verum end; A22: now__::_thesis:_for_b_being_Element_of_T_st_f_.:_X_is_>=_than_b_holds_ f_._(inf_X)_>=_b let b be Element of T; ::_thesis: ( f .: X is_>=_than b implies f . (inf X) >= b ) assume A23: f .: X is_>=_than b ; ::_thesis: f . (inf X) >= b f .: Z is_>=_than b proof let a be Element of T; :: according to LATTICE3:def_8 ::_thesis: ( not a in f .: Z or b <= a ) assume a in f .: Z ; ::_thesis: b <= a then consider x being set such that x in dom f and A24: x in Z and A25: a = f . x by FUNCT_1:def_6; consider Y being non empty finite Subset of X such that A26: ex_inf_of Y,S and A27: x = "/\" (Y,S) by A4, A24; reconsider Y = Y as Subset of S by XBOOLE_1:1; A28: f .: Y c= f .: X by RELAT_1:123; A29: f preserves_inf_of Y by A1, Th2; A30: b is_<=_than f .: Y by A23, A28, YELLOW_0:9; A31: a = "/\" ((f .: Y),T) by A25, A26, A27, A29, WAYBEL_0:def_30; ex_inf_of f .: Y,T by A26, A29, WAYBEL_0:def_30; hence b <= a by A30, A31, YELLOW_0:def_10; ::_thesis: verum end; hence f . (inf X) >= b by A14, A15, A16, YELLOW_0:31; ::_thesis: verum end; hence ex_inf_of f .: X,T by A21, YELLOW_0:16; ::_thesis: "/\" ((f .: X),T) = f . ("/\" (X,S)) hence inf (f .: X) = f . (inf X) by A21, A22, YELLOW_0:def_10; ::_thesis: verum end; theorem Th5: :: WAYBEL21:5 for S, T being Semilattice for f being Function of S,T st f is infs-preserving holds f is SemilatticeHomomorphism of S,T proof let S, T be Semilattice; ::_thesis: for f being Function of S,T st f is infs-preserving holds f is SemilatticeHomomorphism of S,T let f be Function of S,T; ::_thesis: ( f is infs-preserving implies f is SemilatticeHomomorphism of S,T ) assume A1: f is infs-preserving ; ::_thesis: f is SemilatticeHomomorphism of S,T reconsider e = {} as Subset of S by XBOOLE_1:2; hereby :: according to WAYBEL21:def_1 ::_thesis: for X being finite Subset of S holds f preserves_inf_of X assume S is upper-bounded ; ::_thesis: T is upper-bounded then A2: ex_inf_of e,S by YELLOW_0:43; f preserves_inf_of e by A1, WAYBEL_0:def_32; then A3: ex_inf_of f .: e,T by A2, WAYBEL_0:def_30; f .: e = {} ; hence T is upper-bounded by A3, WAYBEL20:5; ::_thesis: verum end; let X be finite Subset of S; ::_thesis: f preserves_inf_of X thus f preserves_inf_of X by A1, WAYBEL_0:def_32; ::_thesis: verum end; theorem Th6: :: WAYBEL21:6 for S1, T1, S2, T2 being non empty RelStr st RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) holds for f1 being Function of S1,T1 for f2 being Function of S2,T2 st f1 = f2 holds ( ( f1 is infs-preserving implies f2 is infs-preserving ) & ( f1 is directed-sups-preserving implies f2 is directed-sups-preserving ) ) proof let S1, T1, S2, T2 be non empty RelStr ; ::_thesis: ( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) implies for f1 being Function of S1,T1 for f2 being Function of S2,T2 st f1 = f2 holds ( ( f1 is infs-preserving implies f2 is infs-preserving ) & ( f1 is directed-sups-preserving implies f2 is directed-sups-preserving ) ) ) assume that A1: RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) and A2: RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) ; ::_thesis: for f1 being Function of S1,T1 for f2 being Function of S2,T2 st f1 = f2 holds ( ( f1 is infs-preserving implies f2 is infs-preserving ) & ( f1 is directed-sups-preserving implies f2 is directed-sups-preserving ) ) let f1 be Function of S1,T1; ::_thesis: for f2 being Function of S2,T2 st f1 = f2 holds ( ( f1 is infs-preserving implies f2 is infs-preserving ) & ( f1 is directed-sups-preserving implies f2 is directed-sups-preserving ) ) let f2 be Function of S2,T2; ::_thesis: ( f1 = f2 implies ( ( f1 is infs-preserving implies f2 is infs-preserving ) & ( f1 is directed-sups-preserving implies f2 is directed-sups-preserving ) ) ) assume A3: f1 = f2 ; ::_thesis: ( ( f1 is infs-preserving implies f2 is infs-preserving ) & ( f1 is directed-sups-preserving implies f2 is directed-sups-preserving ) ) thus ( f1 is infs-preserving implies f2 is infs-preserving ) ::_thesis: ( f1 is directed-sups-preserving implies f2 is directed-sups-preserving ) proof assume A4: for X being Subset of S1 holds f1 preserves_inf_of X ; :: according to WAYBEL_0:def_32 ::_thesis: f2 is infs-preserving let X be Subset of S2; :: according to WAYBEL_0:def_32 ::_thesis: f2 preserves_inf_of X thus f2 preserves_inf_of X by A1, A2, A3, A4, WAYBEL_0:65; ::_thesis: verum end; assume A5: for X being Subset of S1 st not X is empty & X is directed holds f1 preserves_sup_of X ; :: according to WAYBEL_0:def_37 ::_thesis: f2 is directed-sups-preserving let X be Subset of S2; :: according to WAYBEL_0:def_37 ::_thesis: ( X is empty or not X is directed or f2 preserves_sup_of X ) reconsider Y = X as Subset of S1 by A1; assume ( not X is empty & X is directed ) ; ::_thesis: f2 preserves_sup_of X then f1 preserves_sup_of Y by A1, A5, WAYBEL_0:3; hence f2 preserves_sup_of X by A1, A2, A3, WAYBEL_0:65; ::_thesis: verum end; theorem :: WAYBEL21:7 for S1, T1, S2, T2 being non empty RelStr st RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) holds for f1 being Function of S1,T1 for f2 being Function of S2,T2 st f1 = f2 holds ( ( f1 is sups-preserving implies f2 is sups-preserving ) & ( f1 is filtered-infs-preserving implies f2 is filtered-infs-preserving ) ) proof let S1, T1, S2, T2 be non empty RelStr ; ::_thesis: ( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) implies for f1 being Function of S1,T1 for f2 being Function of S2,T2 st f1 = f2 holds ( ( f1 is sups-preserving implies f2 is sups-preserving ) & ( f1 is filtered-infs-preserving implies f2 is filtered-infs-preserving ) ) ) assume that A1: RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) and A2: RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) ; ::_thesis: for f1 being Function of S1,T1 for f2 being Function of S2,T2 st f1 = f2 holds ( ( f1 is sups-preserving implies f2 is sups-preserving ) & ( f1 is filtered-infs-preserving implies f2 is filtered-infs-preserving ) ) let f1 be Function of S1,T1; ::_thesis: for f2 being Function of S2,T2 st f1 = f2 holds ( ( f1 is sups-preserving implies f2 is sups-preserving ) & ( f1 is filtered-infs-preserving implies f2 is filtered-infs-preserving ) ) let f2 be Function of S2,T2; ::_thesis: ( f1 = f2 implies ( ( f1 is sups-preserving implies f2 is sups-preserving ) & ( f1 is filtered-infs-preserving implies f2 is filtered-infs-preserving ) ) ) assume A3: f1 = f2 ; ::_thesis: ( ( f1 is sups-preserving implies f2 is sups-preserving ) & ( f1 is filtered-infs-preserving implies f2 is filtered-infs-preserving ) ) thus ( f1 is sups-preserving implies f2 is sups-preserving ) ::_thesis: ( f1 is filtered-infs-preserving implies f2 is filtered-infs-preserving ) proof assume A4: for X being Subset of S1 holds f1 preserves_sup_of X ; :: according to WAYBEL_0:def_33 ::_thesis: f2 is sups-preserving let X be Subset of S2; :: according to WAYBEL_0:def_33 ::_thesis: f2 preserves_sup_of X thus f2 preserves_sup_of X by A1, A2, A3, A4, WAYBEL_0:65; ::_thesis: verum end; assume A5: for X being Subset of S1 st not X is empty & X is filtered holds f1 preserves_inf_of X ; :: according to WAYBEL_0:def_36 ::_thesis: f2 is filtered-infs-preserving let X be Subset of S2; :: according to WAYBEL_0:def_36 ::_thesis: ( X is empty or not X is filtered or f2 preserves_inf_of X ) reconsider Y = X as Subset of S1 by A1; assume ( not X is empty & X is filtered ) ; ::_thesis: f2 preserves_inf_of X then f1 preserves_inf_of Y by A1, A5, WAYBEL_0:4; hence f2 preserves_inf_of X by A1, A2, A3, WAYBEL_0:65; ::_thesis: verum end; theorem Th8: :: WAYBEL21:8 for T being complete LATTICE for S being non empty full infs-inheriting SubRelStr of T holds incl (S,T) is infs-preserving proof let T be complete LATTICE; ::_thesis: for S being non empty full infs-inheriting SubRelStr of T holds incl (S,T) is infs-preserving let S be non empty full infs-inheriting SubRelStr of T; ::_thesis: incl (S,T) is infs-preserving set f = incl (S,T); let X be Subset of S; :: according to WAYBEL_0:def_32 ::_thesis: incl (S,T) preserves_inf_of X assume ex_inf_of X,S ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of (incl (S,T)) .: X,T & "/\" (((incl (S,T)) .: X),T) = (incl (S,T)) . ("/\" (X,S)) ) thus ex_inf_of (incl (S,T)) .: X,T by YELLOW_0:17; ::_thesis: "/\" (((incl (S,T)) .: X),T) = (incl (S,T)) . ("/\" (X,S)) the carrier of S c= the carrier of T by YELLOW_0:def_13; then A1: incl (S,T) = id the carrier of S by YELLOW_9:def_1; then A2: (incl (S,T)) .: X = X by FUNCT_1:92; A3: ex_inf_of X,T by YELLOW_0:17; A4: (incl (S,T)) . (inf X) = inf X by A1, FUNCT_1:18; "/\" (X,T) in the carrier of S by A3, YELLOW_0:def_18; hence "/\" (((incl (S,T)) .: X),T) = (incl (S,T)) . ("/\" (X,S)) by A2, A3, A4, YELLOW_0:63; ::_thesis: verum end; theorem :: WAYBEL21:9 for T being complete LATTICE for S being non empty full sups-inheriting SubRelStr of T holds incl (S,T) is sups-preserving proof let T be complete LATTICE; ::_thesis: for S being non empty full sups-inheriting SubRelStr of T holds incl (S,T) is sups-preserving let S be non empty full sups-inheriting SubRelStr of T; ::_thesis: incl (S,T) is sups-preserving set f = incl (S,T); let X be Subset of S; :: according to WAYBEL_0:def_33 ::_thesis: incl (S,T) preserves_sup_of X assume ex_sup_of X,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (incl (S,T)) .: X,T & "\/" (((incl (S,T)) .: X),T) = (incl (S,T)) . ("\/" (X,S)) ) thus ex_sup_of (incl (S,T)) .: X,T by YELLOW_0:17; ::_thesis: "\/" (((incl (S,T)) .: X),T) = (incl (S,T)) . ("\/" (X,S)) the carrier of S c= the carrier of T by YELLOW_0:def_13; then A1: incl (S,T) = id the carrier of S by YELLOW_9:def_1; then A2: (incl (S,T)) .: X = X by FUNCT_1:92; A3: ex_sup_of X,T by YELLOW_0:17; A4: (incl (S,T)) . (sup X) = sup X by A1, FUNCT_1:18; "\/" (X,T) in the carrier of S by A3, YELLOW_0:def_19; hence "\/" (((incl (S,T)) .: X),T) = (incl (S,T)) . ("\/" (X,S)) by A2, A3, A4, YELLOW_0:64; ::_thesis: verum end; theorem Th10: :: WAYBEL21:10 for T being non empty up-complete Poset for S being non empty full directed-sups-inheriting SubRelStr of T holds incl (S,T) is directed-sups-preserving proof let T be non empty up-complete Poset; ::_thesis: for S being non empty full directed-sups-inheriting SubRelStr of T holds incl (S,T) is directed-sups-preserving let S be non empty full directed-sups-inheriting SubRelStr of T; ::_thesis: incl (S,T) is directed-sups-preserving set f = incl (S,T); let X be Subset of S; :: according to WAYBEL_0:def_37 ::_thesis: ( X is empty or not X is directed or incl (S,T) preserves_sup_of X ) assume that A1: ( not X is empty & X is directed ) and ex_sup_of X,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (incl (S,T)) .: X,T & "\/" (((incl (S,T)) .: X),T) = (incl (S,T)) . ("\/" (X,S)) ) reconsider X9 = X as non empty directed Subset of T by A1, YELLOW_2:7; the carrier of S c= the carrier of T by YELLOW_0:def_13; then A2: incl (S,T) = id the carrier of S by YELLOW_9:def_1; then A3: (incl (S,T)) .: X = X9 by FUNCT_1:92; A4: (incl (S,T)) . (sup X) = sup X by A2, FUNCT_1:18; thus ex_sup_of (incl (S,T)) .: X,T by A3, WAYBEL_0:75; ::_thesis: "\/" (((incl (S,T)) .: X),T) = (incl (S,T)) . ("\/" (X,S)) hence "\/" (((incl (S,T)) .: X),T) = (incl (S,T)) . ("\/" (X,S)) by A1, A3, A4, WAYBEL_0:7; ::_thesis: verum end; theorem :: WAYBEL21:11 for T being complete LATTICE for S being non empty full filtered-infs-inheriting SubRelStr of T holds incl (S,T) is filtered-infs-preserving proof let T be complete LATTICE; ::_thesis: for S being non empty full filtered-infs-inheriting SubRelStr of T holds incl (S,T) is filtered-infs-preserving let S be non empty full filtered-infs-inheriting SubRelStr of T; ::_thesis: incl (S,T) is filtered-infs-preserving set f = incl (S,T); let X be Subset of S; :: according to WAYBEL_0:def_36 ::_thesis: ( X is empty or not X is filtered or incl (S,T) preserves_inf_of X ) assume that A1: ( not X is empty & X is filtered ) and ex_inf_of X,S ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of (incl (S,T)) .: X,T & "/\" (((incl (S,T)) .: X),T) = (incl (S,T)) . ("/\" (X,S)) ) thus ex_inf_of (incl (S,T)) .: X,T by YELLOW_0:17; ::_thesis: "/\" (((incl (S,T)) .: X),T) = (incl (S,T)) . ("/\" (X,S)) the carrier of S c= the carrier of T by YELLOW_0:def_13; then A2: incl (S,T) = id the carrier of S by YELLOW_9:def_1; then A3: (incl (S,T)) .: X = X by FUNCT_1:92; A4: ex_inf_of X,T by YELLOW_0:17; (incl (S,T)) . (inf X) = inf X by A2, FUNCT_1:18; hence "/\" (((incl (S,T)) .: X),T) = (incl (S,T)) . ("/\" (X,S)) by A1, A3, A4, WAYBEL_0:6; ::_thesis: verum end; theorem Th12: :: WAYBEL21:12 for T1, T2, R being RelStr for S being SubRelStr of T1 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of R, the InternalRel of R #) holds ( R is SubRelStr of T2 & ( S is full implies R is full SubRelStr of T2 ) ) proof let T, T2, R be RelStr ; ::_thesis: for S being SubRelStr of T st RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of R, the InternalRel of R #) holds ( R is SubRelStr of T2 & ( S is full implies R is full SubRelStr of T2 ) ) let S be SubRelStr of T; ::_thesis: ( RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of R, the InternalRel of R #) implies ( R is SubRelStr of T2 & ( S is full implies R is full SubRelStr of T2 ) ) ) assume that A1: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of T2, the InternalRel of T2 #) and A2: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of R, the InternalRel of R #) ; ::_thesis: ( R is SubRelStr of T2 & ( S is full implies R is full SubRelStr of T2 ) ) A3: the carrier of R c= the carrier of T2 by A1, A2, YELLOW_0:def_13; A4: the InternalRel of R c= the InternalRel of T2 by A1, A2, YELLOW_0:def_13; hence R is SubRelStr of T2 by A3, YELLOW_0:def_13; ::_thesis: ( S is full implies R is full SubRelStr of T2 ) assume the InternalRel of S = the InternalRel of T |_2 the carrier of S ; :: according to YELLOW_0:def_14 ::_thesis: R is full SubRelStr of T2 hence R is full SubRelStr of T2 by A1, A2, A3, A4, YELLOW_0:def_13, YELLOW_0:def_14; ::_thesis: verum end; theorem Th13: :: WAYBEL21:13 for T being non empty RelStr holds T is full infs-inheriting sups-inheriting SubRelStr of T proof let T be non empty RelStr ; ::_thesis: T is full infs-inheriting sups-inheriting SubRelStr of T reconsider R = T as full SubRelStr of T by YELLOW_6:6; A1: R is infs-inheriting proof let X be Subset of R; :: according to YELLOW_0:def_18 ::_thesis: ( not ex_inf_of X,T or "/\" (X,T) in the carrier of R ) thus ( not ex_inf_of X,T or "/\" (X,T) in the carrier of R ) ; ::_thesis: verum end; R is sups-inheriting proof let X be Subset of R; :: according to YELLOW_0:def_19 ::_thesis: ( not ex_sup_of X,T or "\/" (X,T) in the carrier of R ) thus ( not ex_sup_of X,T or "\/" (X,T) in the carrier of R ) ; ::_thesis: verum end; hence T is full infs-inheriting sups-inheriting SubRelStr of T by A1; ::_thesis: verum end; registration let T be complete LATTICE; cluster non empty reflexive transitive antisymmetric full meet-inheriting infs-inheriting filtered-infs-inheriting directed-sups-inheriting with_infima complete for SubRelStr of T; existence ex b1 being CLSubFrame of T st b1 is complete proof T is full infs-inheriting sups-inheriting SubRelStr of T by Th13; hence ex b1 being CLSubFrame of T st b1 is complete ; ::_thesis: verum end; end; theorem Th14: :: WAYBEL21:14 for T being Semilattice for S being non empty full SubRelStr of T holds ( S is meet-inheriting iff for X being non empty finite Subset of S holds "/\" (X,T) in the carrier of S ) proof let T be Semilattice; ::_thesis: for S being non empty full SubRelStr of T holds ( S is meet-inheriting iff for X being non empty finite Subset of S holds "/\" (X,T) in the carrier of S ) let S be non empty full SubRelStr of T; ::_thesis: ( S is meet-inheriting iff for X being non empty finite Subset of S holds "/\" (X,T) in the carrier of S ) hereby ::_thesis: ( ( for X being non empty finite Subset of S holds "/\" (X,T) in the carrier of S ) implies S is meet-inheriting ) assume A1: S is meet-inheriting ; ::_thesis: for X being non empty finite Subset of S holds "/\" (X,T) in the carrier of S let X be non empty finite Subset of S; ::_thesis: "/\" (X,T) in the carrier of S A2: X is finite ; defpred S1[ set ] means ( \$1 <> {} implies "/\" (\$1,T) in the carrier of S ); A3: S1[ {} ] ; A4: now__::_thesis:_for_y,_x_being_set_st_y_in_X_&_x_c=_X_&_S1[x]_holds_ S1[x_\/_{y}] let y, x be set ; ::_thesis: ( y in X & x c= X & S1[x] implies S1[x \/ {y}] ) assume that A5: y in X and A6: x c= X and A7: S1[x] ; ::_thesis: S1[x \/ {y}] thus S1[x \/ {y}] ::_thesis: verum proof assume x \/ {y} <> {} ; ::_thesis: "/\" ((x \/ {y}),T) in the carrier of S reconsider y9 = y as Element of S by A5; reconsider z = y9 as Element of T by YELLOW_0:58; A8: x c= the carrier of S by A6, XBOOLE_1:1; the carrier of S c= the carrier of T by YELLOW_0:def_13; then reconsider x9 = x as finite Subset of T by A6, A8, XBOOLE_1:1; A9: ex_inf_of {z},T by YELLOW_0:38; A10: inf {z} = y9 by YELLOW_0:39; now__::_thesis:_(_x9_<>_{}_implies_inf_(x9_\/_{z})_in_the_carrier_of_S_) assume A11: x9 <> {} ; ::_thesis: inf (x9 \/ {z}) in the carrier of S then ex_inf_of x9,T by YELLOW_0:55; then A12: inf (x9 \/ {z}) = (inf x9) "/\" z by A9, A10, YELLOW_2:4; ex_inf_of {(inf x9),z},T by YELLOW_0:21; then inf {(inf x9),z} in the carrier of S by A1, A7, A11, YELLOW_0:def_16; hence inf (x9 \/ {z}) in the carrier of S by A12, YELLOW_0:40; ::_thesis: verum end; hence "/\" ((x \/ {y}),T) in the carrier of S by A10; ::_thesis: verum end; end; S1[X] from FINSET_1:sch_2(A2, A3, A4); hence "/\" (X,T) in the carrier of S ; ::_thesis: verum end; assume A13: for X being non empty finite Subset of S holds "/\" (X,T) in the carrier of S ; ::_thesis: S is meet-inheriting let x, y be Element of T; :: according to YELLOW_0:def_16 ::_thesis: ( not x in the carrier of S or not y in the carrier of S or not ex_inf_of {x,y},T or "/\" ({x,y},T) in the carrier of S ) assume that A14: x in the carrier of S and A15: y in the carrier of S ; ::_thesis: ( not ex_inf_of {x,y},T or "/\" ({x,y},T) in the carrier of S ) {x,y} c= the carrier of S by A14, A15, ZFMISC_1:32; hence ( not ex_inf_of {x,y},T or "/\" ({x,y},T) in the carrier of S ) by A13; ::_thesis: verum end; theorem Th15: :: WAYBEL21:15 for T being sup-Semilattice for S being non empty full SubRelStr of T holds ( S is join-inheriting iff for X being non empty finite Subset of S holds "\/" (X,T) in the carrier of S ) proof let T be sup-Semilattice; ::_thesis: for S being non empty full SubRelStr of T holds ( S is join-inheriting iff for X being non empty finite Subset of S holds "\/" (X,T) in the carrier of S ) let S be non empty full SubRelStr of T; ::_thesis: ( S is join-inheriting iff for X being non empty finite Subset of S holds "\/" (X,T) in the carrier of S ) hereby ::_thesis: ( ( for X being non empty finite Subset of S holds "\/" (X,T) in the carrier of S ) implies S is join-inheriting ) assume A1: S is join-inheriting ; ::_thesis: for X being non empty finite Subset of S holds "\/" (X,T) in the carrier of S let X be non empty finite Subset of S; ::_thesis: "\/" (X,T) in the carrier of S A2: X is finite ; defpred S1[ set ] means ( \$1 <> {} implies "\/" (\$1,T) in the carrier of S ); A3: S1[ {} ] ; A4: now__::_thesis:_for_y,_x_being_set_st_y_in_X_&_x_c=_X_&_S1[x]_holds_ S1[x_\/_{y}] let y, x be set ; ::_thesis: ( y in X & x c= X & S1[x] implies S1[x \/ {y}] ) assume that A5: y in X and A6: x c= X and A7: S1[x] ; ::_thesis: S1[x \/ {y}] reconsider y9 = y as Element of S by A5; reconsider z = y9 as Element of T by YELLOW_0:58; thus S1[x \/ {y}] ::_thesis: verum proof assume x \/ {y} <> {} ; ::_thesis: "\/" ((x \/ {y}),T) in the carrier of S A8: x c= the carrier of S by A6, XBOOLE_1:1; the carrier of S c= the carrier of T by YELLOW_0:def_13; then reconsider x9 = x as finite Subset of T by A6, A8, XBOOLE_1:1; A9: ex_sup_of {z},T by YELLOW_0:38; A10: sup {z} = y9 by YELLOW_0:39; now__::_thesis:_(_x9_<>_{}_implies_sup_(x9_\/_{z})_in_the_carrier_of_S_) assume A11: x9 <> {} ; ::_thesis: sup (x9 \/ {z}) in the carrier of S then ex_sup_of x9,T by YELLOW_0:54; then A12: sup (x9 \/ {z}) = (sup x9) "\/" z by A9, A10, YELLOW_2:3; ex_sup_of {(sup x9),z},T by YELLOW_0:20; then sup {(sup x9),z} in the carrier of S by A1, A7, A11, YELLOW_0:def_17; hence sup (x9 \/ {z}) in the carrier of S by A12, YELLOW_0:41; ::_thesis: verum end; hence "\/" ((x \/ {y}),T) in the carrier of S by A10; ::_thesis: verum end; end; S1[X] from FINSET_1:sch_2(A2, A3, A4); hence "\/" (X,T) in the carrier of S ; ::_thesis: verum end; assume A13: for X being non empty finite Subset of S holds "\/" (X,T) in the carrier of S ; ::_thesis: S is join-inheriting let x, y be Element of T; :: according to YELLOW_0:def_17 ::_thesis: ( not x in the carrier of S or not y in the carrier of S or not ex_sup_of {x,y},T or "\/" ({x,y},T) in the carrier of S ) assume that A14: x in the carrier of S and A15: y in the carrier of S ; ::_thesis: ( not ex_sup_of {x,y},T or "\/" ({x,y},T) in the carrier of S ) {x,y} c= the carrier of S by A14, A15, ZFMISC_1:32; hence ( not ex_sup_of {x,y},T or "\/" ({x,y},T) in the carrier of S ) by A13; ::_thesis: verum end; theorem Th16: :: WAYBEL21:16 for T being upper-bounded Semilattice for S being non empty full meet-inheriting SubRelStr of T st Top T in the carrier of S & S is filtered-infs-inheriting holds S is infs-inheriting proof let T be upper-bounded Semilattice; ::_thesis: for S being non empty full meet-inheriting SubRelStr of T st Top T in the carrier of S & S is filtered-infs-inheriting holds S is infs-inheriting let S be non empty full meet-inheriting SubRelStr of T; ::_thesis: ( Top T in the carrier of S & S is filtered-infs-inheriting implies S is infs-inheriting ) assume that A1: Top T in the carrier of S and A2: S is filtered-infs-inheriting ; ::_thesis: S is infs-inheriting let A be Subset of S; :: according to YELLOW_0:def_18 ::_thesis: ( not ex_inf_of A,T or "/\" (A,T) in the carrier of S ) the carrier of S c= the carrier of T by YELLOW_0:def_13; then reconsider C = A as Subset of T by XBOOLE_1:1; set F = fininfs C; assume A3: ex_inf_of A,T ; ::_thesis: "/\" (A,T) in the carrier of S then A4: inf (fininfs C) = inf C by WAYBEL_0:60; fininfs C c= the carrier of S proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in fininfs C or x in the carrier of S ) assume x in fininfs C ; ::_thesis: x in the carrier of S then consider Y being finite Subset of C such that A5: x = "/\" (Y,T) and ex_inf_of Y,T ; reconsider Y = Y as finite Subset of T by XBOOLE_1:1; reconsider Z = Y as finite Subset of S by XBOOLE_1:1; assume A6: not x in the carrier of S ; ::_thesis: contradiction then Z <> {} by A1, A5; hence contradiction by A5, A6, Th14; ::_thesis: verum end; then reconsider G = fininfs C as non empty Subset of S ; reconsider G = G as non empty filtered Subset of S by WAYBEL10:23; A7: now__::_thesis:_for_Y_being_finite_Subset_of_C_st_Y_<>_{}_holds_ ex_inf_of_Y,T let Y be finite Subset of C; ::_thesis: ( Y <> {} implies ex_inf_of Y,T ) Y c= the carrier of T by XBOOLE_1:1; hence ( Y <> {} implies ex_inf_of Y,T ) by YELLOW_0:55; ::_thesis: verum end; A8: now__::_thesis:_for_x_being_Element_of_T_st_x_in_fininfs_C_holds_ ex_Y_being_finite_Subset_of_C_st_ (_ex_inf_of_Y,T_&_x_=_"/\"_(Y,T)_) let x be Element of T; ::_thesis: ( x in fininfs C implies ex Y being finite Subset of C st ( ex_inf_of Y,T & x = "/\" (Y,T) ) ) assume x in fininfs C ; ::_thesis: ex Y being finite Subset of C st ( ex_inf_of Y,T & x = "/\" (Y,T) ) then ex Y being finite Subset of C st ( x = "/\" (Y,T) & ex_inf_of Y,T ) ; hence ex Y being finite Subset of C st ( ex_inf_of Y,T & x = "/\" (Y,T) ) ; ::_thesis: verum end; now__::_thesis:_for_Y_being_finite_Subset_of_C_st_Y_<>_{}_holds_ "/\"_(Y,T)_in_fininfs_C let Y be finite Subset of C; ::_thesis: ( Y <> {} implies "/\" (Y,T) in fininfs C ) reconsider Z = Y as finite Subset of T by XBOOLE_1:1; assume Y <> {} ; ::_thesis: "/\" (Y,T) in fininfs C then ex_inf_of Z,T by YELLOW_0:55; hence "/\" (Y,T) in fininfs C ; ::_thesis: verum end; then ex_inf_of G,T by A3, A7, A8, WAYBEL_0:58; hence "/\" (A,T) in the carrier of S by A2, A4, WAYBEL_0:def_3; ::_thesis: verum end; theorem :: WAYBEL21:17 for T being lower-bounded sup-Semilattice for S being non empty full join-inheriting SubRelStr of T st Bottom T in the carrier of S & S is directed-sups-inheriting holds S is sups-inheriting proof let T be lower-bounded sup-Semilattice; ::_thesis: for S being non empty full join-inheriting SubRelStr of T st Bottom T in the carrier of S & S is directed-sups-inheriting holds S is sups-inheriting let S be non empty full join-inheriting SubRelStr of T; ::_thesis: ( Bottom T in the carrier of S & S is directed-sups-inheriting implies S is sups-inheriting ) assume that A1: Bottom T in the carrier of S and A2: S is directed-sups-inheriting ; ::_thesis: S is sups-inheriting let A be Subset of S; :: according to YELLOW_0:def_19 ::_thesis: ( not ex_sup_of A,T or "\/" (A,T) in the carrier of S ) the carrier of S c= the carrier of T by YELLOW_0:def_13; then reconsider C = A as Subset of T by XBOOLE_1:1; set F = finsups C; assume A3: ex_sup_of A,T ; ::_thesis: "\/" (A,T) in the carrier of S then A4: sup (finsups C) = sup C by WAYBEL_0:55; finsups C c= the carrier of S proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in finsups C or x in the carrier of S ) assume x in finsups C ; ::_thesis: x in the carrier of S then consider Y being finite Subset of C such that A5: x = "\/" (Y,T) and ex_sup_of Y,T ; reconsider Y = Y as finite Subset of T by XBOOLE_1:1; reconsider Z = Y as finite Subset of S by XBOOLE_1:1; assume A6: not x in the carrier of S ; ::_thesis: contradiction then Z <> {} by A1, A5; hence contradiction by A5, A6, Th15; ::_thesis: verum end; then reconsider G = finsups C as non empty Subset of S ; reconsider G = G as non empty directed Subset of S by WAYBEL10:23; A7: now__::_thesis:_for_Y_being_finite_Subset_of_C_st_Y_<>_{}_holds_ ex_sup_of_Y,T let Y be finite Subset of C; ::_thesis: ( Y <> {} implies ex_sup_of Y,T ) Y c= the carrier of T by XBOOLE_1:1; hence ( Y <> {} implies ex_sup_of Y,T ) by YELLOW_0:54; ::_thesis: verum end; A8: now__::_thesis:_for_x_being_Element_of_T_st_x_in_finsups_C_holds_ ex_Y_being_finite_Subset_of_C_st_ (_ex_sup_of_Y,T_&_x_=_"\/"_(Y,T)_) let x be Element of T; ::_thesis: ( x in finsups C implies ex Y being finite Subset of C st ( ex_sup_of Y,T & x = "\/" (Y,T) ) ) assume x in finsups C ; ::_thesis: ex Y being finite Subset of C st ( ex_sup_of Y,T & x = "\/" (Y,T) ) then ex Y being finite Subset of C st ( x = "\/" (Y,T) & ex_sup_of Y,T ) ; hence ex Y being finite Subset of C st ( ex_sup_of Y,T & x = "\/" (Y,T) ) ; ::_thesis: verum end; now__::_thesis:_for_Y_being_finite_Subset_of_C_st_Y_<>_{}_holds_ "\/"_(Y,T)_in_finsups_C let Y be finite Subset of C; ::_thesis: ( Y <> {} implies "\/" (Y,T) in finsups C ) reconsider Z = Y as finite Subset of T by XBOOLE_1:1; assume Y <> {} ; ::_thesis: "\/" (Y,T) in finsups C then ex_sup_of Z,T by YELLOW_0:54; hence "\/" (Y,T) in finsups C ; ::_thesis: verum end; then ex_sup_of G,T by A3, A7, A8, WAYBEL_0:53; hence "\/" (A,T) in the carrier of S by A2, A4, WAYBEL_0:def_4; ::_thesis: verum end; theorem Th18: :: WAYBEL21:18 for T being complete LATTICE for S being non empty full SubRelStr of T st S is infs-inheriting holds S is complete proof let T be complete LATTICE; ::_thesis: for S being non empty full SubRelStr of T st S is infs-inheriting holds S is complete let S be non empty full SubRelStr of T; ::_thesis: ( S is infs-inheriting implies S is complete ) assume A1: S is infs-inheriting ; ::_thesis: S is complete now__::_thesis:_for_X_being_set_holds_ex_inf_of_X,S let X be set ; ::_thesis: ex_inf_of X,S set Y = X /\ the carrier of S; reconsider Y = X /\ the carrier of S as Subset of S by XBOOLE_1:17; A2: ex_inf_of Y,T by YELLOW_0:17; then "/\" (Y,T) in the carrier of S by A1, YELLOW_0:def_18; then ex_inf_of Y,S by A2, YELLOW_0:63; hence ex_inf_of X,S by YELLOW_0:50; ::_thesis: verum end; hence S is complete by YELLOW_2:25; ::_thesis: verum end; theorem :: WAYBEL21:19 for T being complete LATTICE for S being non empty full SubRelStr of T st S is sups-inheriting holds S is complete proof let T be complete LATTICE; ::_thesis: for S being non empty full SubRelStr of T st S is sups-inheriting holds S is complete let S be non empty full SubRelStr of T; ::_thesis: ( S is sups-inheriting implies S is complete ) assume A1: S is sups-inheriting ; ::_thesis: S is complete now__::_thesis:_for_X_being_set_holds_ex_sup_of_X,S let X be set ; ::_thesis: ex_sup_of X,S set Y = X /\ the carrier of S; reconsider Y = X /\ the carrier of S as Subset of S by XBOOLE_1:17; A2: ex_sup_of Y,T by YELLOW_0:17; then "\/" (Y,T) in the carrier of S by A1, YELLOW_0:def_19; then ex_sup_of Y,S by A2, YELLOW_0:64; hence ex_sup_of X,S by YELLOW_0:50; ::_thesis: verum end; hence S is complete by YELLOW_2:24; ::_thesis: verum end; theorem :: WAYBEL21:20 for T1, T2 being non empty RelStr for S1 being non empty full SubRelStr of T1 for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is infs-inheriting holds S2 is infs-inheriting proof let T1, T2 be non empty RelStr ; ::_thesis: for S1 being non empty full SubRelStr of T1 for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is infs-inheriting holds S2 is infs-inheriting let S1 be non empty full SubRelStr of T1; ::_thesis: for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is infs-inheriting holds S2 is infs-inheriting let S2 be non empty full SubRelStr of T2; ::_thesis: ( RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is infs-inheriting implies S2 is infs-inheriting ) assume A1: RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) ; ::_thesis: ( not the carrier of S1 = the carrier of S2 or not S1 is infs-inheriting or S2 is infs-inheriting ) assume A2: the carrier of S1 = the carrier of S2 ; ::_thesis: ( not S1 is infs-inheriting or S2 is infs-inheriting ) assume A3: for X being Subset of S1 st ex_inf_of X,T1 holds "/\" (X,T1) in the carrier of S1 ; :: according to YELLOW_0:def_18 ::_thesis: S2 is infs-inheriting let X be Subset of S2; :: according to YELLOW_0:def_18 ::_thesis: ( not ex_inf_of X,T2 or "/\" (X,T2) in the carrier of S2 ) reconsider Y = X as Subset of S1 by A2; assume A4: ex_inf_of X,T2 ; ::_thesis: "/\" (X,T2) in the carrier of S2 then "/\" (Y,T1) in the carrier of S1 by A1, A3, YELLOW_0:14; hence "/\" (X,T2) in the carrier of S2 by A1, A2, A4, YELLOW_0:27; ::_thesis: verum end; theorem :: WAYBEL21:21 for T1, T2 being non empty RelStr for S1 being non empty full SubRelStr of T1 for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is sups-inheriting holds S2 is sups-inheriting proof let T1, T2 be non empty RelStr ; ::_thesis: for S1 being non empty full SubRelStr of T1 for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is sups-inheriting holds S2 is sups-inheriting let S1 be non empty full SubRelStr of T1; ::_thesis: for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is sups-inheriting holds S2 is sups-inheriting let S2 be non empty full SubRelStr of T2; ::_thesis: ( RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is sups-inheriting implies S2 is sups-inheriting ) assume A1: RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) ; ::_thesis: ( not the carrier of S1 = the carrier of S2 or not S1 is sups-inheriting or S2 is sups-inheriting ) assume A2: the carrier of S1 = the carrier of S2 ; ::_thesis: ( not S1 is sups-inheriting or S2 is sups-inheriting ) assume A3: for X being Subset of S1 st ex_sup_of X,T1 holds "\/" (X,T1) in the carrier of S1 ; :: according to YELLOW_0:def_19 ::_thesis: S2 is sups-inheriting let X be Subset of S2; :: according to YELLOW_0:def_19 ::_thesis: ( not ex_sup_of X,T2 or "\/" (X,T2) in the carrier of S2 ) reconsider Y = X as Subset of S1 by A2; assume A4: ex_sup_of X,T2 ; ::_thesis: "\/" (X,T2) in the carrier of S2 then "\/" (Y,T1) in the carrier of S1 by A1, A3, YELLOW_0:14; hence "\/" (X,T2) in the carrier of S2 by A1, A2, A4, YELLOW_0:26; ::_thesis: verum end; theorem :: WAYBEL21:22 for T1, T2 being non empty RelStr for S1 being non empty full SubRelStr of T1 for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is directed-sups-inheriting holds S2 is directed-sups-inheriting proof let T1, T2 be non empty RelStr ; ::_thesis: for S1 being non empty full SubRelStr of T1 for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is directed-sups-inheriting holds S2 is directed-sups-inheriting let S1 be non empty full SubRelStr of T1; ::_thesis: for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is directed-sups-inheriting holds S2 is directed-sups-inheriting let S2 be non empty full SubRelStr of T2; ::_thesis: ( RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is directed-sups-inheriting implies S2 is directed-sups-inheriting ) assume A1: RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) ; ::_thesis: ( not the carrier of S1 = the carrier of S2 or not S1 is directed-sups-inheriting or S2 is directed-sups-inheriting ) RelStr(# the carrier of S2, the InternalRel of S2 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) ; then reconsider R = S2 as full SubRelStr of T1 by A1, Th12; assume A2: the carrier of S1 = the carrier of S2 ; ::_thesis: ( not S1 is directed-sups-inheriting or S2 is directed-sups-inheriting ) then A3: RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_0:57; assume A4: for X being directed Subset of S1 st X <> {} & ex_sup_of X,T1 holds "\/" (X,T1) in the carrier of S1 ; :: according to WAYBEL_0:def_4 ::_thesis: S2 is directed-sups-inheriting let X be directed Subset of S2; :: according to WAYBEL_0:def_4 ::_thesis: ( X = {} or not ex_sup_of X,T2 or "\/" (X,T2) in the carrier of S2 ) assume A5: X <> {} ; ::_thesis: ( not ex_sup_of X,T2 or "\/" (X,T2) in the carrier of S2 ) reconsider Y = X as directed Subset of S1 by A3, WAYBEL_0:3; assume A6: ex_sup_of X,T2 ; ::_thesis: "\/" (X,T2) in the carrier of S2 then "\/" (Y,T1) in the carrier of S1 by A1, A4, A5, YELLOW_0:14; hence "\/" (X,T2) in the carrier of S2 by A1, A2, A6, YELLOW_0:26; ::_thesis: verum end; theorem :: WAYBEL21:23 for T1, T2 being non empty RelStr for S1 being non empty full SubRelStr of T1 for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is filtered-infs-inheriting holds S2 is filtered-infs-inheriting proof let T1, T2 be non empty RelStr ; ::_thesis: for S1 being non empty full SubRelStr of T1 for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is filtered-infs-inheriting holds S2 is filtered-infs-inheriting let S1 be non empty full SubRelStr of T1; ::_thesis: for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is filtered-infs-inheriting holds S2 is filtered-infs-inheriting let S2 be non empty full SubRelStr of T2; ::_thesis: ( RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is filtered-infs-inheriting implies S2 is filtered-infs-inheriting ) assume A1: RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) ; ::_thesis: ( not the carrier of S1 = the carrier of S2 or not S1 is filtered-infs-inheriting or S2 is filtered-infs-inheriting ) RelStr(# the carrier of S2, the InternalRel of S2 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) ; then reconsider R = S2 as full SubRelStr of T1 by A1, Th12; assume A2: the carrier of S1 = the carrier of S2 ; ::_thesis: ( not S1 is filtered-infs-inheriting or S2 is filtered-infs-inheriting ) then A3: RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_0:57; assume A4: for X being filtered Subset of S1 st X <> {} & ex_inf_of X,T1 holds "/\" (X,T1) in the carrier of S1 ; :: according to WAYBEL_0:def_3 ::_thesis: S2 is filtered-infs-inheriting let X be filtered Subset of S2; :: according to WAYBEL_0:def_3 ::_thesis: ( X = {} or not ex_inf_of X,T2 or "/\" (X,T2) in the carrier of S2 ) assume A5: X <> {} ; ::_thesis: ( not ex_inf_of X,T2 or "/\" (X,T2) in the carrier of S2 ) reconsider Y = X as filtered Subset of S1 by A3, WAYBEL_0:4; assume A6: ex_inf_of X,T2 ; ::_thesis: "/\" (X,T2) in the carrier of S2 then "/\" (Y,T1) in the carrier of S1 by A1, A4, A5, YELLOW_0:14; hence "/\" (X,T2) in the carrier of S2 by A1, A2, A6, YELLOW_0:27; ::_thesis: verum end; begin theorem Th24: :: WAYBEL21:24 for S, T being non empty TopSpace for N being net of S for f being Function of S,T st f is continuous holds f .: (Lim N) c= Lim (f * N) proof let S, T be non empty TopSpace; ::_thesis: for N being net of S for f being Function of S,T st f is continuous holds f .: (Lim N) c= Lim (f * N) let N be net of S; ::_thesis: for f being Function of S,T st f is continuous holds f .: (Lim N) c= Lim (f * N) A1: [#] T <> {} ; let f be Function of S,T; ::_thesis: ( f is continuous implies f .: (Lim N) c= Lim (f * N) ) assume A2: f is continuous ; ::_thesis: f .: (Lim N) c= Lim (f * N) let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in f .: (Lim N) or p in Lim (f * N) ) assume A3: p in f .: (Lim N) ; ::_thesis: p in Lim (f * N) then reconsider p = p as Point of T ; consider x being set such that A4: x in the carrier of S and A5: x in Lim N and A6: p = f . x by A3, FUNCT_2:64; reconsider x = x as Element of S by A4; now__::_thesis:_for_V_being_a_neighborhood_of_p_holds_f_*_N_is_eventually_in_V let V be a_neighborhood of p; ::_thesis: f * N is_eventually_in V A7: p in Int V by CONNSP_2:def_1; A8: x in f " (Int V) by A6, A7, FUNCT_2:38; f " (Int V) is open by A1, A2, TOPS_2:43; then f " (Int V) is a_neighborhood of x by A8, CONNSP_2:3; then N is_eventually_in f " (Int V) by A5, YELLOW_6:def_15; then consider i being Element of N such that A9: for j being Element of N st j >= i holds N . j in f " (Int V) by WAYBEL_0:def_11; A10: the mapping of (f * N) = f * the mapping of N by WAYBEL_9:def_8; A11: RelStr(# the carrier of (f * N), the InternalRel of (f * N) #) = RelStr(# the carrier of N, the InternalRel of N #) by WAYBEL_9:def_8; then reconsider i9 = i as Element of (f * N) ; thus f * N is_eventually_in V ::_thesis: verum proof take i9 ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of (f * N) holds ( not i9 <= b1 or (f * N) . b1 in V ) let j9 be Element of (f * N); ::_thesis: ( not i9 <= j9 or (f * N) . j9 in V ) reconsider j = j9 as Element of N by A11; A12: f . (N . j) = (f * N) . j9 by A10, FUNCT_2:15; assume j9 >= i9 ; ::_thesis: (f * N) . j9 in V then N . j in f " (Int V) by A9, A11, YELLOW_0:1; then A13: f . (N . j) in Int V by FUNCT_2:38; Int V c= V by TOPS_1:16; hence (f * N) . j9 in V by A12, A13; ::_thesis: verum end; end; hence p in Lim (f * N) by YELLOW_6:def_15; ::_thesis: verum end; definition let T be non empty RelStr ; let N be non empty NetStr over T; redefine attr N is antitone means :Def2: :: WAYBEL21:def 2 for i, j being Element of N st i <= j holds N . i >= N . j; compatibility ( N is antitone iff for i, j being Element of N st i <= j holds N . i >= N . j ) proof hereby ::_thesis: ( ( for i, j being Element of N st i <= j holds N . i >= N . j ) implies N is antitone ) assume N is antitone ; ::_thesis: for i, j being Element of N st i <= j holds N . i >= N . j then A1: netmap (N,T) is antitone by WAYBEL_0:def_10; let i, j be Element of N; ::_thesis: ( i <= j implies N . i >= N . j ) assume i <= j ; ::_thesis: N . i >= N . j hence N . i >= N . j by A1, WAYBEL_0:def_5; ::_thesis: verum end; assume A2: for i, j being Element of N st i <= j holds N . i >= N . j ; ::_thesis: N is antitone let i, j be Element of N; :: according to WAYBEL_0:def_5,WAYBEL_0:def_10 ::_thesis: ( not i <= j or for b1, b2 being Element of the carrier of T holds ( not b1 = (netmap (N,T)) . i or not b2 = (netmap (N,T)) . j or b2 <= b1 ) ) A3: N . i = (netmap (N,T)) . i ; N . j = (netmap (N,T)) . j ; hence ( not i <= j or for b1, b2 being Element of the carrier of T holds ( not b1 = (netmap (N,T)) . i or not b2 = (netmap (N,T)) . j or b2 <= b1 ) ) by A2, A3; ::_thesis: verum end; end; :: deftheorem Def2 defines antitone WAYBEL21:def_2_:_ for T being non empty RelStr for N being non empty NetStr over T holds ( N is antitone iff for i, j being Element of N st i <= j holds N . i >= N . j ); registration let T be non empty reflexive RelStr ; let x be Element of T; cluster{x} opp+id -> transitive directed monotone antitone ; coherence ( {x} opp+id is transitive & {x} opp+id is directed & {x} opp+id is monotone & {x} opp+id is antitone ) proof set N = {x} opp+id ; A1: the carrier of ({x} opp+id) = {x} by YELLOW_9:7; thus {x} opp+id is transitive ::_thesis: ( {x} opp+id is directed & {x} opp+id is monotone & {x} opp+id is antitone ) proof let i, j, k be Element of ({x} opp+id); :: according to YELLOW_0:def_2 ::_thesis: ( not i <= j or not j <= k or i <= k ) i = x by A1, TARSKI:def_1; hence ( not i <= j or not j <= k or i <= k ) by A1, TARSKI:def_1; ::_thesis: verum end; thus {x} opp+id is directed ::_thesis: ( {x} opp+id is monotone & {x} opp+id is antitone ) proof let i, j be Element of ({x} opp+id); :: according to YELLOW_6:def_3 ::_thesis: ex b1 being Element of the carrier of ({x} opp+id) st ( i <= b1 & j <= b1 ) A2: i = x by A1, TARSKI:def_1; A3: i <= i ; j <= i by A1, A2, TARSKI:def_1; hence ex b1 being Element of the carrier of ({x} opp+id) st ( i <= b1 & j <= b1 ) by A3; ::_thesis: verum end; thus {x} opp+id is monotone ::_thesis: {x} opp+id is antitone proof let i, j be Element of ({x} opp+id); :: according to WAYBEL_0:def_9,WAYBEL_1:def_2 ::_thesis: ( not i <= j or (netmap (({x} opp+id),T)) . i <= (netmap (({x} opp+id),T)) . j ) A4: i = x by A1, TARSKI:def_1; j = x by A1, TARSKI:def_1; hence ( not i <= j or (netmap (({x} opp+id),T)) . i <= (netmap (({x} opp+id),T)) . j ) by A4, YELLOW_0:def_1; ::_thesis: verum end; let i, j be Element of ({x} opp+id); :: according to WAYBEL21:def_2 ::_thesis: ( i <= j implies ({x} opp+id) . i >= ({x} opp+id) . j ) A5: i = x by A1, TARSKI:def_1; j = x by A1, TARSKI:def_1; hence ( i <= j implies ({x} opp+id) . i >= ({x} opp+id) . j ) by A5, YELLOW_0:def_1; ::_thesis: verum end; end; registration let T be non empty reflexive RelStr ; cluster non empty reflexive transitive strict directed monotone antitone for NetStr over T; existence ex b1 being net of T st ( b1 is monotone & b1 is antitone & b1 is reflexive & b1 is strict ) proof set x = the Element of T; take { the Element of T} opp+id ; ::_thesis: ( { the Element of T} opp+id is monotone & { the Element of T} opp+id is antitone & { the Element of T} opp+id is reflexive & { the Element of T} opp+id is strict ) thus ( { the Element of T} opp+id is monotone & { the Element of T} opp+id is antitone & { the Element of T} opp+id is reflexive & { the Element of T} opp+id is strict ) ; ::_thesis: verum end; end; registration let T be non empty RelStr ; let F be non empty Subset of T; clusterF opp+id -> antitone ; coherence F opp+id is antitone proof let i, j be Element of (F opp+id); :: according to WAYBEL21:def_2 ::_thesis: ( i <= j implies (F opp+id) . i >= (F opp+id) . j ) A1: F opp+id is full SubRelStr of T opp by YELLOW_9:7; then reconsider x = i, y = j as Element of (T opp) by YELLOW_0:58; assume i <= j ; ::_thesis: (F opp+id) . i >= (F opp+id) . j then x <= y by A1, YELLOW_0:59; then ~ x >= ~ y by YELLOW_7:1; then (F opp+id) . i >= ~ y by YELLOW_9:7; hence (F opp+id) . i >= (F opp+id) . j by YELLOW_9:7; ::_thesis: verum end; end; registration let S, T be non empty reflexive RelStr ; let f be monotone Function of S,T; let N be non empty antitone NetStr over S; clusterf * N -> antitone ; coherence f * N is antitone proof let i, j be Element of (f * N); :: according to WAYBEL21:def_2 ::_thesis: ( i <= j implies (f * N) . i >= (f * N) . j ) A1: the mapping of (f * N) = f * the mapping of N by WAYBEL_9:def_8; A2: RelStr(# the carrier of (f * N), the InternalRel of (f * N) #) = RelStr(# the carrier of N, the InternalRel of N #) by WAYBEL_9:def_8; then reconsider x = i, y = j as Element of N ; assume i <= j ; ::_thesis: (f * N) . i >= (f * N) . j then x <= y by A2, YELLOW_0:1; then N . x >= N . y by Def2; then f . (N . x) >= f . (N . y) by WAYBEL_1:def_2; then (f * N) . i >= f . (N . y) by A1, FUNCT_2:15; hence (f * N) . i >= (f * N) . j by A1, FUNCT_2:15; ::_thesis: verum end; end; theorem Th25: :: WAYBEL21:25 for S being complete LATTICE for N being net of S holds { ("/\" ( { (N . i) where i is Element of N : i >= j } ,S)) where j is Element of N : verum } is non empty directed Subset of S proof let S be complete LATTICE; ::_thesis: for N being net of S holds { ("/\" ( { (N . i) where i is Element of N : i >= j } ,S)) where j is Element of N : verum } is non empty directed Subset of S let N be net of S; ::_thesis: { ("/\" ( { (N . i) where i is Element of N : i >= j } ,S)) where j is Element of N : verum } is non empty directed Subset of S set X = { ("/\" ( { (N . i) where i is Element of N : i >= j } ,S)) where j is Element of N : verum } ; { ("/\" ( { (N . i) where i is Element of N : i >= j } ,S)) where j is Element of N : verum } c= the carrier of S proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,S)) where j is Element of N : verum } or x in the carrier of S ) assume x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,S)) where j is Element of N : verum } ; ::_thesis: x in the carrier of S then ex j being Element of N st x = "/\" ( { (N . i) where i is Element of N : i >= j } ,S) ; hence x in the carrier of S ; ::_thesis: verum end; then reconsider X = { ("/\" ( { (N . i) where i is Element of N : i >= j } ,S)) where j is Element of N : verum } as Subset of S ; ( not X is empty & X is directed ) by WAYBEL11:30; hence { ("/\" ( { (N . i) where i is Element of N : i >= j } ,S)) where j is Element of N : verum } is non empty directed Subset of S ; ::_thesis: verum end; theorem :: WAYBEL21:26 for S being non empty Poset for N being reflexive monotone net of S holds { ("/\" ( { (N . i) where i is Element of N : i >= j } ,S)) where j is Element of N : verum } is non empty directed Subset of S proof let S be non empty Poset; ::_thesis: for N being reflexive monotone net of S holds { ("/\" ( { (N . i) where i is Element of N : i >= j } ,S)) where j is Element of N : verum } is non empty directed Subset of S let N be reflexive monotone net of S; ::_thesis: { ("/\" ( { (N . i) where i is Element of N : i >= j } ,S)) where j is Element of N : verum } is non empty directed Subset of S set X = { ("/\" ( { (N . i) where i is Element of N : i >= j } ,S)) where j is Element of N : verum } ; set jj = the Element of N; A1: "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,S) in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,S)) where j is Element of N : verum } ; { ("/\" ( { (N . i) where i is Element of N : i >= j } ,S)) where j is Element of N : verum } c= the carrier of S proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,S)) where j is Element of N : verum } or x in the carrier of S ) assume x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,S)) where j is Element of N : verum } ; ::_thesis: x in the carrier of S then ex j being Element of N st x = "/\" ( { (N . i) where i is Element of N : i >= j } ,S) ; hence x in the carrier of S ; ::_thesis: verum end; then reconsider X = { ("/\" ( { (N . i) where i is Element of N : i >= j } ,S)) where j is Element of N : verum } as non empty Subset of S by A1; X is directed proof let x, y be Element of S; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in X or not y in X or ex b1 being Element of the carrier of S st ( b1 in X & x <= b1 & y <= b1 ) ) assume x in X ; ::_thesis: ( not y in X or ex b1 being Element of the carrier of S st ( b1 in X & x <= b1 & y <= b1 ) ) then consider j1 being Element of N such that A2: x = "/\" ( { (N . i) where i is Element of N : i >= j1 } ,S) ; assume y in X ; ::_thesis: ex b1 being Element of the carrier of S st ( b1 in X & x <= b1 & y <= b1 ) then consider j2 being Element of N such that A3: y = "/\" ( { (N . i) where i is Element of N : i >= j2 } ,S) ; reconsider j1 = j1, j2 = j2 as Element of N ; [#] N is directed by WAYBEL_0:def_6; then consider j being Element of N such that j in [#] N and A4: j >= j1 and A5: j >= j2 by WAYBEL_0:def_1; set z = "/\" ( { (N . i) where i is Element of N : i >= j } ,S); take "/\" ( { (N . i) where i is Element of N : i >= j } ,S) ; ::_thesis: ( "/\" ( { (N . i) where i is Element of N : i >= j } ,S) in X & x <= "/\" ( { (N . i) where i is Element of N : i >= j } ,S) & y <= "/\" ( { (N . i) where i is Element of N : i >= j } ,S) ) thus "/\" ( { (N . i) where i is Element of N : i >= j } ,S) in X ; ::_thesis: ( x <= "/\" ( { (N . i) where i is Element of N : i >= j } ,S) & y <= "/\" ( { (N . i) where i is Element of N : i >= j } ,S) ) deffunc H1( Element of N) -> set = { (N . i) where i is Element of N : i >= \$1 } ; A6: for j being Element of N holds ex_inf_of H1(j),S proof let j be Element of N; ::_thesis: ex_inf_of H1(j),S reconsider j9 = j as Element of N ; now__::_thesis:_ex_x_being_Element_of_the_carrier_of_S_st_ (_x_is_<=_than_H1(j)_&_(_for_y_being_Element_of_S_st_y_is_<=_than_H1(j)_holds_ y_<=_x_)_) take x = N . j; ::_thesis: ( x is_<=_than H1(j) & ( for y being Element of S st y is_<=_than H1(j) holds y <= x ) ) j9 <= j9 ; then A7: x in H1(j) ; thus x is_<=_than H1(j) ::_thesis: for y being Element of S st y is_<=_than H1(j) holds y <= x proof let y be Element of S; :: according to LATTICE3:def_8 ::_thesis: ( not y in H1(j) or x <= y ) assume y in H1(j) ; ::_thesis: x <= y then ex i being Element of N st ( y = N . i & i >= j ) ; hence x <= y by WAYBEL11:def_9; ::_thesis: verum end; let y be Element of S; ::_thesis: ( y is_<=_than H1(j) implies y <= x ) assume y is_<=_than H1(j) ; ::_thesis: y <= x hence y <= x by A7, LATTICE3:def_8; ::_thesis: verum end; hence ex_inf_of H1(j),S by YELLOW_0:16; ::_thesis: verum end; then A8: ex_inf_of H1(j1),S ; A9: ex_inf_of H1(j2),S by A6; A10: ex_inf_of H1(j),S by A6; set A = { (N . i) where i is Element of N : i >= j } ; { (N . i) where i is Element of N : i >= j } c= { (N . k) where k is Element of N : k >= j1 } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (N . i) where i is Element of N : i >= j } or a in { (N . k) where k is Element of N : k >= j1 } ) assume a in { (N . i) where i is Element of N : i >= j } ; ::_thesis: a in { (N . k) where k is Element of N : k >= j1 } then consider k being Element of N such that A11: a = N . k and A12: k >= j ; reconsider k = k as Element of N ; k >= j1 by A4, A12, ORDERS_2:3; hence a in { (N . k) where k is Element of N : k >= j1 } by A11; ::_thesis: verum end; hence "/\" ( { (N . i) where i is Element of N : i >= j } ,S) >= x by A2, A8, A10, YELLOW_0:35; ::_thesis: y <= "/\" ( { (N . i) where i is Element of N : i >= j } ,S) { (N . i) where i is Element of N : i >= j } c= { (N . k) where k is Element of N : k >= j2 } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (N . i) where i is Element of N : i >= j } or a in { (N . k) where k is Element of N : k >= j2 } ) assume a in { (N . i) where i is Element of N : i >= j } ; ::_thesis: a in { (N . k) where k is Element of N : k >= j2 } then consider k being Element of N such that A13: a = N . k and A14: k >= j ; reconsider k = k as Element of N ; k >= j2 by A5, A14, ORDERS_2:3; hence a in { (N . k) where k is Element of N : k >= j2 } by A13; ::_thesis: verum end; hence y <= "/\" ( { (N . i) where i is Element of N : i >= j } ,S) by A3, A9, A10, YELLOW_0:35; ::_thesis: verum end; hence { ("/\" ( { (N . i) where i is Element of N : i >= j } ,S)) where j is Element of N : verum } is non empty directed Subset of S ; ::_thesis: verum end; theorem Th27: :: WAYBEL21:27 for S being non empty 1-sorted for N being non empty NetStr over S for X being set st rng the mapping of N c= X holds N is_eventually_in X proof let S be non empty 1-sorted ; ::_thesis: for N being non empty NetStr over S for X being set st rng the mapping of N c= X holds N is_eventually_in X let N be non empty NetStr over S; ::_thesis: for X being set st rng the mapping of N c= X holds N is_eventually_in X let X be set ; ::_thesis: ( rng the mapping of N c= X implies N is_eventually_in X ) assume A1: rng the mapping of N c= X ; ::_thesis: N is_eventually_in X set i = the Element of N; take the Element of N ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds ( not the Element of N <= b1 or N . b1 in X ) let j be Element of N; ::_thesis: ( not the Element of N <= j or N . j in X ) N . j in rng the mapping of N by FUNCT_2:4; hence ( not the Element of N <= j or N . j in X ) by A1; ::_thesis: verum end; theorem Th28: :: WAYBEL21:28 for R being non empty /\-complete Poset for F being non empty filtered Subset of R holds lim_inf (F opp+id) = inf F proof let R be non empty /\-complete Poset; ::_thesis: for F being non empty filtered Subset of R holds lim_inf (F opp+id) = inf F let F be non empty filtered Subset of R; ::_thesis: lim_inf (F opp+id) = inf F set N = F opp+id ; defpred S1[ set ] means verum; deffunc H1( Element of (F opp+id)) -> Element of the carrier of R = inf F; deffunc H2( Element of (F opp+id)) -> Element of the carrier of R = "/\" ( { ((F opp+id) . i) where i is Element of (F opp+id) : i >= \$1 } ,R); A1: for v being Element of (F opp+id) st S1[v] holds H1(v) = H2(v) proof let v be Element of (F opp+id); ::_thesis: ( S1[v] implies H1(v) = H2(v) ) set X = { ((F opp+id) . i) where i is Element of (F opp+id) : i >= v } ; A2: the carrier of (F opp+id) = F by YELLOW_9:7; then v in F ; then reconsider j = v as Element of R ; reconsider vv = v as Element of (F opp+id) ; A3: { ((F opp+id) . i) where i is Element of (F opp+id) : i >= v } c= F proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ((F opp+id) . i) where i is Element of (F opp+id) : i >= v } or x in F ) assume x in { ((F opp+id) . i) where i is Element of (F opp+id) : i >= v } ; ::_thesis: x in F then consider i being Element of (F opp+id) such that A4: x = (F opp+id) . i and i >= v ; reconsider i = i as Element of (F opp+id) ; x = i by A4, YELLOW_9:7; hence x in F by A2; ::_thesis: verum end; vv <= vv ; then (F opp+id) . v in { ((F opp+id) . i) where i is Element of (F opp+id) : i >= v } ; then reconsider X = { ((F opp+id) . i) where i is Element of (F opp+id) : i >= v } as non empty Subset of R by A3, XBOOLE_1:1; A5: ex_inf_of F,R by WAYBEL_0:76; A6: ex_inf_of X,R by WAYBEL_0:76; then A7: inf X >= inf F by A3, A5, YELLOW_0:35; F is_>=_than inf X proof let a be Element of R; :: according to LATTICE3:def_8 ::_thesis: ( not a in F or inf X <= a ) assume a in F ; ::_thesis: inf X <= a then consider b being Element of R such that A8: b in F and A9: a >= b and A10: j >= b by A2, WAYBEL_0:def_2; reconsider k = b as Element of (F opp+id) by A8, YELLOW_9:7; A11: F opp+id is full SubRelStr of R opp by YELLOW_9:7; A12: j ~ <= b ~ by A10, LATTICE3:9; A13: (F opp+id) . k = b by YELLOW_9:7; k >= vv by A11, A12, YELLOW_0:60; then b in X by A13; then A14: {b} c= X by ZFMISC_1:31; A15: ex_inf_of {b},R by YELLOW_0:38; inf {b} = b by YELLOW_0:39; then b >= inf X by A6, A14, A15, YELLOW_0:35; hence inf X <= a by A9, YELLOW_0:def_2; ::_thesis: verum end; then inf F >= "/\" (X,R) by A5, YELLOW_0:31; hence ( S1[v] implies H1(v) = H2(v) ) by A7, ORDERS_2:2; ::_thesis: verum end; A16: { H1(j) where j is Element of (F opp+id) : S1[j] } = { H2(k) where k is Element of (F opp+id) : S1[k] } from FRAENKEL:sch_6(A1); A17: ex j being Element of (F opp+id) st S1[j] ; { (inf F) where j is Element of (F opp+id) : S1[j] } = {(inf F)} from LATTICE3:sch_1(A17); hence lim_inf (F opp+id) = "\/" ({(inf F)},R) by A16, WAYBEL11:def_6 .= inf F by YELLOW_0:39 ; ::_thesis: verum end; theorem Th29: :: WAYBEL21:29 for S, T being non empty /\-complete Poset for X being non empty filtered Subset of S for f being monotone Function of S,T holds lim_inf (f * (X opp+id)) = inf (f .: X) proof let S, T be non empty /\-complete Poset; ::_thesis: for X being non empty filtered Subset of S for f being monotone Function of S,T holds lim_inf (f * (X opp+id)) = inf (f .: X) let X be non empty filtered Subset of S; ::_thesis: for f being monotone Function of S,T holds lim_inf (f * (X opp+id)) = inf (f .: X) let f be monotone Function of S,T; ::_thesis: lim_inf (f * (X opp+id)) = inf (f .: X) set M = X opp+id ; set N = f * (X opp+id); deffunc H1( Element of (f * (X opp+id))) -> set = { ((f * (X opp+id)) . i) where i is Element of (f * (X opp+id)) : i >= \$1 } ; deffunc H2( Element of (f * (X opp+id))) -> Element of the carrier of T = "/\" (H1(\$1),T); A1: RelStr(# the carrier of (f * (X opp+id)), the InternalRel of (f * (X opp+id)) #) = RelStr(# the carrier of (X opp+id), the InternalRel of (X opp+id) #) by WAYBEL_9:def_8; A2: the mapping of (f * (X opp+id)) = f * the mapping of (X opp+id) by WAYBEL_9:def_8; A3: the carrier of (X opp+id) = X by YELLOW_9:7; A4: the mapping of (X opp+id) = id X by WAYBEL19:27; defpred S1[ set ] means verum; deffunc H3( set ) -> Element of the carrier of T = inf (f .: X); A5: for j being Element of (f * (X opp+id)) st S1[j] holds H2(j) = H3(j) proof let j be Element of (f * (X opp+id)); ::_thesis: ( S1[j] implies H2(j) = H3(j) ) reconsider j = j as Element of (f * (X opp+id)) ; A6: [#] (f * (X opp+id)) is directed by WAYBEL_0:def_6; then consider i9 being Element of (f * (X opp+id)) such that i9 in [#] (f * (X opp+id)) and A7: i9 >= j and i9 >= j by WAYBEL_0:def_1; A8: H1(j) c= f .: X proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in H1(j) or a in f .: X ) assume a in H1(j) ; ::_thesis: a in f .: X then consider i being Element of (f * (X opp+id)) such that A9: a = (f * (X opp+id)) . i and i >= j ; reconsider i = i as Element of (f * (X opp+id)) ; reconsider i9 = i as Element of (X opp+id) by A1; A10: (f * (X opp+id)) . i = f . ((id X) . i) by A1, A2, A4, FUNCT_2:15 .= f . i9 by A3, FUNCT_1:18 ; i9 in X by A3; hence a in f .: X by A9, A10, FUNCT_2:35; ::_thesis: verum end; then A11: H1(j) c= the carrier of T by XBOOLE_1:1; (f * (X opp+id)) . i9 in H1(j) by A7; then A12: ex_inf_of H1(j),T by A11, WAYBEL_0:76; A13: ex_inf_of f .: X,T by WAYBEL_0:76; then A14: H2(j) >= inf (f .: X) by A8, A12, YELLOW_0:35; H2(j) is_<=_than f .: X proof let x be Element of T; :: according to LATTICE3:def_8 ::_thesis: ( not x in f .: X or H2(j) <= x ) assume x in f .: X ; ::_thesis: H2(j) <= x then consider y being set such that A15: y in the carrier of S and A16: y in X and A17: x = f . y by FUNCT_2:64; reconsider y = y as Element of (f * (X opp+id)) by A1, A16, YELLOW_9:7; consider i being Element of (f * (X opp+id)) such that i in [#] (f * (X opp+id)) and A18: i >= y and A19: i >= j by A6, WAYBEL_0:def_1; i in X by A1, A3; then reconsider xi = i, xy = y as Element of S by A15; X opp+id is full SubRelStr of S opp by YELLOW_9:7; then f * (X opp+id) is full SubRelStr of S opp by A1, Th12; then xi ~ >= xy ~ by A18, YELLOW_0:59; then xi <= xy by LATTICE3:9; then A20: f . xi <= x by A17, WAYBEL_1:def_2; (f * (X opp+id)) . i = f . ((id X) . i) by A1, A2, A4, FUNCT_2:15 .= f . xi by A1, A3, FUNCT_1:18 ; then f . xi in H1(j) by A19; then f . xi >= H2(j) by A12, YELLOW_4:2; hence H2(j) <= x by A20, ORDERS_2:3; ::_thesis: verum end; then H2(j) <= inf (f .: X) by A13, YELLOW_0:31; hence ( S1[j] implies H2(j) = H3(j) ) by A14, ORDERS_2:2; ::_thesis: verum end; A21: ex j being Element of (f * (X opp+id)) st S1[j] ; { H2(j) where j is Element of (f * (X opp+id)) : S1[j] } = { H3(j) where j is Element of (f * (X opp+id)) : S1[j] } from FRAENKEL:sch_6(A5) .= { (inf (f .: X)) where j is Element of (f * (X opp+id)) : S1[j] } .= {(inf (f .: X))} from LATTICE3:sch_1(A21) ; hence lim_inf (f * (X opp+id)) = sup {(inf (f .: X))} by WAYBEL11:def_6 .= inf (f .: X) by YELLOW_0:39 ; ::_thesis: verum end; theorem Th30: :: WAYBEL21:30 for S, T being non empty TopPoset for X being non empty filtered Subset of S for f being monotone Function of S,T for Y being non empty filtered Subset of T st Y = f .: X holds f * (X opp+id) is subnet of Y opp+id proof let S, T be non empty TopPoset; ::_thesis: for X being non empty filtered Subset of S for f being monotone Function of S,T for Y being non empty filtered Subset of T st Y = f .: X holds f * (X opp+id) is subnet of Y opp+id let X be non empty filtered Subset of S; ::_thesis: for f being monotone Function of S,T for Y being non empty filtered Subset of T st Y = f .: X holds f * (X opp+id) is subnet of Y opp+id let f be monotone Function of S,T; ::_thesis: for Y being non empty filtered Subset of T st Y = f .: X holds f * (X opp+id) is subnet of Y opp+id let Y be non empty filtered Subset of T; ::_thesis: ( Y = f .: X implies f * (X opp+id) is subnet of Y opp+id ) assume A1: Y = f .: X ; ::_thesis: f * (X opp+id) is subnet of Y opp+id set N = f * (X opp+id); set M = Y opp+id ; A2: RelStr(# the carrier of (f * (X opp+id)), the InternalRel of (f * (X opp+id)) #) = RelStr(# the carrier of (X opp+id), the InternalRel of (X opp+id) #) by WAYBEL_9:def_8; A3: the mapping of (f * (X opp+id)) = f * the mapping of (X opp+id) by WAYBEL_9:def_8; A4: the carrier of (Y opp+id) = Y by YELLOW_9:7; A5: the mapping of (Y opp+id) = id Y by WAYBEL19:27; A6: the carrier of (X opp+id) = X by YELLOW_9:7; the mapping of (X opp+id) = id X by WAYBEL19:27; then A7: the mapping of (f * (X opp+id)) = f | X by A3, RELAT_1:65; then A8: rng the mapping of (f * (X opp+id)) = f .: X by RELAT_1:115; dom the mapping of (f * (X opp+id)) = X by A2, A6, FUNCT_2:def_1; then reconsider g = f | X as Function of (f * (X opp+id)),(Y opp+id) by A1, A2, A4, A6, A7, A8, FUNCT_2:def_1, RELSET_1:4; take g ; :: according to YELLOW_6:def_9 ::_thesis: ( the mapping of (f * (X opp+id)) = the mapping of (Y opp+id) * g & ( for b1 being Element of the carrier of (Y opp+id) ex b2 being Element of the carrier of (f * (X opp+id)) st for b3 being Element of the carrier of (f * (X opp+id)) holds ( not b2 <= b3 or b1 <= g . b3 ) ) ) thus the mapping of (f * (X opp+id)) = the mapping of (Y opp+id) * g by A1, A5, A7, A8, RELAT_1:53; ::_thesis: for b1 being Element of the carrier of (Y opp+id) ex b2 being Element of the carrier of (f * (X opp+id)) st for b3 being Element of the carrier of (f * (X opp+id)) holds ( not b2 <= b3 or b1 <= g . b3 ) let m be Element of (Y opp+id); ::_thesis: ex b1 being Element of the carrier of (f * (X opp+id)) st for b2 being Element of the carrier of (f * (X opp+id)) holds ( not b1 <= b2 or m <= g . b2 ) consider n being set such that A9: n in the carrier of S and A10: n in X and A11: m = f . n by A1, A4, FUNCT_2:64; reconsider n = n as Element of (f * (X opp+id)) by A2, A10, YELLOW_9:7; take n ; ::_thesis: for b1 being Element of the carrier of (f * (X opp+id)) holds ( not n <= b1 or m <= g . b1 ) let p be Element of (f * (X opp+id)); ::_thesis: ( not n <= p or m <= g . p ) p in X by A2, A6; then reconsider n9 = n, p9 = p as Element of S by A9; reconsider fp = f . p9 as Element of (Y opp+id) by A1, A2, A4, A6, FUNCT_2:35; X opp+id is SubRelStr of S opp by YELLOW_9:7; then A12: f * (X opp+id) is SubRelStr of S opp by A2, Th12; A13: Y opp+id is full SubRelStr of T opp by YELLOW_9:7; assume n <= p ; ::_thesis: m <= g . p then n9 ~ <= p9 ~ by A12, YELLOW_0:59; then n9 >= p9 by LATTICE3:9; then f . n9 >= f . p9 by WAYBEL_1:def_2; then (f . n9) ~ <= (f . p9) ~ by LATTICE3:9; then fp >= m by A11, A13, YELLOW_0:60; hence m <= g . p by A2, A6, FUNCT_1:49; ::_thesis: verum end; theorem :: WAYBEL21:31 for S, T being non empty TopPoset for X being non empty filtered Subset of S for f being monotone Function of S,T for Y being non empty filtered Subset of T st Y = f .: X holds Lim (Y opp+id) c= Lim (f * (X opp+id)) proof let S, T be non empty TopPoset; ::_thesis: for X being non empty filtered Subset of S for f being monotone Function of S,T for Y being non empty filtered Subset of T st Y = f .: X holds Lim (Y opp+id) c= Lim (f * (X opp+id)) let X be non empty filtered Subset of S; ::_thesis: for f being monotone Function of S,T for Y being non empty filtered Subset of T st Y = f .: X holds Lim (Y opp+id) c= Lim (f * (X opp+id)) let f be monotone Function of S,T; ::_thesis: for Y being non empty filtered Subset of T st Y = f .: X holds Lim (Y opp+id) c= Lim (f * (X opp+id)) let Y be non empty filtered Subset of T; ::_thesis: ( Y = f .: X implies Lim (Y opp+id) c= Lim (f * (X opp+id)) ) assume Y = f .: X ; ::_thesis: Lim (Y opp+id) c= Lim (f * (X opp+id)) then f * (X opp+id) is subnet of Y opp+id by Th30; hence Lim (Y opp+id) c= Lim (f * (X opp+id)) by YELLOW_6:32; ::_thesis: verum end; theorem Th32: :: WAYBEL21:32 for S being non empty reflexive RelStr for D being non empty Subset of S holds ( the mapping of (Net-Str D) = id D & the carrier of (Net-Str D) = D & Net-Str D is full SubRelStr of S ) proof let S be non empty reflexive RelStr ; ::_thesis: for D being non empty Subset of S holds ( the mapping of (Net-Str D) = id D & the carrier of (Net-Str D) = D & Net-Str D is full SubRelStr of S ) let D be non empty Subset of S; ::_thesis: ( the mapping of (Net-Str D) = id D & the carrier of (Net-Str D) = D & Net-Str D is full SubRelStr of S ) set N = Net-Str D; A1: dom (id D) = D ; rng (id D) = D ; then reconsider g = id D as Function of D, the carrier of S by A1, FUNCT_2:def_1, RELSET_1:4; (id the carrier of S) | D = id D by FUNCT_3:1; then A2: Net-Str D = NetStr(# D,( the InternalRel of S |_2 D),g #) by WAYBEL17:def_4; then the InternalRel of (Net-Str D) c= the InternalRel of S by XBOOLE_1:17; hence ( the mapping of (Net-Str D) = id D & the carrier of (Net-Str D) = D & Net-Str D is full SubRelStr of S ) by A2, YELLOW_0:def_13, YELLOW_0:def_14; ::_thesis: verum end; theorem Th33: :: WAYBEL21:33 for S, T being non empty up-complete Poset for f being monotone Function of S,T for D being non empty directed Subset of S holds lim_inf (f * (Net-Str D)) = sup (f .: D) proof let S, T be non empty up-complete Poset; ::_thesis: for f being monotone Function of S,T for D being non empty directed Subset of S holds lim_inf (f * (Net-Str D)) = sup (f .: D) let f be monotone Function of S,T; ::_thesis: for D being non empty directed Subset of S holds lim_inf (f * (Net-Str D)) = sup (f .: D) let X be non empty directed Subset of S; ::_thesis: lim_inf (f * (Net-Str X)) = sup (f .: X) set M = Net-Str X; set N = f * (Net-Str X); deffunc H1( Element of (f * (Net-Str X))) -> set = { ((f * (Net-Str X)) . i) where i is Element of (f * (Net-Str X)) : i >= \$1 } ; deffunc H2( Element of (f * (Net-Str X))) -> Element of the carrier of T = "/\" (H1(\$1),T); set NT = { H2(j) where j is Element of (f * (Net-Str X)) : verum } ; A1: RelStr(# the carrier of (f * (Net-Str X)), the InternalRel of (f * (Net-Str X)) #) = RelStr(# the carrier of (Net-Str X), the InternalRel of (Net-Str X) #) by WAYBEL_9:def_8; A2: the mapping of (f * (Net-Str X)) = f * the mapping of (Net-Str X) by WAYBEL_9:def_8; A3: the carrier of (Net-Str X) = X by Th32; A4: the mapping of (Net-Str X) = id X by Th32; A5: now__::_thesis:_for_i_being_Element_of_(f_*_(Net-Str_X))_holds_(f_*_(Net-Str_X))_._i_=_f_._i let i be Element of (f * (Net-Str X)); ::_thesis: (f * (Net-Str X)) . i = f . i thus (f * (Net-Str X)) . i = f . ((id X) . i) by A1, A2, A4, FUNCT_2:15 .= f . i by A1, A3, FUNCT_1:18 ; ::_thesis: verum end; A6: for i being Element of (f * (Net-Str X)) holds H2(i) = f . i proof let i be Element of (f * (Net-Str X)); ::_thesis: H2(i) = f . i i in X by A1, A3; then reconsider x = i as Element of S ; A7: i <= i ; (f * (Net-Str X)) . i = f . x by A5; then f . x in H1(i) by A7; then A8: for z being Element of T st z is_<=_than H1(i) holds z <= f . x by LATTICE3:def_8; f . x is_<=_than H1(i) proof let z be Element of T; :: according to LATTICE3:def_8 ::_thesis: ( not z in H1(i) or f . x <= z ) assume z in H1(i) ; ::_thesis: f . x <= z then consider j being Element of (f * (Net-Str X)) such that A9: z = (f * (Net-Str X)) . j and A10: j >= i ; reconsider j = j as Element of (f * (Net-Str X)) ; j in X by A1, A3; then reconsider y = j as Element of S ; A11: Net-Str X is full SubRelStr of S by Th32; RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of S, the InternalRel of S #) ; then f * (Net-Str X) is full SubRelStr of S by A1, A11, Th12; then y >= x by A10, YELLOW_0:59; then f . y >= f . x by WAYBEL_1:def_2; hence f . x <= z by A5, A9; ::_thesis: verum end; hence H2(i) = f . i by A8, YELLOW_0:31; ::_thesis: verum end; { H2(j) where j is Element of (f * (Net-Str X)) : verum } = f .: X proof thus { H2(j) where j is Element of (f * (Net-Str X)) : verum } c= f .: X :: according to XBOOLE_0:def_10 ::_thesis: f .: X c= { H2(j) where j is Element of (f * (Net-Str X)) : verum } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { H2(j) where j is Element of (f * (Net-Str X)) : verum } or x in f .: X ) assume x in { H2(j) where j is Element of (f * (Net-Str X)) : verum } ; ::_thesis: x in f .: X then consider j being Element of (f * (Net-Str X)) such that A12: x = H2(j) ; reconsider j = j as Element of (f * (Net-Str X)) ; A13: x = f . j by A6, A12; j in X by A1, A3; hence x in f .: X by A13, FUNCT_2:35; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: X or y in { H2(j) where j is Element of (f * (Net-Str X)) : verum } ) assume y in f .: X ; ::_thesis: y in { H2(j) where j is Element of (f * (Net-Str X)) : verum } then consider x being set such that A14: x in the carrier of S and A15: x in X and A16: y = f . x by FUNCT_2:64; reconsider x = x as Element of S by A14; reconsider i = x as Element of (f * (Net-Str X)) by A1, A15, Th32; f . x = H2(i) by A6; hence y in { H2(j) where j is Element of (f * (Net-Str X)) : verum } by A16; ::_thesis: verum end; hence lim_inf (f * (Net-Str X)) = sup (f .: X) by WAYBEL11:def_6; ::_thesis: verum end; theorem Th34: :: WAYBEL21:34 for S being non empty reflexive RelStr for D being non empty directed Subset of S for i, j being Element of (Net-Str D) holds ( i <= j iff (Net-Str D) . i <= (Net-Str D) . j ) proof let S be non empty reflexive RelStr ; ::_thesis: for D being non empty directed Subset of S for i, j being Element of (Net-Str D) holds ( i <= j iff (Net-Str D) . i <= (Net-Str D) . j ) let D be non empty directed Subset of S; ::_thesis: for i, j being Element of (Net-Str D) holds ( i <= j iff (Net-Str D) . i <= (Net-Str D) . j ) A1: dom (id D) = D ; rng (id D) = D ; then reconsider g = id D as Function of D, the carrier of S by A1, FUNCT_2:def_1, RELSET_1:4; (id the carrier of S) | D = id D by FUNCT_3:1; then Net-Str D = Net-Str (D,g) by WAYBEL17:9; hence for i, j being Element of (Net-Str D) holds ( i <= j iff (Net-Str D) . i <= (Net-Str D) . j ) by WAYBEL11:def_10; ::_thesis: verum end; theorem Th35: :: WAYBEL21:35 for T being complete Lawson TopLattice for D being non empty directed Subset of T holds sup D in Lim (Net-Str D) proof let T be complete Lawson TopLattice; ::_thesis: for D being non empty directed Subset of T holds sup D in Lim (Net-Str D) let D be non empty directed Subset of T; ::_thesis: sup D in Lim (Net-Str D) set N = Net-Str D; A1: the mapping of (Net-Str D) = id D by Th32; A2: the carrier of (Net-Str D) = D by Th32; set K = the prebasis of T; now__::_thesis:_for_A_being_Subset_of_T_st_sup_D_in_A_&_A_in_the_prebasis_of_T_holds_ Net-Str_D_is_eventually_in_A let A be Subset of T; ::_thesis: ( sup D in A & A in the prebasis of T implies Net-Str D is_eventually_in A ) assume A3: sup D in A ; ::_thesis: ( A in the prebasis of T implies Net-Str D is_eventually_in A ) A4: the prebasis of T c= the topology of T by TOPS_2:64; assume A in the prebasis of T ; ::_thesis: Net-Str D is_eventually_in A then A is open by A4, PRE_TOPC:def_2; then A is property(S) by WAYBEL19:36; then consider y being Element of T such that A5: y in D and A6: for x being Element of T st x in D & x >= y holds x in A by A3, WAYBEL11:def_3; reconsider i = y as Element of (Net-Str D) by A5, Th32; thus Net-Str D is_eventually_in A ::_thesis: verum proof take i ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of (Net-Str D) holds ( not i <= b1 or (Net-Str D) . b1 in A ) let j be Element of (Net-Str D); ::_thesis: ( not i <= j or (Net-Str D) . j in A ) A7: j = (Net-Str D) . j by A1, A2, FUNCT_1:17; A8: y = (Net-Str D) . i by A1, A2, FUNCT_1:17; assume j >= i ; ::_thesis: (Net-Str D) . j in A then (Net-Str D) . j >= (Net-Str D) . i by Th34; hence (Net-Str D) . j in A by A2, A6, A7, A8; ::_thesis: verum end; end; hence sup D in Lim (Net-Str D) by WAYBEL19:25; ::_thesis: verum end; definition let T be non empty 1-sorted ; let N be net of T; let M be non empty NetStr over T; assume A1: M is subnet of N ; mode Embedding of M,N -> Function of M,N means :Def3: :: WAYBEL21:def 3 ( the mapping of M = the mapping of N * it & ( for m being Element of N ex n being Element of M st for p being Element of M st n <= p holds m <= it . p ) ); existence ex b1 being Function of M,N st ( the mapping of M = the mapping of N * b1 & ( for m being Element of N ex n being Element of M st for p being Element of M st n <= p holds m <= b1 . p ) ) by A1, YELLOW_6:def_9; end; :: deftheorem Def3 defines Embedding WAYBEL21:def_3_:_ for T being non empty 1-sorted for N being net of T for M being non empty NetStr over T st M is subnet of N holds for b4 being Function of M,N holds ( b4 is Embedding of M,N iff ( the mapping of M = the mapping of N * b4 & ( for m being Element of N ex n being Element of M st for p being Element of M st n <= p holds m <= b4 . p ) ) ); theorem Th36: :: WAYBEL21:36 for T being non empty 1-sorted for N being net of T for M being subnet of N for e being Embedding of M,N for i being Element of M holds M . i = N . (e . i) proof let T be non empty 1-sorted ; ::_thesis: for N being net of T for M being subnet of N for e being Embedding of M,N for i being Element of M holds M . i = N . (e . i) let N be net of T; ::_thesis: for M being subnet of N for e being Embedding of M,N for i being Element of M holds M . i = N . (e . i) let M be subnet of N; ::_thesis: for e being Embedding of M,N for i being Element of M holds M . i = N . (e . i) let e be Embedding of M,N; ::_thesis: for i being Element of M holds M . i = N . (e . i) let i be Element of M; ::_thesis: M . i = N . (e . i) the mapping of M = the mapping of N * e by Def3; hence M . i = N . (e . i) by FUNCT_2:15; ::_thesis: verum end; theorem Th37: :: WAYBEL21:37 for T being complete LATTICE for N being net of T for M being subnet of N holds lim_inf N <= lim_inf M proof let T be complete LATTICE; ::_thesis: for N being net of T for M being subnet of N holds lim_inf N <= lim_inf M let N be net of T; ::_thesis: for M being subnet of N holds lim_inf N <= lim_inf M let M be subnet of N; ::_thesis: lim_inf N <= lim_inf M deffunc H1( net of T) -> set = { ("/\" ( { (\$1 . i) where i is Element of \$1 : i >= j } ,T)) where j is Element of \$1 : verum } ; A1: "\/" (H1(M),T) is_>=_than H1(N) proof let t be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not t in H1(N) or t <= "\/" (H1(M),T) ) assume t in H1(N) ; ::_thesis: t <= "\/" (H1(M),T) then consider j being Element of N such that A2: t = "/\" ( { (N . i) where i is Element of N : i >= j } ,T) ; set e = the Embedding of M,N; reconsider j = j as Element of N ; consider j9 being Element of M such that A3: for p being Element of M st j9 <= p holds j <= the Embedding of M,N . p by Def3; set X = { (N . i) where i is Element of N : i >= j } ; set Y = { (M . i) where i is Element of M : i >= j9 } ; A4: ex_inf_of { (N . i) where i is Element of N : i >= j } ,T by YELLOW_0:17; A5: ex_inf_of { (M . i) where i is Element of M : i >= j9 } ,T by YELLOW_0:17; { (M . i) where i is Element of M : i >= j9 } c= { (N . i) where i is Element of N : i >= j } proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { (M . i) where i is Element of M : i >= j9 } or y in { (N . i) where i is Element of N : i >= j } ) assume y in { (M . i) where i is Element of M : i >= j9 } ; ::_thesis: y in { (N . i) where i is Element of N : i >= j } then consider i being Element of M such that A6: y = M . i and A7: i >= j9 ; reconsider i = i as Element of M ; the Embedding of M,N . i >= j by A3, A7; then N . ( the Embedding of M,N . i) in { (N . i) where i is Element of N : i >= j } ; hence y in { (N . i) where i is Element of N : i >= j } by A6, Th36; ::_thesis: verum end; then A8: t <= "/\" ( { (M . i) where i is Element of M : i >= j9 } ,T) by A2, A4, A5, YELLOW_0:35; "/\" ( { (M . i) where i is Element of M : i >= j9 } ,T) in H1(M) ; then "/\" ( { (M . i) where i is Element of M : i >= j9 } ,T) <= "\/" (H1(M),T) by YELLOW_2:22; hence t <= "\/" (H1(M),T) by A8, YELLOW_0:def_2; ::_thesis: verum end; A9: lim_inf M = "\/" (H1(M),T) by WAYBEL11:def_6; lim_inf N = "\/" (H1(N),T) by WAYBEL11:def_6; hence lim_inf N <= lim_inf M by A1, A9, YELLOW_0:32; ::_thesis: verum end; theorem Th38: :: WAYBEL21:38 for T being complete LATTICE for N being net of T for M being subnet of N for e being Embedding of M,N st ( for i being Element of N for j being Element of M st e . j <= i holds ex j9 being Element of M st ( j9 >= j & N . i >= M . j9 ) ) holds lim_inf N = lim_inf M proof let T be complete LATTICE; ::_thesis: for N being net of T for M being subnet of N for e being Embedding of M,N st ( for i being Element of N for j being Element of M st e . j <= i holds ex j9 being Element of M st ( j9 >= j & N . i >= M . j9 ) ) holds lim_inf N = lim_inf M let N be net of T; ::_thesis: for M being subnet of N for e being Embedding of M,N st ( for i being Element of N for j being Element of M st e . j <= i holds ex j9 being Element of M st ( j9 >= j & N . i >= M . j9 ) ) holds lim_inf N = lim_inf M let M be subnet of N; ::_thesis: for e being Embedding of M,N st ( for i being Element of N for j being Element of M st e . j <= i holds ex j9 being Element of M st ( j9 >= j & N . i >= M . j9 ) ) holds lim_inf N = lim_inf M let e be Embedding of M,N; ::_thesis: ( ( for i being Element of N for j being Element of M st e . j <= i holds ex j9 being Element of M st ( j9 >= j & N . i >= M . j9 ) ) implies lim_inf N = lim_inf M ) assume A1: for i being Element of N for j being Element of M st e . j <= i holds ex j9 being Element of M st ( j9 >= j & N . i >= M . j9 ) ; ::_thesis: lim_inf N = lim_inf M deffunc H1( net of T) -> set = { ("/\" ( { (\$1 . i) where i is Element of \$1 : i >= j } ,T)) where j is Element of \$1 : verum } ; "\/" (H1(N),T) is_>=_than H1(M) proof let t be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not t in H1(M) or t <= "\/" (H1(N),T) ) assume t in H1(M) ; ::_thesis: t <= "\/" (H1(N),T) then consider j being Element of M such that A2: t = "/\" ( { (M . i) where i is Element of M : i >= j } ,T) ; reconsider j = j as Element of M ; set j9 = e . j; set X = { (N . i) where i is Element of N : i >= e . j } ; set Y = { (M . i) where i is Element of M : i >= j } ; t is_<=_than { (N . i) where i is Element of N : i >= e . j } proof let x be Element of T; :: according to LATTICE3:def_8 ::_thesis: ( not x in { (N . i) where i is Element of N : i >= e . j } or t <= x ) assume x in { (N . i) where i is Element of N : i >= e . j } ; ::_thesis: t <= x then consider i being Element of N such that A3: x = N . i and A4: i >= e . j ; reconsider i = i as Element of N ; consider k being Element of M such that A5: k >= j and A6: N . i >= M . k by A1, A4; M . k in { (M . i) where i is Element of M : i >= j } by A5; then M . k >= t by A2, YELLOW_2:22; hence t <= x by A3, A6, YELLOW_0:def_2; ::_thesis: verum end; then A7: t <= "/\" ( { (N . i) where i is Element of N : i >= e . j } ,T) by YELLOW_0:33; "/\" ( { (N . i) where i is Element of N : i >= e . j } ,T) in H1(N) ; then "/\" ( { (N . i) where i is Element of N : i >= e . j } ,T) <= "\/" (H1(N),T) by YELLOW_2:22; hence t <= "\/" (H1(N),T) by A7, YELLOW_0:def_2; ::_thesis: verum end; then "\/" (H1(N),T) >= "\/" (H1(M),T) by YELLOW_0:32; then lim_inf N >= "\/" (H1(M),T) by WAYBEL11:def_6; then A8: lim_inf N >= lim_inf M by WAYBEL11:def_6; lim_inf M >= lim_inf N by Th37; hence lim_inf N = lim_inf M by A8, YELLOW_0:def_3; ::_thesis: verum end; theorem :: WAYBEL21:39 for T being non empty RelStr for N being net of T for M being non empty full SubNetStr of N st ( for i being Element of N ex j being Element of N st ( j >= i & j in the carrier of M ) ) holds ( M is subnet of N & incl (M,N) is Embedding of M,N ) proof let T be non empty RelStr ; ::_thesis: for N being net of T for M being non empty full SubNetStr of N st ( for i being Element of N ex j being Element of N st ( j >= i & j in the carrier of M ) ) holds ( M is subnet of N & incl (M,N) is Embedding of M,N ) let N be net of T; ::_thesis: for M being non empty full SubNetStr of N st ( for i being Element of N ex j being Element of N st ( j >= i & j in the carrier of M ) ) holds ( M is subnet of N & incl (M,N) is Embedding of M,N ) let M be non empty full SubNetStr of N; ::_thesis: ( ( for i being Element of N ex j being Element of N st ( j >= i & j in the carrier of M ) ) implies ( M is subnet of N & incl (M,N) is Embedding of M,N ) ) assume A1: for i being Element of N ex j being Element of N st ( j >= i & j in the carrier of M ) ; ::_thesis: ( M is subnet of N & incl (M,N) is Embedding of M,N ) A2: the mapping of M = the mapping of N | the carrier of M by YELLOW_6:def_6; A3: M is full SubRelStr of N by YELLOW_6:def_7; then A4: the carrier of M c= the carrier of N by YELLOW_0:def_13; M is directed proof let x, y be Element of M; :: according to YELLOW_6:def_3 ::_thesis: ex b1 being Element of the carrier of M st ( x <= b1 & y <= b1 ) reconsider i = x, j = y as Element of N by A3, YELLOW_0:58; consider k being Element of N such that A5: k >= i and A6: k >= j by YELLOW_6:def_3; consider l being Element of N such that A7: l >= k and A8: l in the carrier of M by A1; reconsider z = l as Element of M by A8; take z ; ::_thesis: ( x <= z & y <= z ) A9: l >= i by A5, A7, YELLOW_0:def_2; l >= j by A6, A7, YELLOW_0:def_2; hence ( x <= z & y <= z ) by A9, YELLOW_6:12; ::_thesis: verum end; then reconsider K = M as net of T by A3; A10: now__::_thesis:_(_the_mapping_of_K_=_the_mapping_of_N_*_(incl_(K,N))_&_(_for_m_being_Element_of_N_ex_n_being_Element_of_K_st_ for_p_being_Element_of_K_st_n_<=_p_holds_ m_<=_(incl_(K,N))_._p_)_) set f = incl (K,N); A11: incl (K,N) = id the carrier of K by A4, YELLOW_9:def_1; hence the mapping of K = the mapping of N * (incl (K,N)) by A2, RELAT_1:65; ::_thesis: for m being Element of N ex n being Element of K st for p being Element of K st n <= p holds m <= (incl (K,N)) . p let m be Element of N; ::_thesis: ex n being Element of K st for p being Element of K st n <= p holds m <= (incl (K,N)) . p consider j being Element of N such that A12: j >= m and A13: j in the carrier of K by A1; reconsider n = j as Element of K by A13; take n = n; ::_thesis: for p being Element of K st n <= p holds m <= (incl (K,N)) . p let p be Element of K; ::_thesis: ( n <= p implies m <= (incl (K,N)) . p ) reconsider q = p as Element of N by A3, YELLOW_0:58; assume n <= p ; ::_thesis: m <= (incl (K,N)) . p then A14: j <= q by YELLOW_6:11; (incl (K,N)) . p = q by A11, FUNCT_1:18; hence m <= (incl (K,N)) . p by A12, A14, YELLOW_0:def_2; ::_thesis: verum end; hence M is subnet of N by YELLOW_6:def_9; ::_thesis: incl (M,N) is Embedding of M,N hence incl (M,N) is Embedding of M,N by A10, Def3; ::_thesis: verum end; theorem Th40: :: WAYBEL21:40 for T being non empty RelStr for N being net of T for i being Element of N holds ( N | i is subnet of N & incl ((N | i),N) is Embedding of N | i,N ) proof let T be non empty RelStr ; ::_thesis: for N being net of T for i being Element of N holds ( N | i is subnet of N & incl ((N | i),N) is Embedding of N | i,N ) let N be net of T; ::_thesis: for i being Element of N holds ( N | i is subnet of N & incl ((N | i),N) is Embedding of N | i,N ) let i be Element of N; ::_thesis: ( N | i is subnet of N & incl ((N | i),N) is Embedding of N | i,N ) set M = N | i; set f = incl ((N | i),N); thus N | i is subnet of N ; ::_thesis: incl ((N | i),N) is Embedding of N | i,N thus N | i is subnet of N ; :: according to WAYBEL21:def_3 ::_thesis: ( the mapping of (N | i) = the mapping of N * (incl ((N | i),N)) & ( for m being Element of N ex n being Element of (N | i) st for p being Element of (N | i) st n <= p holds m <= (incl ((N | i),N)) . p ) ) N | i is full SubNetStr of N by WAYBEL_9:14; then A1: N | i is full SubRelStr of N by YELLOW_6:def_7; A2: incl ((N | i),N) = id the carrier of (N | i) by WAYBEL_9:13, YELLOW_9:def_1; the mapping of (N | i) = the mapping of N | the carrier of (N | i) by WAYBEL_9:def_7; hence the mapping of (N | i) = the mapping of N * (incl ((N | i),N)) by A2, RELAT_1:65; ::_thesis: for m being Element of N ex n being Element of (N | i) st for p being Element of (N | i) st n <= p holds m <= (incl ((N | i),N)) . p let m be Element of N; ::_thesis: ex n being Element of (N | i) st for p being Element of (N | i) st n <= p holds m <= (incl ((N | i),N)) . p consider n9 being Element of N such that A3: n9 >= i and A4: n9 >= m by YELLOW_6:def_3; reconsider n = n9 as Element of (N | i) by A3, WAYBEL_9:def_7; take n ; ::_thesis: for p being Element of (N | i) st n <= p holds m <= (incl ((N | i),N)) . p let p be Element of (N | i); ::_thesis: ( n <= p implies m <= (incl ((N | i),N)) . p ) reconsider p9 = p as Element of N by A1, YELLOW_0:58; assume n <= p ; ::_thesis: m <= (incl ((N | i),N)) . p then n9 <= p9 by A1, YELLOW_0:59; then m <= p9 by A4, YELLOW_0:def_2; hence m <= (incl ((N | i),N)) . p by A2, FUNCT_1:18; ::_thesis: verum end; theorem Th41: :: WAYBEL21:41 for T being complete LATTICE for N being net of T for i being Element of N holds lim_inf (N | i) = lim_inf N proof let T be complete LATTICE; ::_thesis: for N being net of T for i being Element of N holds lim_inf (N | i) = lim_inf N let N be net of T; ::_thesis: for i being Element of N holds lim_inf (N | i) = lim_inf N let i be Element of N; ::_thesis: lim_inf (N | i) = lim_inf N reconsider M = N | i as subnet of N ; reconsider e = incl (M,N) as Embedding of M,N by Th40; M is full SubNetStr of N by WAYBEL_9:14; then A1: M is full SubRelStr of N by YELLOW_6:def_7; A2: incl (M,N) = id the carrier of M by WAYBEL_9:13, YELLOW_9:def_1; now__::_thesis:_for_k_being_Element_of_N for_j_being_Element_of_M_st_e_._j_<=_k_holds_ ex_k9_being_Element_of_M_st_ (_k9_>=_j_&_N_._k_>=_M_._k9_) let k be Element of N; ::_thesis: for j being Element of M st e . j <= k holds ex k9 being Element of M st ( k9 >= j & N . k >= M . k9 ) let j be Element of M; ::_thesis: ( e . j <= k implies ex k9 being Element of M st ( k9 >= j & N . k >= M . k9 ) ) consider j9 being Element of N such that A3: j9 = j and A4: j9 >= i by WAYBEL_9:def_7; assume e . j <= k ; ::_thesis: ex k9 being Element of M st ( k9 >= j & N . k >= M . k9 ) then A5: k >= j9 by A2, A3, FUNCT_1:18; then k >= i by A4, YELLOW_0:def_2; then reconsider k9 = k as Element of M by WAYBEL_9:def_7; take k9 = k9; ::_thesis: ( k9 >= j & N . k >= M . k9 ) thus k9 >= j by A1, A3, A5, YELLOW_0:60; ::_thesis: N . k >= M . k9 A6: M . k9 = N . (e . k9) by Th36; M . k9 <= M . k9 ; hence N . k >= M . k9 by A2, A6, FUNCT_1:18; ::_thesis: verum end; hence lim_inf (N | i) = lim_inf N by Th38; ::_thesis: verum end; theorem Th42: :: WAYBEL21:42 for T being non empty RelStr for N being net of T for X being set st N is_eventually_in X holds ex i being Element of N st ( N . i in X & rng the mapping of (N | i) c= X ) proof let T be non empty RelStr ; ::_thesis: for N being net of T for X being set st N is_eventually_in X holds ex i being Element of N st ( N . i in X & rng the mapping of (N | i) c= X ) let N be net of T; ::_thesis: for X being set st N is_eventually_in X holds ex i being Element of N st ( N . i in X & rng the mapping of (N | i) c= X ) let X be set ; ::_thesis: ( N is_eventually_in X implies ex i being Element of N st ( N . i in X & rng the mapping of (N | i) c= X ) ) given i9 being Element of N such that A1: for j being Element of N st j >= i9 holds N . j in X ; :: according to WAYBEL_0:def_11 ::_thesis: ex i being Element of N st ( N . i in X & rng the mapping of (N | i) c= X ) [#] N is directed by WAYBEL_0:def_6; then consider i being Element of N such that i in [#] N and A2: i9 <= i and i9 <= i by WAYBEL_0:def_1; take i ; ::_thesis: ( N . i in X & rng the mapping of (N | i) c= X ) thus N . i in X by A1, A2; ::_thesis: rng the mapping of (N | i) c= X let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng the mapping of (N | i) or x in X ) assume x in rng the mapping of (N | i) ; ::_thesis: x in X then consider j being set such that A3: j in dom the mapping of (N | i) and A4: x = the mapping of (N | i) . j by FUNCT_1:def_3; A5: dom the mapping of (N | i) = the carrier of (N | i) by FUNCT_2:def_1; reconsider j = j as Element of (N | i) by A3; the carrier of (N | i) = { y where y is Element of N : i <= y } by WAYBEL_9:12; then consider k being Element of N such that A6: j = k and A7: i <= k by A3, A5; x = (N | i) . j by A4 .= N . k by A6, WAYBEL_9:16 ; hence x in X by A1, A2, A7, ORDERS_2:3; ::_thesis: verum end; theorem Th43: :: WAYBEL21:43 for T being complete Lawson TopLattice for N being eventually-filtered net of T holds rng the mapping of N is non empty filtered Subset of T proof let T be complete Lawson TopLattice; ::_thesis: for N being eventually-filtered net of T holds rng the mapping of N is non empty filtered Subset of T let N be eventually-filtered net of T; ::_thesis: rng the mapping of N is non empty filtered Subset of T reconsider F = rng the mapping of N as non empty Subset of T ; F is filtered proof let x, y be Element of T; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in F or not y in F or ex b1 being Element of the carrier of T st ( b1 in F & b1 <= x & b1 <= y ) ) assume x in F ; ::_thesis: ( not y in F or ex b1 being Element of the carrier of T st ( b1 in F & b1 <= x & b1 <= y ) ) then consider i1 being set such that A1: i1 in dom the mapping of N and A2: x = the mapping of N . i1 by FUNCT_1:def_3; assume y in F ; ::_thesis: ex b1 being Element of the carrier of T st ( b1 in F & b1 <= x & b1 <= y ) then consider i2 being set such that A3: i2 in dom the mapping of N and A4: y = the mapping of N . i2 by FUNCT_1:def_3; A5: dom the mapping of N = the carrier of N by FUNCT_2:def_1; reconsider i1 = i1, i2 = i2 as Element of N by A1, A3; consider j1 being Element of N such that A6: for k being Element of N st j1 <= k holds N . i1 >= N . k by WAYBEL_0:12; consider j2 being Element of N such that A7: for k being Element of N st j2 <= k holds N . i2 >= N . k by WAYBEL_0:12; consider j being Element of N such that A8: j2 <= j and A9: j1 <= j by YELLOW_6:def_3; take z = N . j; ::_thesis: ( z in F & z <= x & z <= y ) thus z in F by A5, FUNCT_1:def_3; ::_thesis: ( z <= x & z <= y ) thus ( z <= x & z <= y ) by A2, A4, A6, A7, A8, A9; ::_thesis: verum end; hence rng the mapping of N is non empty filtered Subset of T ; ::_thesis: verum end; theorem Th44: :: WAYBEL21:44 for T being complete Lawson TopLattice for N being eventually-filtered net of T holds Lim N = {(inf N)} proof let T be complete Lawson TopLattice; ::_thesis: for N being eventually-filtered net of T holds Lim N = {(inf N)} set S = the Scott TopAugmentation of T; let N be eventually-filtered net of T; ::_thesis: Lim N = {(inf N)} reconsider F = rng the mapping of N as non empty filtered Subset of T by Th43; A1: the topology of the Scott TopAugmentation of T = sigma T by YELLOW_9:51; A2: RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4; A3: inf N = Inf by WAYBEL_9:def_2 .= "/\" (F,T) by YELLOW_2:def_6 ; A4: dom the mapping of N = the carrier of N by FUNCT_2:def_1; thus Lim N c= {(inf N)} :: according to XBOOLE_0:def_10 ::_thesis: {(inf N)} c= Lim N proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in Lim N or p in {(inf N)} ) assume A5: p in Lim N ; ::_thesis: p in {(inf N)} then reconsider p = p as Element of T ; p is_<=_than F proof let u be Element of T; :: according to LATTICE3:def_8 ::_thesis: ( not u in F or p <= u ) assume u in F ; ::_thesis: p <= u then consider i being set such that A6: i in dom the mapping of N and A7: u = the mapping of N . i by FUNCT_1:def_3; reconsider i = i as Element of N by A6; consider ii being Element of N such that A8: for k being Element of N st ii <= k holds N . i >= N . k by WAYBEL_0:12; downarrow u is closed by WAYBEL19:38; then A9: Cl (downarrow u) = downarrow u by PRE_TOPC:22; N is_eventually_in downarrow u proof take ii ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds ( not ii <= b1 or N . b1 in downarrow u ) let j be Element of N; ::_thesis: ( not ii <= j or N . j in downarrow u ) assume j >= ii ; ::_thesis: N . j in downarrow u then N . j <= N . i by A8; hence N . j in downarrow u by A7, WAYBEL_0:17; ::_thesis: verum end; then Lim N c= downarrow u by A9, WAYBEL19:26; hence p <= u by A5, WAYBEL_0:17; ::_thesis: verum end; then A10: p <= inf N by A3, YELLOW_0:33; inf N is_<=_than F by A3, YELLOW_0:33; then A11: F c= uparrow (inf N) by YELLOW_2:2; uparrow (inf N) is closed by WAYBEL19:38; then Cl (uparrow (inf N)) = uparrow (inf N) by PRE_TOPC:22; then A12: Cl F c= uparrow (inf N) by A11, PRE_TOPC:19; p in Cl F by A5, WAYBEL_9:24; then p >= inf N by A12, WAYBEL_0:18; then p = inf N by A10, ORDERS_2:2; hence p in {(inf N)} by TARSKI:def_1; ::_thesis: verum end; reconsider K = (sigma T) \/ { ((uparrow x) `) where x is Element of T : verum } as prebasis of T by WAYBEL19:30; now__::_thesis:_for_A_being_Subset_of_T_st_inf_F_in_A_&_A_in_K_holds_ N_is_eventually_in_A let A be Subset of T; ::_thesis: ( inf F in A & A in K implies N is_eventually_in b1 ) assume that A13: inf F in A and A14: A in K ; ::_thesis: N is_eventually_in b1 percases ( A in sigma T or A in { ((uparrow x) `) where x is Element of T : verum } ) by A14, XBOOLE_0:def_3; supposeA15: A in sigma T ; ::_thesis: N is_eventually_in b1 then reconsider a = A as Subset of the Scott TopAugmentation of T by A1; a is open by A1, A15, PRE_TOPC:def_2; then a is upper by WAYBEL11:def_4; then A16: A is upper by A2, WAYBEL_0:25; set i = the Element of N; thus N is_eventually_in A ::_thesis: verum proof take the Element of N ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds ( not the Element of N <= b1 or N . b1 in A ) let j be Element of N; ::_thesis: ( not the Element of N <= j or N . j in A ) N . j in F by A4, FUNCT_1:def_3; then N . j >= inf F by YELLOW_2:22; hence ( not the Element of N <= j or N . j in A ) by A13, A16, WAYBEL_0:def_20; ::_thesis: verum end; end; suppose A in { ((uparrow x) `) where x is Element of T : verum } ; ::_thesis: N is_eventually_in b1 then consider x being Element of T such that A17: A = (uparrow x) ` ; not inf F >= x by A13, A17, YELLOW_9:1; then not F is_>=_than x by YELLOW_0:33; then consider y being Element of T such that A18: y in F and A19: not y >= x by LATTICE3:def_8; consider i being set such that A20: i in the carrier of N and A21: y = the mapping of N . i by A4, A18, FUNCT_1:def_3; thus N is_eventually_in A ::_thesis: verum proof reconsider i = i as Element of N by A20; consider ii being Element of N such that A22: for k being Element of N st ii <= k holds N . i >= N . k by WAYBEL_0:12; take ii ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds ( not ii <= b1 or N . b1 in A ) let j be Element of N; ::_thesis: ( not ii <= j or N . j in A ) assume j >= ii ; ::_thesis: N . j in A then N . j <= N . i by A22; then not N . j >= x by A19, A21, ORDERS_2:3; hence N . j in A by A17, YELLOW_9:1; ::_thesis: verum end; end; end; end; then inf F in Lim N by WAYBEL19:25; hence {(inf N)} c= Lim N by A3, ZFMISC_1:31; ::_thesis: verum end; begin theorem Th45: :: WAYBEL21:45 for S, T being complete Lawson TopLattice for f being meet-preserving Function of S,T holds ( f is continuous iff ( f is directed-sups-preserving & ( for X being non empty Subset of S holds f preserves_inf_of X ) ) ) proof let S, T be complete Lawson TopLattice; ::_thesis: for f being meet-preserving Function of S,T holds ( f is continuous iff ( f is directed-sups-preserving & ( for X being non empty Subset of S holds f preserves_inf_of X ) ) ) A1: [#] T <> {} ; set Ss = the Scott TopAugmentation of S; set Ts = the Scott TopAugmentation of T; set Sl = the correct lower TopAugmentation of S; set Tl = the correct lower TopAugmentation of T; A2: S is TopAugmentation of S by YELLOW_9:44; A3: T is TopAugmentation of T by YELLOW_9:44; A4: S is Refinement of the Scott TopAugmentation of S, the correct lower TopAugmentation of S by A2, WAYBEL19:29; A5: T is Refinement of the Scott TopAugmentation of T, the correct lower TopAugmentation of T by A3, WAYBEL19:29; A6: T is TopAugmentation of the Scott TopAugmentation of T by YELLOW_9:45; A7: S is TopAugmentation of the Scott TopAugmentation of S by YELLOW_9:45; A8: RelStr(# the carrier of the Scott TopAugmentation of S, the InternalRel of the Scott TopAugmentation of S #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4; A9: RelStr(# the carrier of the correct lower TopAugmentation of S, the InternalRel of the correct lower TopAugmentation of S #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4; A10: RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4; A11: RelStr(# the carrier of the correct lower TopAugmentation of T, the InternalRel of the correct lower TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4; let f be meet-preserving Function of S,T; ::_thesis: ( f is continuous iff ( f is directed-sups-preserving & ( for X being non empty Subset of S holds f preserves_inf_of X ) ) ) reconsider g = f as Function of the correct lower TopAugmentation of S, the correct lower TopAugmentation of T by A9, A11; reconsider h = f as Function of the Scott TopAugmentation of S, the Scott TopAugmentation of T by A8, A10; A12: [#] the Scott TopAugmentation of T <> {} ; hereby ::_thesis: ( f is directed-sups-preserving & ( for X being non empty Subset of S holds f preserves_inf_of X ) implies f is continuous ) assume A13: f is continuous ; ::_thesis: ( f is directed-sups-preserving & ( for X being non empty Subset of S holds f preserves_inf_of X ) ) now__::_thesis:_for_P_being_Subset_of_the_Scott_TopAugmentation_of_T_st_P_is_open_holds_ h_"_P_is_open let P be Subset of the Scott TopAugmentation of T; ::_thesis: ( P is open implies h " P is open ) reconsider A = P as Subset of the Scott TopAugmentation of T ; reconsider C = A as Subset of T by A10; assume A14: P is open ; ::_thesis: h " P is open then C is open by A6, WAYBEL19:37; then A15: f " C is open by A1, A13, TOPS_2:43; A is upper by A14, WAYBEL11:def_4; then h " A is upper by A8, A10, WAYBEL17:2, WAYBEL_9:1; then f " C is upper by A8, WAYBEL_0:25; hence h " P is open by A7, A15, WAYBEL19:41; ::_thesis: verum end; then h is continuous by A12, TOPS_2:43; hence f is directed-sups-preserving by A8, A10, Th6; ::_thesis: for X being non empty Subset of S holds f preserves_inf_of X for X being non empty filtered Subset of S holds f preserves_inf_of X proof let F be non empty filtered Subset of S; ::_thesis: f preserves_inf_of F assume ex_inf_of F,S ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of f .: F,T & "/\" ((f .: F),T) = f . ("/\" (F,S)) ) thus ex_inf_of f .: F,T by YELLOW_0:17; ::_thesis: "/\" ((f .: F),T) = f . ("/\" (F,S)) {(inf F)} = Lim (F opp+id) by WAYBEL19:43; then Im (f,(inf F)) c= Lim (f * (F opp+id)) by A13, Th24; then {(f . (inf F))} c= Lim (f * (F opp+id)) by SETWISEO:8; then A16: f . (inf F) in Lim (f * (F opp+id)) by ZFMISC_1:31; reconsider G = f .: F as non empty filtered Subset of T by WAYBEL20:24; A17: rng the mapping of (f * (F opp+id)) = rng (f * the mapping of (F opp+id)) by WAYBEL_9:def_8 .= rng (f * (id F)) by WAYBEL19:27 .= rng (f | F) by RELAT_1:65 .= G by RELAT_1:115 ; Lim (f * (F opp+id)) = {(inf (f * (F opp+id)))} by Th44 .= {(Inf )} by WAYBEL_9:def_2 .= {(inf G)} by A17, YELLOW_2:def_6 ; hence "/\" ((f .: F),T) = f . ("/\" (F,S)) by A16, TARSKI:def_1; ::_thesis: verum end; hence for X being non empty Subset of S holds f preserves_inf_of X by Th4; ::_thesis: verum end; assume f is directed-sups-preserving ; ::_thesis: ( ex X being non empty Subset of S st not f preserves_inf_of X or f is continuous ) then A18: h is directed-sups-preserving by A8, A10, Th6; assume for X being non empty Subset of S holds f preserves_inf_of X ; ::_thesis: f is continuous then for X being non empty Subset of the correct lower TopAugmentation of S holds g preserves_inf_of X by A9, A11, WAYBEL_0:65; then g is continuous by WAYBEL19:8; hence f is continuous by A4, A5, A18, WAYBEL19:24; ::_thesis: verum end; theorem Th46: :: WAYBEL21:46 for S, T being complete Lawson TopLattice for f being SemilatticeHomomorphism of S,T holds ( f is continuous iff ( f is infs-preserving & f is directed-sups-preserving ) ) proof let S, T be complete Lawson TopLattice; ::_thesis: for f being SemilatticeHomomorphism of S,T holds ( f is continuous iff ( f is infs-preserving & f is directed-sups-preserving ) ) let f be SemilatticeHomomorphism of S,T; ::_thesis: ( f is continuous iff ( f is infs-preserving & f is directed-sups-preserving ) ) hereby ::_thesis: ( f is infs-preserving & f is directed-sups-preserving implies f is continuous ) assume A1: f is continuous ; ::_thesis: ( f is infs-preserving & f is directed-sups-preserving ) A2: for X being finite Subset of S holds f preserves_inf_of X by Def1; for X being non empty filtered Subset of S holds f preserves_inf_of X by A1, Th45; hence f is infs-preserving by A2, WAYBEL_0:71; ::_thesis: f is directed-sups-preserving thus f is directed-sups-preserving by A1, Th45; ::_thesis: verum end; assume f is infs-preserving ; ::_thesis: ( not f is directed-sups-preserving or f is continuous ) then for X being non empty Subset of S holds f preserves_inf_of X by WAYBEL_0:def_32; hence ( not f is directed-sups-preserving or f is continuous ) by Th45; ::_thesis: verum end; definition let S, T be non empty RelStr ; let f be Function of S,T; attrf is lim_infs-preserving means :: WAYBEL21:def 4 for N being net of S holds f . (lim_inf N) = lim_inf (f * N); end; :: deftheorem defines lim_infs-preserving WAYBEL21:def_4_:_ for S, T being non empty RelStr for f being Function of S,T holds ( f is lim_infs-preserving iff for N being net of S holds f . (lim_inf N) = lim_inf (f * N) ); theorem :: WAYBEL21:47 for S, T being complete Lawson TopLattice for f being SemilatticeHomomorphism of S,T holds ( f is continuous iff f is lim_infs-preserving ) proof let S, T be complete Lawson TopLattice; ::_thesis: for f being SemilatticeHomomorphism of S,T holds ( f is continuous iff f is lim_infs-preserving ) let f be SemilatticeHomomorphism of S,T; ::_thesis: ( f is continuous iff f is lim_infs-preserving ) thus ( f is continuous implies f is lim_infs-preserving ) ::_thesis: ( f is lim_infs-preserving implies f is continuous ) proof assume f is continuous ; ::_thesis: f is lim_infs-preserving then A1: ( f is infs-preserving & f is directed-sups-preserving ) by Th46; let N be net of S; :: according to WAYBEL21:def_4 ::_thesis: f . (lim_inf N) = lim_inf (f * N) set M = f * N; set Y = { ("/\" ( { ((f * N) . i) where i is Element of (f * N) : i >= j } ,T)) where j is Element of (f * N) : verum } ; reconsider X = { ("/\" ( { (N . i) where i is Element of N : i >= j } ,S)) where j is Element of N : verum } as non empty directed Subset of S by Th25; A2: ex_sup_of X,S by YELLOW_0:17; A3: f preserves_sup_of X by A1, WAYBEL_0:def_37; A4: RelStr(# the carrier of (f * N), the InternalRel of (f * N) #) = RelStr(# the carrier of N, the InternalRel of N #) by WAYBEL_9:def_8; A5: the carrier of S c= dom f by FUNCT_2:def_1; deffunc H1( Element of N) -> set = { (N . i) where i is Element of N : i >= \$1 } ; deffunc H2( Element of N) -> Element of the carrier of S = "/\" (H1(\$1),S); defpred S1[ set ] means verum; A6: f .: { H2(i) where i is Element of N : S1[i] } = { (f . H2(i)) where i is Element of N : S1[i] } from LATTICE3:sch_2(A5); A7: f .: X = { ("/\" ( { ((f * N) . i) where i is Element of (f * N) : i >= j } ,T)) where j is Element of (f * N) : verum } proof A8: now__::_thesis:_for_j_being_Element_of_N for_j9_being_Element_of_(f_*_N)_st_j9_=_j_holds_ f_.:_H1(j)_=__{__((f_*_N)_._n)_where_n_is_Element_of_(f_*_N)_:_n_>=_j9__}_ let j be Element of N; ::_thesis: for j9 being Element of (f * N) st j9 = j holds f .: H1(j) = { ((f * N) . n) where n is Element of (f * N) : n >= j9 } let j9 be Element of (f * N); ::_thesis: ( j9 = j implies f .: H1(j) = { ((f * N) . n) where n is Element of (f * N) : n >= j9 } ) assume A9: j9 = j ; ::_thesis: f .: H1(j) = { ((f * N) . n) where n is Element of (f * N) : n >= j9 } defpred S2[ Element of N] means \$1 >= j; defpred S3[ Element of (f * N)] means \$1 >= j9; deffunc H3( Element of N) -> Element of the carrier of T = f . (N . \$1); deffunc H4( set ) -> set = f . ( the mapping of N . \$1); A10: for v being Element of N st S2[v] holds H3(v) = H4(v) ; deffunc H5( set ) -> set = (f * the mapping of N) . \$1; deffunc H6( Element of (f * N)) -> Element of the carrier of T = (f * N) . \$1; A11: for v being Element of N st S2[v] holds H4(v) = H5(v) by FUNCT_2:15; A12: for v being Element of (f * N) st S3[v] holds H5(v) = H6(v) by WAYBEL_9:def_8; defpred S4[ set ] means [j9,\$1] in the InternalRel of N; A13: for v being Element of N holds ( S2[v] iff S4[v] ) by A9, ORDERS_2:def_5; A14: for v being Element of (f * N) holds ( S4[v] iff S3[v] ) by A4, ORDERS_2:def_5; deffunc H7( Element of N) -> Element of the carrier of S = N . \$1; thus f .: H1(j) = f .: { H7(i) where i is Element of N : S2[i] } .= { (f . H7(k)) where k is Element of N : S2[k] } from LATTICE3:sch_2(A5) .= { H3(k) where k is Element of N : S2[k] } .= { H4(s) where s is Element of N : S2[s] } from FRAENKEL:sch_6(A10) .= { H5(o) where o is Element of N : S2[o] } from FRAENKEL:sch_6(A11) .= { H5(r) where r is Element of N : S4[r] } from FRAENKEL:sch_3(A13) .= { H5(m) where m is Element of (f * N) : S4[m] } by A4 .= { H5(q) where q is Element of (f * N) : S3[q] } from FRAENKEL:sch_3(A14) .= { H6(n) where n is Element of (f * N) : S3[n] } from FRAENKEL:sch_6(A12) .= { ((f * N) . n) where n is Element of (f * N) : n >= j9 } ; ::_thesis: verum end; A15: now__::_thesis:_for_j_being_Element_of_N_holds_f_._("/\"_(H1(j),S))_=_"/\"_((f_.:_H1(j)),T) let j be Element of N; ::_thesis: f . ("/\" (H1(j),S)) = "/\" ((f .: H1(j)),T) H1(j) c= the carrier of S proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in H1(j) or b in the carrier of S ) assume b in H1(j) ; ::_thesis: b in the carrier of S then ex i being Element of N st ( b = N . i & i >= j ) ; hence b in the carrier of S ; ::_thesis: verum end; then reconsider A = H1(j) as Subset of S ; A16: f preserves_inf_of A by A1, WAYBEL_0:def_32; ex_inf_of A,S by YELLOW_0:17; hence f . ("/\" (H1(j),S)) = "/\" ((f .: H1(j)),T) by A16, WAYBEL_0:def_30; ::_thesis: verum end; thus f .: X c= { ("/\" ( { ((f * N) . i) where i is Element of (f * N) : i >= j } ,T)) where j is Element of (f * N) : verum } :: according to XBOOLE_0:def_10 ::_thesis: { ("/\" ( { ((f * N) . i) where i is Element of (f * N) : i >= j } ,T)) where j is Element of (f * N) : verum } c= f .: X proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in f .: X or a in { ("/\" ( { ((f * N) . i) where i is Element of (f * N) : i >= j } ,T)) where j is Element of (f * N) : verum } ) assume a in f .: X ; ::_thesis: a in { ("/\" ( { ((f * N) . i) where i is Element of (f * N) : i >= j } ,T)) where j is Element of (f * N) : verum } then consider j being Element of N such that A17: a = f . ("/\" ( { (N . i) where i is Element of N : i >= j } ,S)) by A6; A18: a = "/\" ((f .: H1(j)),T) by A15, A17; reconsider j9 = j as Element of (f * N) by A4; f .: H1(j) = { ((f * N) . n) where n is Element of (f * N) : n >= j9 } by A8; hence a in { ("/\" ( { ((f * N) . i) where i is Element of (f * N) : i >= j } ,T)) where j is Element of (f * N) : verum } by A18; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ("/\" ( { ((f * N) . i) where i is Element of (f * N) : i >= j } ,T)) where j is Element of (f * N) : verum } or a in f .: X ) assume a in { ("/\" ( { ((f * N) . i) where i is Element of (f * N) : i >= j } ,T)) where j is Element of (f * N) : verum } ; ::_thesis: a in f .: X then consider j9 being Element of (f * N) such that A19: a = "/\" ( { ((f * N) . n) where n is Element of (f * N) : n >= j9 } ,T) ; reconsider j = j9 as Element of N by A4; a = "/\" ((f .: H1(j)),T) by A8, A19 .= f . ("/\" (H1(j),S)) by A15 ; hence a in f .: X by A6; ::_thesis: verum end; thus f . (lim_inf N) = f . (sup X) by WAYBEL11:def_6 .= sup (f .: X) by A2, A3, WAYBEL_0:def_31 .= lim_inf (f * N) by A7, WAYBEL11:def_6 ; ::_thesis: verum end; assume A20: for N being net of S holds f . (lim_inf N) = lim_inf (f * N) ; :: according to WAYBEL21:def_4 ::_thesis: f is continuous A21: f is directed-sups-preserving proof let D be Subset of S; :: according to WAYBEL_0:def_37 ::_thesis: ( D is empty or not D is directed or f preserves_sup_of D ) assume ( not D is empty & D is directed ) ; ::_thesis: f preserves_sup_of D then reconsider D9 = D as non empty directed Subset of S ; assume ex_sup_of D,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of f .: D,T & "\/" ((f .: D),T) = f . ("\/" (D,S)) ) thus ex_sup_of f .: D,T by YELLOW_0:17; ::_thesis: "\/" ((f .: D),T) = f . ("\/" (D,S)) thus f . (sup D) = f . (lim_inf (Net-Str D9)) by WAYBEL17:10 .= lim_inf (f * (Net-Str D9)) by A20 .= sup (f .: D) by Th33 ; ::_thesis: verum end; A22: for X being finite Subset of S holds f preserves_inf_of X by Def1; now__::_thesis:_for_X_being_non_empty_filtered_Subset_of_S_holds_f_preserves_inf_of_X let X be non empty filtered Subset of S; ::_thesis: f preserves_inf_of X reconsider fX = f .: X as non empty filtered Subset of T by WAYBEL20:24; thus f preserves_inf_of X ::_thesis: verum proof assume ex_inf_of X,S ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of f .: X,T & "/\" ((f .: X),T) = f . ("/\" (X,S)) ) thus ex_inf_of f .: X,T by YELLOW_0:17; ::_thesis: "/\" ((f .: X),T) = f . ("/\" (X,S)) f . (inf X) = f . (lim_inf (X opp+id)) by Th28 .= lim_inf (f * (X opp+id)) by A20 .= inf fX by Th29 .= lim_inf (fX opp+id) by Th28 ; hence "/\" ((f .: X),T) = f . ("/\" (X,S)) by Th28; ::_thesis: verum end; end; then f is infs-preserving by A22, WAYBEL_0:71; hence f is continuous by A21, Th46; ::_thesis: verum end; theorem Th48: :: WAYBEL21:48 for T being continuous complete Lawson TopLattice for S being non empty full meet-inheriting SubRelStr of T st Top T in the carrier of S & ex X being Subset of T st ( X = the carrier of S & X is closed ) holds S is infs-inheriting proof let T be continuous complete Lawson TopLattice; ::_thesis: for S being non empty full meet-inheriting SubRelStr of T st Top T in the carrier of S & ex X being Subset of T st ( X = the carrier of S & X is closed ) holds S is infs-inheriting let S be non empty full meet-inheriting SubRelStr of T; ::_thesis: ( Top T in the carrier of S & ex X being Subset of T st ( X = the carrier of S & X is closed ) implies S is infs-inheriting ) assume A1: Top T in the carrier of S ; ::_thesis: ( for X being Subset of T holds ( not X = the carrier of S or not X is closed ) or S is infs-inheriting ) given X being Subset of T such that A2: X = the carrier of S and A3: X is closed ; ::_thesis: S is infs-inheriting S is filtered-infs-inheriting proof let Y be filtered Subset of S; :: according to WAYBEL_0:def_3 ::_thesis: ( Y = {} or not ex_inf_of Y,T or "/\" (Y,T) in the carrier of S ) assume Y <> {} ; ::_thesis: ( not ex_inf_of Y,T or "/\" (Y,T) in the carrier of S ) then reconsider F = Y as non empty filtered Subset of T by YELLOW_2:7; set N = F opp+id ; assume ex_inf_of Y,T ; ::_thesis: "/\" (Y,T) in the carrier of S the mapping of (F opp+id) = id Y by WAYBEL19:27; then A4: rng the mapping of (F opp+id) = Y by RELAT_1:45; Lim (F opp+id) = {(inf F)} by WAYBEL19:43; then {(inf F)} c= Cl X by A2, A4, Th27, WAYBEL19:26; then {(inf F)} c= X by A3, PRE_TOPC:22; hence "/\" (Y,T) in the carrier of S by A2, ZFMISC_1:31; ::_thesis: verum end; hence S is infs-inheriting by A1, Th16; ::_thesis: verum end; theorem Th49: :: WAYBEL21:49 for T being continuous complete Lawson TopLattice for S being non empty full SubRelStr of T st ex X being Subset of T st ( X = the carrier of S & X is closed ) holds S is directed-sups-inheriting proof let T be continuous complete Lawson TopLattice; ::_thesis: for S being non empty full SubRelStr of T st ex X being Subset of T st ( X = the carrier of S & X is closed ) holds S is directed-sups-inheriting let S be non empty full SubRelStr of T; ::_thesis: ( ex X being Subset of T st ( X = the carrier of S & X is closed ) implies S is directed-sups-inheriting ) given X being Subset of T such that A1: X = the carrier of S and A2: X is closed ; ::_thesis: S is directed-sups-inheriting let Y be directed Subset of S; :: according to WAYBEL_0:def_4 ::_thesis: ( Y = {} or not ex_sup_of Y,T or "\/" (Y,T) in the carrier of S ) assume Y <> {} ; ::_thesis: ( not ex_sup_of Y,T or "\/" (Y,T) in the carrier of S ) then reconsider D = Y as non empty directed Subset of T by YELLOW_2:7; set N = Net-Str D; assume ex_sup_of Y,T ; ::_thesis: "\/" (Y,T) in the carrier of S the mapping of (Net-Str D) = id Y by Th32; then rng the mapping of (Net-Str D) = Y by RELAT_1:45; then Lim (Net-Str D) c= Cl X by A1, Th27, WAYBEL19:26; then A3: Lim (Net-Str D) c= X by A2, PRE_TOPC:22; sup D in Lim (Net-Str D) by Th35; hence "\/" (Y,T) in the carrier of S by A1, A3; ::_thesis: verum end; theorem Th50: :: WAYBEL21:50 for T being continuous complete Lawson TopLattice for S being non empty full infs-inheriting directed-sups-inheriting SubRelStr of T ex X being Subset of T st ( X = the carrier of S & X is closed ) proof let T be continuous complete Lawson TopLattice; ::_thesis: for S being non empty full infs-inheriting directed-sups-inheriting SubRelStr of T ex X being Subset of T st ( X = the carrier of S & X is closed ) let S be non empty full infs-inheriting directed-sups-inheriting SubRelStr of T; ::_thesis: ex X being Subset of T st ( X = the carrier of S & X is closed ) reconsider X = the carrier of S as Subset of T by YELLOW_0:def_13; take X ; ::_thesis: ( X = the carrier of S & X is closed ) thus X = the carrier of S ; ::_thesis: X is closed reconsider S = S as complete CLSubFrame of T by Th18; set SL = the correct Lawson TopAugmentation of S; A1: RelStr(# the carrier of the correct Lawson TopAugmentation of S, the InternalRel of the correct Lawson TopAugmentation of S #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4; set f = incl ( the correct Lawson TopAugmentation of S,T); set f9 = incl (S,T); A2: the carrier of S c= the carrier of T by YELLOW_0:def_13; then A3: incl ( the correct Lawson TopAugmentation of S,T) = id the carrier of the correct Lawson TopAugmentation of S by A1, YELLOW_9:def_1; A4: incl (S,T) = id the carrier of the correct Lawson TopAugmentation of S by A1, A2, YELLOW_9:def_1; A5: [#] the correct Lawson TopAugmentation of S is compact by COMPTS_1:1; A6: incl (S,T) is infs-preserving by Th8; RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of T, the InternalRel of T #) ; then A7: ( incl ( the correct Lawson TopAugmentation of S,T) is infs-preserving & incl ( the correct Lawson TopAugmentation of S,T) is directed-sups-preserving ) by A1, A3, A4, A6, Th6, Th10; then incl ( the correct Lawson TopAugmentation of S,T) is SemilatticeHomomorphism of the correct Lawson TopAugmentation of S,T by Th5; then incl ( the correct Lawson TopAugmentation of S,T) is continuous by A7, Th46; then (incl ( the correct Lawson TopAugmentation of S,T)) .: ([#] the correct Lawson TopAugmentation of S) is compact by A5, WEIERSTR:8; then X is compact by A1, A3, FUNCT_1:92; hence X is closed by COMPTS_1:7; ::_thesis: verum end; theorem Th51: :: WAYBEL21:51 for T being continuous complete Lawson TopLattice for S being non empty full infs-inheriting directed-sups-inheriting SubRelStr of T for N being net of T st N is_eventually_in the carrier of S holds lim_inf N in the carrier of S proof let T be continuous complete Lawson TopLattice; ::_thesis: for S being non empty full infs-inheriting directed-sups-inheriting SubRelStr of T for N being net of T st N is_eventually_in the carrier of S holds lim_inf N in the carrier of S let S be non empty full infs-inheriting directed-sups-inheriting SubRelStr of T; ::_thesis: for N being net of T st N is_eventually_in the carrier of S holds lim_inf N in the carrier of S set X = the carrier of S; let N be net of T; ::_thesis: ( N is_eventually_in the carrier of S implies lim_inf N in the carrier of S ) assume N is_eventually_in the carrier of S ; ::_thesis: lim_inf N in the carrier of S then consider a being Element of N such that N . a in the carrier of S and A1: rng the mapping of (N | a) c= the carrier of S by Th42; deffunc H1( Element of (N | a)) -> set = { ((N | a) . i) where i is Element of (N | a) : i >= \$1 } ; reconsider iN = { ("/\" (H1(j),T)) where j is Element of (N | a) : verum } as non empty directed Subset of T by Th25; iN c= the carrier of S proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in iN or z in the carrier of S ) assume z in iN ; ::_thesis: z in the carrier of S then consider j being Element of (N | a) such that A2: z = "/\" (H1(j),T) ; H1(j) c= the carrier of S proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in H1(j) or u in the carrier of S ) assume u in H1(j) ; ::_thesis: u in the carrier of S then ex i being Element of (N | a) st ( u = (N | a) . i & i >= j ) ; then u in rng the mapping of (N | a) by FUNCT_2:4; hence u in the carrier of S by A1; ::_thesis: verum end; then reconsider Xj = H1(j) as Subset of S ; ex_inf_of Xj,T by YELLOW_0:17; hence z in the carrier of S by A2, YELLOW_0:def_18; ::_thesis: verum end; then reconsider jN = iN as non empty Subset of S ; A3: jN is directed by WAYBEL10:23; ex_sup_of jN,T by YELLOW_0:17; then "\/" (jN,T) in the carrier of S by A3, WAYBEL_0:def_4; then lim_inf (N | a) in the carrier of S by WAYBEL11:def_6; hence lim_inf N in the carrier of S by Th41; ::_thesis: verum end; theorem Th52: :: WAYBEL21:52 for T being continuous complete Lawson TopLattice for S being non empty full meet-inheriting SubRelStr of T st Top T in the carrier of S & ( for N being net of T st rng the mapping of N c= the carrier of S holds lim_inf N in the carrier of S ) holds S is infs-inheriting proof let T be continuous complete Lawson TopLattice; ::_thesis: for S being non empty full meet-inheriting SubRelStr of T st Top T in the carrier of S & ( for N being net of T st rng the mapping of N c= the carrier of S holds lim_inf N in the carrier of S ) holds S is infs-inheriting let S be non empty full meet-inheriting SubRelStr of T; ::_thesis: ( Top T in the carrier of S & ( for N being net of T st rng the mapping of N c= the carrier of S holds lim_inf N in the carrier of S ) implies S is infs-inheriting ) assume A1: Top T in the carrier of S ; ::_thesis: ( ex N being net of T st ( rng the mapping of N c= the carrier of S & not lim_inf N in the carrier of S ) or S is infs-inheriting ) set X = the carrier of S; assume A2: for N being net of T st rng the mapping of N c= the carrier of S holds lim_inf N in the carrier of S ; ::_thesis: S is infs-inheriting S is filtered-infs-inheriting proof let Y be filtered Subset of S; :: according to WAYBEL_0:def_3 ::_thesis: ( Y = {} or not ex_inf_of Y,T or "/\" (Y,T) in the carrier of S ) assume Y <> {} ; ::_thesis: ( not ex_inf_of Y,T or "/\" (Y,T) in the carrier of S ) then reconsider F = Y as non empty filtered Subset of T by YELLOW_2:7; assume ex_inf_of Y,T ; ::_thesis: "/\" (Y,T) in the carrier of S the mapping of (F opp+id) = id F by WAYBEL19:27; then A3: rng the mapping of (F opp+id) = Y by RELAT_1:45; lim_inf (F opp+id) = inf F by Th28; hence "/\" (Y,T) in the carrier of S by A2, A3; ::_thesis: verum end; hence S is infs-inheriting by A1, Th16; ::_thesis: verum end; theorem Th53: :: WAYBEL21:53 for T being continuous complete Lawson TopLattice for S being non empty full SubRelStr of T st ( for N being net of T st rng the mapping of N c= the carrier of S holds lim_inf N in the carrier of S ) holds S is directed-sups-inheriting proof let T be continuous complete Lawson TopLattice; ::_thesis: for S being non empty full SubRelStr of T st ( for N being net of T st rng the mapping of N c= the carrier of S holds lim_inf N in the carrier of S ) holds S is directed-sups-inheriting let S be non empty full SubRelStr of T; ::_thesis: ( ( for N being net of T st rng the mapping of N c= the carrier of S holds lim_inf N in the carrier of S ) implies S is directed-sups-inheriting ) set X = the carrier of S; assume A1: for N being net of T st rng the mapping of N c= the carrier of S holds lim_inf N in the carrier of S ; ::_thesis: S is directed-sups-inheriting let Y be directed Subset of S; :: according to WAYBEL_0:def_4 ::_thesis: ( Y = {} or not ex_sup_of Y,T or "\/" (Y,T) in the carrier of S ) assume Y <> {} ; ::_thesis: ( not ex_sup_of Y,T or "\/" (Y,T) in the carrier of S ) then reconsider F = Y as non empty directed Subset of T by YELLOW_2:7; assume ex_sup_of Y,T ; ::_thesis: "\/" (Y,T) in the carrier of S the mapping of (Net-Str F) = id F by Th32; then A2: rng the mapping of (Net-Str F) = Y by RELAT_1:45; lim_inf (Net-Str F) = sup F by WAYBEL17:10; hence "\/" (Y,T) in the carrier of S by A1, A2; ::_thesis: verum end; theorem :: WAYBEL21:54 for T being continuous complete Lawson TopLattice for S being non empty full meet-inheriting SubRelStr of T for X being Subset of T st X = the carrier of S & Top T in X holds ( X is closed iff for N being net of T st N is_eventually_in X holds lim_inf N in X ) proof let T be continuous complete Lawson TopLattice; ::_thesis: for S being non empty full meet-inheriting SubRelStr of T for X being Subset of T st X = the carrier of S & Top T in X holds ( X is closed iff for N being net of T st N is_eventually_in X holds lim_inf N in X ) let S be non empty full meet-inheriting SubRelStr of T; ::_thesis: for X being Subset of T st X = the carrier of S & Top T in X holds ( X is closed iff for N being net of T st N is_eventually_in X holds lim_inf N in X ) let X be Subset of T; ::_thesis: ( X = the carrier of S & Top T in X implies ( X is closed iff for N being net of T st N is_eventually_in X holds lim_inf N in X ) ) assume that A1: X = the carrier of S and A2: Top T in X ; ::_thesis: ( X is closed iff for N being net of T st N is_eventually_in X holds lim_inf N in X ) hereby ::_thesis: ( ( for N being net of T st N is_eventually_in X holds lim_inf N in X ) implies X is closed ) assume X is closed ; ::_thesis: for N being net of T st N is_eventually_in X holds lim_inf N in X then S is non empty full infs-inheriting directed-sups-inheriting SubRelStr of T by A1, A2, Th48, Th49; hence for N being net of T st N is_eventually_in X holds lim_inf N in X by A1, Th51; ::_thesis: verum end; assume for N being net of T st N is_eventually_in X holds lim_inf N in X ; ::_thesis: X is closed then for N being net of T st rng the mapping of N c= the carrier of S holds lim_inf N in the carrier of S by A1, Th27; then ( S is infs-inheriting & S is directed-sups-inheriting ) by A1, A2, Th52, Th53; then ex X being Subset of T st ( X = the carrier of S & X is closed ) by Th50; hence X is closed by A1; ::_thesis: verum end;