:: Auxiliary and Approximating Relations :: by Adam Grabowski :: :: Received October 21, 1996 :: Copyright (c) 1996-2012 Association of Mizar Users begin definition let L be non empty reflexive RelStr ; funcL -waybelow -> Relation of L means :Def1: :: WAYBEL_4:def 1 for x, y being Element of L holds ( [x,y] in it iff x << y ); existence ex b1 being Relation of L st for x, y being Element of L holds ( [x,y] in b1 iff x << y ) proofend; uniqueness for b1, b2 being Relation of L st ( for x, y being Element of L holds ( [x,y] in b1 iff x << y ) ) & ( for x, y being Element of L holds ( [x,y] in b2 iff x << y ) ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines -waybelow WAYBEL_4:def_1_:_ for L being non empty reflexive RelStr for b2 being Relation of L holds ( b2 = L -waybelow iff for x, y being Element of L holds ( [x,y] in b2 iff x << y ) ); definition let L be RelStr ; func IntRel L -> Relation of L equals :: WAYBEL_4:def 2 the InternalRel of L; coherence the InternalRel of L is Relation of L ; correctness ; end; :: deftheorem defines IntRel WAYBEL_4:def_2_:_ for L being RelStr holds IntRel L = the InternalRel of L; definition let L be RelStr ; let R be Relation of L; attrR is auxiliary(i) means :Def3: :: WAYBEL_4:def 3 for x, y being Element of L st [x,y] in R holds x <= y; attrR is auxiliary(ii) means :Def4: :: WAYBEL_4:def 4 for x, y, z, u being Element of L st u <= x & [x,y] in R & y <= z holds [u,z] in R; end; :: deftheorem Def3 defines auxiliary(i) WAYBEL_4:def_3_:_ for L being RelStr for R being Relation of L holds ( R is auxiliary(i) iff for x, y being Element of L st [x,y] in R holds x <= y ); :: deftheorem Def4 defines auxiliary(ii) WAYBEL_4:def_4_:_ for L being RelStr for R being Relation of L holds ( R is auxiliary(ii) iff for x, y, z, u being Element of L st u <= x & [x,y] in R & y <= z holds [u,z] in R ); definition let L be non empty RelStr ; let R be Relation of L; attrR is auxiliary(iii) means :Def5: :: WAYBEL_4:def 5 for x, y, z being Element of L st [x,z] in R & [y,z] in R holds [(x "\/" y),z] in R; attrR is auxiliary(iv) means :Def6: :: WAYBEL_4:def 6 for x being Element of L holds [(Bottom L),x] in R; end; :: deftheorem Def5 defines auxiliary(iii) WAYBEL_4:def_5_:_ for L being non empty RelStr for R being Relation of L holds ( R is auxiliary(iii) iff for x, y, z being Element of L st [x,z] in R & [y,z] in R holds [(x "\/" y),z] in R ); :: deftheorem Def6 defines auxiliary(iv) WAYBEL_4:def_6_:_ for L being non empty RelStr for R being Relation of L holds ( R is auxiliary(iv) iff for x being Element of L holds [(Bottom L),x] in R ); :: Definition 1.9 p.43 definition let L be non empty RelStr ; let R be Relation of L; attrR is auxiliary means :Def7: :: WAYBEL_4:def 7 ( R is auxiliary(i) & R is auxiliary(ii) & R is auxiliary(iii) & R is auxiliary(iv) ); end; :: deftheorem Def7 defines auxiliary WAYBEL_4:def_7_:_ for L being non empty RelStr for R being Relation of L holds ( R is auxiliary iff ( R is auxiliary(i) & R is auxiliary(ii) & R is auxiliary(iii) & R is auxiliary(iv) ) ); registration let L be non empty RelStr ; cluster auxiliary -> auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) for Element of bool [: the carrier of L, the carrier of L:]; coherence for b1 being Relation of L st b1 is auxiliary holds ( b1 is auxiliary(i) & b1 is auxiliary(ii) & b1 is auxiliary(iii) & b1 is auxiliary(iv) ) by Def7; cluster auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) -> auxiliary for Element of bool [: the carrier of L, the carrier of L:]; coherence for b1 being Relation of L st b1 is auxiliary(i) & b1 is auxiliary(ii) & b1 is auxiliary(iii) & b1 is auxiliary(iv) holds b1 is auxiliary by Def7; end; registration let L be transitive antisymmetric lower-bounded with_suprema RelStr ; cluster Relation-like auxiliary for Element of bool [: the carrier of L, the carrier of L:]; existence ex b1 being Relation of L st b1 is auxiliary proofend; end; theorem Th1: :: WAYBEL_4:1 for L being lower-bounded sup-Semilattice for AR being auxiliary(ii) auxiliary(iii) Relation of L for x, y, z, u being Element of L st [x,z] in AR & [y,u] in AR holds [(x "\/" y),(z "\/" u)] in AR proofend; Lm1: for L being lower-bounded sup-Semilattice for AR being auxiliary(i) auxiliary(ii) Relation of L holds AR is transitive proofend; registration let L be lower-bounded sup-Semilattice; cluster auxiliary(i) auxiliary(ii) -> transitive for Element of bool [: the carrier of L, the carrier of L:]; coherence for b1 being Relation of L st b1 is auxiliary(i) & b1 is auxiliary(ii) holds b1 is transitive by Lm1; end; registration let L be RelStr ; cluster IntRel L -> auxiliary(i) ; coherence IntRel L is auxiliary(i) proofend; end; registration let L be transitive RelStr ; cluster IntRel L -> auxiliary(ii) ; coherence IntRel L is auxiliary(ii) proofend; end; registration let L be antisymmetric with_suprema RelStr ; cluster IntRel L -> auxiliary(iii) ; coherence IntRel L is auxiliary(iii) proofend; end; registration let L be non empty antisymmetric lower-bounded RelStr ; cluster IntRel L -> auxiliary(iv) ; coherence IntRel L is auxiliary(iv) proofend; end; definition let L be lower-bounded sup-Semilattice; func Aux L -> set means :Def8: :: WAYBEL_4:def 8 for a being set holds ( a in it iff a is auxiliary Relation of L ); existence ex b1 being set st for a being set holds ( a in b1 iff a is auxiliary Relation of L ) proofend; uniqueness for b1, b2 being set st ( for a being set holds ( a in b1 iff a is auxiliary Relation of L ) ) & ( for a being set holds ( a in b2 iff a is auxiliary Relation of L ) ) holds b1 = b2 proofend; end; :: deftheorem Def8 defines Aux WAYBEL_4:def_8_:_ for L being lower-bounded sup-Semilattice for b2 being set holds ( b2 = Aux L iff for a being set holds ( a in b2 iff a is auxiliary Relation of L ) ); registration let L be lower-bounded sup-Semilattice; cluster Aux L -> non empty ; coherence not Aux L is empty proofend; end; Lm2: for L being lower-bounded sup-Semilattice for AR being auxiliary(i) Relation of L for a, b being set st [a,b] in AR holds [a,b] in IntRel L proofend; theorem Th2: :: WAYBEL_4:2 for L being lower-bounded sup-Semilattice for AR being auxiliary(i) Relation of L holds AR c= IntRel L proofend; theorem :: WAYBEL_4:3 for L being lower-bounded sup-Semilattice holds Top (InclPoset (Aux L)) = IntRel L proofend; registration let L be lower-bounded sup-Semilattice; cluster InclPoset (Aux L) -> upper-bounded ; coherence InclPoset (Aux L) is upper-bounded proofend; end; definition let L be non empty RelStr ; func AuxBottom L -> Relation of L means :Def9: :: WAYBEL_4:def 9 for x, y being Element of L holds ( [x,y] in it iff x = Bottom L ); existence ex b1 being Relation of L st for x, y being Element of L holds ( [x,y] in b1 iff x = Bottom L ) proofend; uniqueness for b1, b2 being Relation of L st ( for x, y being Element of L holds ( [x,y] in b1 iff x = Bottom L ) ) & ( for x, y being Element of L holds ( [x,y] in b2 iff x = Bottom L ) ) holds b1 = b2 proofend; end; :: deftheorem Def9 defines AuxBottom WAYBEL_4:def_9_:_ for L being non empty RelStr for b2 being Relation of L holds ( b2 = AuxBottom L iff for x, y being Element of L holds ( [x,y] in b2 iff x = Bottom L ) ); registration let L be lower-bounded sup-Semilattice; cluster AuxBottom L -> auxiliary ; coherence AuxBottom L is auxiliary proofend; end; theorem Th4: :: WAYBEL_4:4 for L being lower-bounded sup-Semilattice for AR being auxiliary(iv) Relation of L holds AuxBottom L c= AR proofend; theorem :: WAYBEL_4:5 for L being lower-bounded sup-Semilattice holds Bottom (InclPoset (Aux L)) = AuxBottom L proofend; registration let L be lower-bounded sup-Semilattice; cluster InclPoset (Aux L) -> lower-bounded ; coherence InclPoset (Aux L) is lower-bounded proofend; end; theorem Th6: :: WAYBEL_4:6 for L being lower-bounded sup-Semilattice for a, b being auxiliary(i) Relation of L holds a /\ b is auxiliary(i) Relation of L proofend; theorem Th7: :: WAYBEL_4:7 for L being lower-bounded sup-Semilattice for a, b being auxiliary(ii) Relation of L holds a /\ b is auxiliary(ii) Relation of L proofend; theorem Th8: :: WAYBEL_4:8 for L being lower-bounded sup-Semilattice for a, b being auxiliary(iii) Relation of L holds a /\ b is auxiliary(iii) Relation of L proofend; theorem Th9: :: WAYBEL_4:9 for L being lower-bounded sup-Semilattice for a, b being auxiliary(iv) Relation of L holds a /\ b is auxiliary(iv) Relation of L proofend; theorem Th10: :: WAYBEL_4:10 for L being lower-bounded sup-Semilattice for a, b being auxiliary Relation of L holds a /\ b is auxiliary Relation of L proofend; theorem Th11: :: WAYBEL_4:11 for L being lower-bounded sup-Semilattice for X being non empty Subset of (InclPoset (Aux L)) holds meet X is auxiliary Relation of L proofend; registration let L be lower-bounded sup-Semilattice; cluster InclPoset (Aux L) -> with_infima ; coherence InclPoset (Aux L) is with_infima proofend; end; registration let L be lower-bounded sup-Semilattice; cluster InclPoset (Aux L) -> complete ; coherence InclPoset (Aux L) is complete proofend; end; definition let L be non empty RelStr ; let x be Element of L; let AR be Relation of the carrier of L; A1: { y where y is Element of L : [y,x] in AR } c= the carrier of L proofend; funcAR -below x -> Subset of L equals :: WAYBEL_4:def 10 { y where y is Element of L : [y,x] in AR } ; correctness coherence { y where y is Element of L : [y,x] in AR } is Subset of L; by A1; A2: { y where y is Element of L : [x,y] in AR } c= the carrier of L proofend; funcAR -above x -> Subset of L equals :: WAYBEL_4:def 11 { y where y is Element of L : [x,y] in AR } ; correctness coherence { y where y is Element of L : [x,y] in AR } is Subset of L; by A2; end; :: deftheorem defines -below WAYBEL_4:def_10_:_ for L being non empty RelStr for x being Element of L for AR being Relation of the carrier of L holds AR -below x = { y where y is Element of L : [y,x] in AR } ; :: deftheorem defines -above WAYBEL_4:def_11_:_ for L being non empty RelStr for x being Element of L for AR being Relation of the carrier of L holds AR -above x = { y where y is Element of L : [x,y] in AR } ; theorem Th12: :: WAYBEL_4:12 for L being lower-bounded sup-Semilattice for x being Element of L for AR being auxiliary(i) Relation of L holds AR -below x c= downarrow x proofend; registration let L be lower-bounded sup-Semilattice; let x be Element of L; let AR be auxiliary(iv) Relation of L; clusterAR -below x -> non empty ; coherence not AR -below x is empty proofend; end; registration let L be lower-bounded sup-Semilattice; let x be Element of L; let AR be auxiliary(ii) Relation of L; clusterAR -below x -> lower ; coherence AR -below x is lower proofend; end; registration let L be lower-bounded sup-Semilattice; let x be Element of L; let AR be auxiliary(iii) Relation of L; clusterAR -below x -> directed ; coherence AR -below x is directed proofend; end; definition let L be lower-bounded sup-Semilattice; let AR be auxiliary(ii) auxiliary(iii) auxiliary(iv) Relation of L; funcAR -below -> Function of L,(InclPoset (Ids L)) means :Def12: :: WAYBEL_4:def 12 for x being Element of L holds it . x = AR -below x; existence ex b1 being Function of L,(InclPoset (Ids L)) st for x being Element of L holds b1 . x = AR -below x proofend; uniqueness for b1, b2 being Function of L,(InclPoset (Ids L)) st ( for x being Element of L holds b1 . x = AR -below x ) & ( for x being Element of L holds b2 . x = AR -below x ) holds b1 = b2 proofend; end; :: deftheorem Def12 defines -below WAYBEL_4:def_12_:_ for L being lower-bounded sup-Semilattice for AR being auxiliary(ii) auxiliary(iii) auxiliary(iv) Relation of L for b3 being Function of L,(InclPoset (Ids L)) holds ( b3 = AR -below iff for x being Element of L holds b3 . x = AR -below x ); theorem Th13: :: WAYBEL_4:13 for L being non empty RelStr for AR being Relation of L for a being set for y being Element of L holds ( a in AR -below y iff [a,y] in AR ) proofend; theorem :: WAYBEL_4:14 for a being set for L being sup-Semilattice for AR being Relation of L for y being Element of L holds ( a in AR -above y iff [y,a] in AR ) proofend; Lm3: for L being lower-bounded with_suprema Poset for AR being Relation of L for a being set for y being Element of L holds ( a in downarrow y iff [a,y] in the InternalRel of L ) proofend; theorem :: WAYBEL_4:15 for L being lower-bounded sup-Semilattice for AR being auxiliary(i) Relation of L for x being Element of L st AR = the InternalRel of L holds AR -below x = downarrow x proofend; definition let L be non empty Poset; func MonSet L -> strict RelStr means :Def13: :: WAYBEL_4:def 13 for a being set holds ( ( a in the carrier of it implies ex s being Function of L,(InclPoset (Ids L)) st ( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st ( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of it ) & ( for c, d being set holds ( [c,d] in the InternalRel of it iff ex f, g being Function of L,(InclPoset (Ids L)) st ( c = f & d = g & c in the carrier of it & d in the carrier of it & f <= g ) ) ) ); existence ex b1 being strict RelStr st for a being set holds ( ( a in the carrier of b1 implies ex s being Function of L,(InclPoset (Ids L)) st ( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st ( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of b1 ) & ( for c, d being set holds ( [c,d] in the InternalRel of b1 iff ex f, g being Function of L,(InclPoset (Ids L)) st ( c = f & d = g & c in the carrier of b1 & d in the carrier of b1 & f <= g ) ) ) ) proofend; uniqueness for b1, b2 being strict RelStr st ( for a being set holds ( ( a in the carrier of b1 implies ex s being Function of L,(InclPoset (Ids L)) st ( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st ( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of b1 ) & ( for c, d being set holds ( [c,d] in the InternalRel of b1 iff ex f, g being Function of L,(InclPoset (Ids L)) st ( c = f & d = g & c in the carrier of b1 & d in the carrier of b1 & f <= g ) ) ) ) ) & ( for a being set holds ( ( a in the carrier of b2 implies ex s being Function of L,(InclPoset (Ids L)) st ( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st ( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of b2 ) & ( for c, d being set holds ( [c,d] in the InternalRel of b2 iff ex f, g being Function of L,(InclPoset (Ids L)) st ( c = f & d = g & c in the carrier of b2 & d in the carrier of b2 & f <= g ) ) ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def13 defines MonSet WAYBEL_4:def_13_:_ for L being non empty Poset for b2 being strict RelStr holds ( b2 = MonSet L iff for a being set holds ( ( a in the carrier of b2 implies ex s being Function of L,(InclPoset (Ids L)) st ( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st ( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of b2 ) & ( for c, d being set holds ( [c,d] in the InternalRel of b2 iff ex f, g being Function of L,(InclPoset (Ids L)) st ( c = f & d = g & c in the carrier of b2 & d in the carrier of b2 & f <= g ) ) ) ) ); theorem :: WAYBEL_4:16 for L being lower-bounded sup-Semilattice holds MonSet L is full SubRelStr of (InclPoset (Ids L)) |^ the carrier of L proofend; theorem Th17: :: WAYBEL_4:17 for L being lower-bounded sup-Semilattice for AR being auxiliary(ii) Relation of L for x, y being Element of L st x <= y holds AR -below x c= AR -below y proofend; registration let L be lower-bounded sup-Semilattice; let AR be auxiliary(ii) auxiliary(iii) auxiliary(iv) Relation of L; clusterAR -below -> monotone ; coherence AR -below is monotone proofend; end; theorem Th18: :: WAYBEL_4:18 for L being lower-bounded sup-Semilattice for AR being auxiliary Relation of L holds AR -below in the carrier of (MonSet L) proofend; registration let L be lower-bounded sup-Semilattice; cluster MonSet L -> non empty strict ; coherence not MonSet L is empty by Th18; end; theorem Th19: :: WAYBEL_4:19 for L being lower-bounded sup-Semilattice holds IdsMap L in the carrier of (MonSet L) proofend; theorem :: WAYBEL_4:20 for L being lower-bounded sup-Semilattice for AR being auxiliary Relation of L holds AR -below <= IdsMap L proofend; theorem Th21: :: WAYBEL_4:21 for L being non empty lower-bounded Poset for I being Ideal of L holds Bottom L in I proofend; theorem :: WAYBEL_4:22 for L being non empty upper-bounded Poset for F being Filter of L holds Top L in F proofend; theorem Th23: :: WAYBEL_4:23 for L being non empty lower-bounded Poset holds downarrow (Bottom L) = {(Bottom L)} proofend; theorem :: WAYBEL_4:24 for L being non empty upper-bounded Poset holds uparrow (Top L) = {(Top L)} proofend; Lm4: for L being lower-bounded sup-Semilattice for I being Ideal of L holds {(Bottom L)} c= I proofend; theorem Th25: :: WAYBEL_4:25 for L being lower-bounded sup-Semilattice holds the carrier of L --> {(Bottom L)} is Function of L,(InclPoset (Ids L)) proofend; Lm5: for L being lower-bounded sup-Semilattice for f being Function of L,(InclPoset (Ids L)) st f = the carrier of L --> {(Bottom L)} holds f is monotone proofend; theorem Th26: :: WAYBEL_4:26 for L being lower-bounded sup-Semilattice holds the carrier of L --> {(Bottom L)} in the carrier of (MonSet L) proofend; theorem :: WAYBEL_4:27 for L being lower-bounded sup-Semilattice for AR being auxiliary Relation of L holds [( the carrier of L --> {(Bottom L)}),(AR -below)] in the InternalRel of (MonSet L) proofend; Lm6: for L being lower-bounded sup-Semilattice ex x being Element of (MonSet L) st x is_>=_than the carrier of (MonSet L) proofend; registration let L be lower-bounded sup-Semilattice; cluster MonSet L -> strict upper-bounded ; coherence MonSet L is upper-bounded proofend; end; definition let L be lower-bounded sup-Semilattice; func Rel2Map L -> Function of (InclPoset (Aux L)),(MonSet L) means :Def14: :: WAYBEL_4:def 14 for AR being auxiliary Relation of L holds it . AR = AR -below ; existence ex b1 being Function of (InclPoset (Aux L)),(MonSet L) st for AR being auxiliary Relation of L holds b1 . AR = AR -below proofend; uniqueness for b1, b2 being Function of (InclPoset (Aux L)),(MonSet L) st ( for AR being auxiliary Relation of L holds b1 . AR = AR -below ) & ( for AR being auxiliary Relation of L holds b2 . AR = AR -below ) holds b1 = b2 proofend; end; :: deftheorem Def14 defines Rel2Map WAYBEL_4:def_14_:_ for L being lower-bounded sup-Semilattice for b2 being Function of (InclPoset (Aux L)),(MonSet L) holds ( b2 = Rel2Map L iff for AR being auxiliary Relation of L holds b2 . AR = AR -below ); theorem :: WAYBEL_4:28 for L being lower-bounded sup-Semilattice for R1, R2 being auxiliary Relation of L st R1 c= R2 holds R1 -below <= R2 -below proofend; theorem Th29: :: WAYBEL_4:29 for L being lower-bounded sup-Semilattice for x being Element of L for R1, R2 being Relation of L st R1 c= R2 holds R1 -below x c= R2 -below x proofend; Lm7: for L being lower-bounded sup-Semilattice holds Rel2Map L is monotone proofend; registration let L be lower-bounded sup-Semilattice; cluster Rel2Map L -> monotone ; coherence Rel2Map L is monotone by Lm7; end; definition let L be lower-bounded sup-Semilattice; func Map2Rel L -> Function of (MonSet L),(InclPoset (Aux L)) means :Def15: :: WAYBEL_4:def 15 for s being set st s in the carrier of (MonSet L) holds ex AR being auxiliary Relation of L st ( AR = it . s & ( for x, y being set holds ( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st ( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) ); existence ex b1 being Function of (MonSet L),(InclPoset (Aux L)) st for s being set st s in the carrier of (MonSet L) holds ex AR being auxiliary Relation of L st ( AR = b1 . s & ( for x, y being set holds ( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st ( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) ) proofend; uniqueness for b1, b2 being Function of (MonSet L),(InclPoset (Aux L)) st ( for s being set st s in the carrier of (MonSet L) holds ex AR being auxiliary Relation of L st ( AR = b1 . s & ( for x, y being set holds ( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st ( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) ) ) & ( for s being set st s in the carrier of (MonSet L) holds ex AR being auxiliary Relation of L st ( AR = b2 . s & ( for x, y being set holds ( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st ( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def15 defines Map2Rel WAYBEL_4:def_15_:_ for L being lower-bounded sup-Semilattice for b2 being Function of (MonSet L),(InclPoset (Aux L)) holds ( b2 = Map2Rel L iff for s being set st s in the carrier of (MonSet L) holds ex AR being auxiliary Relation of L st ( AR = b2 . s & ( for x, y being set holds ( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st ( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) ) ); Lm8: for L being lower-bounded sup-Semilattice holds Map2Rel L is monotone proofend; registration let L be lower-bounded sup-Semilattice; cluster Map2Rel L -> monotone ; coherence Map2Rel L is monotone by Lm8; end; theorem Th30: :: WAYBEL_4:30 for L being lower-bounded sup-Semilattice holds (Map2Rel L) * (Rel2Map L) = id (dom (Rel2Map L)) proofend; theorem Th31: :: WAYBEL_4:31 for L being lower-bounded sup-Semilattice holds (Rel2Map L) * (Map2Rel L) = id the carrier of (MonSet L) proofend; registration let L be lower-bounded sup-Semilattice; cluster Rel2Map L -> V16() ; coherence Rel2Map L is one-to-one proofend; end; :: Proposition 1.10 (i) p.43 theorem Th32: :: WAYBEL_4:32 for L being lower-bounded sup-Semilattice holds (Rel2Map L) " = Map2Rel L proofend; :: Proposition 1.10 (ii) p.43 theorem :: WAYBEL_4:33 for L being lower-bounded sup-Semilattice holds Rel2Map L is isomorphic proofend; theorem Th34: :: WAYBEL_4:34 for L being complete LATTICE for x being Element of L holds meet { I where I is Ideal of L : x <= sup I } = waybelow x proofend; definition let L be Semilattice; let I be Ideal of L; func DownMap I -> Function of L,(InclPoset (Ids L)) means :Def16: :: WAYBEL_4:def 16 for x being Element of L holds ( ( x <= sup I implies it . x = (downarrow x) /\ I ) & ( not x <= sup I implies it . x = downarrow x ) ); existence ex b1 being Function of L,(InclPoset (Ids L)) st for x being Element of L holds ( ( x <= sup I implies b1 . x = (downarrow x) /\ I ) & ( not x <= sup I implies b1 . x = downarrow x ) ) proofend; uniqueness for b1, b2 being Function of L,(InclPoset (Ids L)) st ( for x being Element of L holds ( ( x <= sup I implies b1 . x = (downarrow x) /\ I ) & ( not x <= sup I implies b1 . x = downarrow x ) ) ) & ( for x being Element of L holds ( ( x <= sup I implies b2 . x = (downarrow x) /\ I ) & ( not x <= sup I implies b2 . x = downarrow x ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def16 defines DownMap WAYBEL_4:def_16_:_ for L being Semilattice for I being Ideal of L for b3 being Function of L,(InclPoset (Ids L)) holds ( b3 = DownMap I iff for x being Element of L holds ( ( x <= sup I implies b3 . x = (downarrow x) /\ I ) & ( not x <= sup I implies b3 . x = downarrow x ) ) ); Lm9: for L being Semilattice for I being Ideal of L holds DownMap I is monotone proofend; Lm10: for L being Semilattice for x being Element of L for I being Ideal of L holds (DownMap I) . x c= downarrow x proofend; theorem Th35: :: WAYBEL_4:35 for L being Semilattice for I being Ideal of L holds DownMap I in the carrier of (MonSet L) proofend; theorem Th36: :: WAYBEL_4:36 for L being reflexive antisymmetric with_infima RelStr for x being Element of L for D being non empty lower Subset of L holds {x} "/\" D = (downarrow x) /\ D proofend; begin :: Definition 1.11 p.44 definition let L be non empty RelStr ; let AR be Relation of L; attrAR is approximating means :Def17: :: WAYBEL_4:def 17 for x being Element of L holds x = sup (AR -below x); end; :: deftheorem Def17 defines approximating WAYBEL_4:def_17_:_ for L being non empty RelStr for AR being Relation of L holds ( AR is approximating iff for x being Element of L holds x = sup (AR -below x) ); definition let L be non empty Poset; let mp be Function of L,(InclPoset (Ids L)); attrmp is approximating means :Def18: :: WAYBEL_4:def 18 for x being Element of L ex ii being Subset of L st ( ii = mp . x & x = sup ii ); end; :: deftheorem Def18 defines approximating WAYBEL_4:def_18_:_ for L being non empty Poset for mp being Function of L,(InclPoset (Ids L)) holds ( mp is approximating iff for x being Element of L ex ii being Subset of L st ( ii = mp . x & x = sup ii ) ); :: Lemma 1.12 (i) p.44 theorem Th37: :: WAYBEL_4:37 for L being lower-bounded meet-continuous Semilattice for I being Ideal of L holds DownMap I is approximating proofend; Lm11: for L being complete LATTICE for x being Element of L for D being directed Subset of L holds sup ({x} "/\" D) <= x proofend; :: Lemma 1.12 (ii) p.44 theorem Th38: :: WAYBEL_4:38 for L being lower-bounded continuous LATTICE holds L is meet-continuous proofend; registration cluster reflexive transitive antisymmetric lower-bounded with_suprema with_infima continuous -> lower-bounded meet-continuous for RelStr ; coherence for b1 being lower-bounded LATTICE st b1 is continuous holds b1 is meet-continuous by Th38; end; :: Lemma 1.12 (iii) p.44 theorem :: WAYBEL_4:39 for L being lower-bounded continuous LATTICE for I being Ideal of L holds DownMap I is approximating by Th37; registration let L be non empty reflexive antisymmetric RelStr ; clusterL -waybelow -> auxiliary(i) ; coherence L -waybelow is auxiliary(i) proofend; end; registration let L be non empty reflexive transitive RelStr ; clusterL -waybelow -> auxiliary(ii) ; coherence L -waybelow is auxiliary(ii) proofend; end; registration let L be with_suprema Poset; clusterL -waybelow -> auxiliary(iii) ; coherence L -waybelow is auxiliary(iii) proofend; end; registration let L be non empty /\-complete Poset; clusterL -waybelow -> auxiliary(iii) ; coherence L -waybelow is auxiliary(iii) proofend; end; registration let L be non empty reflexive antisymmetric lower-bounded RelStr ; clusterL -waybelow -> auxiliary(iv) ; coherence L -waybelow is auxiliary(iv) proofend; end; theorem Th40: :: WAYBEL_4:40 for L being complete LATTICE for x being Element of L holds (L -waybelow) -below x = waybelow x proofend; theorem Th41: :: WAYBEL_4:41 for L being LATTICE holds IntRel L is approximating proofend; Lm12: for L being lower-bounded continuous LATTICE holds L -waybelow is approximating proofend; registration let L be lower-bounded continuous LATTICE; clusterL -waybelow -> approximating ; coherence L -waybelow is approximating by Lm12; end; registration let L be complete LATTICE; cluster Relation-like auxiliary approximating for Element of bool [: the carrier of L, the carrier of L:]; existence ex b1 being Relation of L st ( b1 is approximating & b1 is auxiliary ) proofend; end; definition let L be complete LATTICE; defpred S1[ set ] means $1 is auxiliary approximating Relation of L; func App L -> set means :Def19: :: WAYBEL_4:def 19 for a being set holds ( a in it iff a is auxiliary approximating Relation of L ); existence ex b1 being set st for a being set holds ( a in b1 iff a is auxiliary approximating Relation of L ) proofend; uniqueness for b1, b2 being set st ( for a being set holds ( a in b1 iff a is auxiliary approximating Relation of L ) ) & ( for a being set holds ( a in b2 iff a is auxiliary approximating Relation of L ) ) holds b1 = b2 proofend; end; :: deftheorem Def19 defines App WAYBEL_4:def_19_:_ for L being complete LATTICE for b2 being set holds ( b2 = App L iff for a being set holds ( a in b2 iff a is auxiliary approximating Relation of L ) ); registration let L be complete LATTICE; cluster App L -> non empty ; coherence not App L is empty proofend; end; theorem Th42: :: WAYBEL_4:42 for L being complete LATTICE for mp being Function of L,(InclPoset (Ids L)) st mp is approximating & mp in the carrier of (MonSet L) holds ex AR being auxiliary approximating Relation of L st AR = (Map2Rel L) . mp proofend; theorem Th43: :: WAYBEL_4:43 for L being complete LATTICE for x being Element of L holds meet { ((DownMap I) . x) where I is Ideal of L : verum } = waybelow x proofend; :: Proposition 1.13 p.45 theorem Th44: :: WAYBEL_4:44 for L being lower-bounded meet-continuous LATTICE for x being Element of L holds meet { (AR -below x) where AR is auxiliary Relation of L : AR in App L } = waybelow x proofend; :: Proposition 1.14 p.45 ( 1 <=> 2 ) theorem Th45: :: WAYBEL_4:45 for L being complete LATTICE holds ( L is continuous iff for R being auxiliary approximating Relation of L holds ( L -waybelow c= R & L -waybelow is approximating ) ) proofend; :: Proposition 1.14 p.45 ( 1 <=> 3 ) theorem :: WAYBEL_4:46 for L being complete LATTICE holds ( L is continuous iff ( L is meet-continuous & ex R being auxiliary approximating Relation of L st for R9 being auxiliary approximating Relation of L holds R c= R9 ) ) proofend; :: Definition 1.15 (SI) p.46 definition let L be RelStr ; let AR be Relation of L; attrAR is satisfying_SI means :Def20: :: WAYBEL_4:def 20 for x, z being Element of L st [x,z] in AR & x <> z holds ex y being Element of L st ( [x,y] in AR & [y,z] in AR & x <> y ); end; :: deftheorem Def20 defines satisfying_SI WAYBEL_4:def_20_:_ for L being RelStr for AR being Relation of L holds ( AR is satisfying_SI iff for x, z being Element of L st [x,z] in AR & x <> z holds ex y being Element of L st ( [x,y] in AR & [y,z] in AR & x <> y ) ); :: Definition 1.15 (INT) p.46 definition let L be RelStr ; let AR be Relation of L; attrAR is satisfying_INT means :Def21: :: WAYBEL_4:def 21 for x, z being Element of L st [x,z] in AR holds ex y being Element of L st ( [x,y] in AR & [y,z] in AR ); end; :: deftheorem Def21 defines satisfying_INT WAYBEL_4:def_21_:_ for L being RelStr for AR being Relation of L holds ( AR is satisfying_INT iff for x, z being Element of L st [x,z] in AR holds ex y being Element of L st ( [x,y] in AR & [y,z] in AR ) ); theorem Th47: :: WAYBEL_4:47 for L being RelStr for AR being Relation of L st AR is satisfying_SI holds AR is satisfying_INT proofend; registration let L be non empty RelStr ; cluster satisfying_SI -> satisfying_INT for Element of bool [: the carrier of L, the carrier of L:]; coherence for b1 being Relation of L st b1 is satisfying_SI holds b1 is satisfying_INT by Th47; end; theorem Th48: :: WAYBEL_4:48 for L being complete LATTICE for x, y being Element of L for AR being approximating Relation of L st not x <= y holds ex u being Element of L st ( [u,x] in AR & not u <= y ) proofend; :: Lemma 1.16 p.46 theorem Th49: :: WAYBEL_4:49 for L being complete LATTICE for x, z being Element of L for R being auxiliary(i) auxiliary(iii) approximating Relation of L st [x,z] in R & x <> z holds ex y being Element of L st ( x <= y & [y,z] in R & x <> y ) proofend; :: Lemma 1.17 p.46 theorem Th50: :: WAYBEL_4:50 for L being complete LATTICE for x, z being Element of L for R being auxiliary approximating Relation of L st x << z & x <> z holds ex y being Element of L st ( [x,y] in R & [y,z] in R & x <> y ) proofend; :: Theorem 1.18 p.47 theorem Th51: :: WAYBEL_4:51 for L being lower-bounded continuous LATTICE holds L -waybelow is satisfying_SI proofend; registration let L be lower-bounded continuous LATTICE; clusterL -waybelow -> satisfying_SI ; coherence L -waybelow is satisfying_SI by Th51; end; theorem Th52: :: WAYBEL_4:52 for L being lower-bounded continuous LATTICE for x, y being Element of L st x << y holds ex x9 being Element of L st ( x << x9 & x9 << y ) proofend; :: Corollary 1.19 p.47 theorem :: WAYBEL_4:53 for L being lower-bounded continuous LATTICE for x, y being Element of L holds ( x << y iff for D being non empty directed Subset of L st y <= sup D holds ex d being Element of L st ( d in D & x << d ) ) proofend; begin definition let L be RelStr ; let X be Subset of L; let R be Relation of the carrier of L; predX is_directed_wrt R means :Def22: :: WAYBEL_4:def 22 for x, y being Element of L st x in X & y in X holds ex z being Element of L st ( z in X & [x,z] in R & [y,z] in R ); end; :: deftheorem Def22 defines is_directed_wrt WAYBEL_4:def_22_:_ for L being RelStr for X being Subset of L for R being Relation of the carrier of L holds ( X is_directed_wrt R iff for x, y being Element of L st x in X & y in X holds ex z being Element of L st ( z in X & [x,z] in R & [y,z] in R ) ); theorem :: WAYBEL_4:54 for L being RelStr for X being Subset of L st X is_directed_wrt the InternalRel of L holds X is directed proofend; definition let X, x be set ; let R be Relation; predx is_maximal_wrt X,R means :Def23: :: WAYBEL_4:def 23 ( x in X & ( for y being set holds ( not y in X or not y <> x or not [x,y] in R ) ) ); end; :: deftheorem Def23 defines is_maximal_wrt WAYBEL_4:def_23_:_ for X, x being set for R being Relation holds ( x is_maximal_wrt X,R iff ( x in X & ( for y being set holds ( not y in X or not y <> x or not [x,y] in R ) ) ) ); definition let L be RelStr ; let X be set ; let x be Element of L; predx is_maximal_in X means :Def24: :: WAYBEL_4:def 24 x is_maximal_wrt X, the InternalRel of L; end; :: deftheorem Def24 defines is_maximal_in WAYBEL_4:def_24_:_ for L being RelStr for X being set for x being Element of L holds ( x is_maximal_in X iff x is_maximal_wrt X, the InternalRel of L ); theorem :: WAYBEL_4:55 for L being RelStr for X being set for x being Element of L holds ( x is_maximal_in X iff ( x in X & ( for y being Element of L holds ( not y in X or not x < y ) ) ) ) proofend; definition let X, x be set ; let R be Relation; predx is_minimal_wrt X,R means :Def25: :: WAYBEL_4:def 25 ( x in X & ( for y being set holds ( not y in X or not y <> x or not [y,x] in R ) ) ); end; :: deftheorem Def25 defines is_minimal_wrt WAYBEL_4:def_25_:_ for X, x being set for R being Relation holds ( x is_minimal_wrt X,R iff ( x in X & ( for y being set holds ( not y in X or not y <> x or not [y,x] in R ) ) ) ); definition let L be RelStr ; let X be set ; let x be Element of L; predx is_minimal_in X means :Def26: :: WAYBEL_4:def 26 x is_minimal_wrt X, the InternalRel of L; end; :: deftheorem Def26 defines is_minimal_in WAYBEL_4:def_26_:_ for L being RelStr for X being set for x being Element of L holds ( x is_minimal_in X iff x is_minimal_wrt X, the InternalRel of L ); theorem :: WAYBEL_4:56 for L being RelStr for X being set for x being Element of L holds ( x is_minimal_in X iff ( x in X & ( for y being Element of L holds ( not y in X or not x > y ) ) ) ) proofend; :: Exercise 1.23 (i) ( 1 => 2 ) theorem :: WAYBEL_4:57 for L being complete LATTICE for AR being Relation of L st AR is satisfying_SI holds for x being Element of L st ex y being Element of L st y is_maximal_wrt AR -below x,AR holds [x,x] in AR proofend; :: Exercise 1.23 (i) ( 2 => 1 ) theorem :: WAYBEL_4:58 for L being complete LATTICE for AR being Relation of L st ( for x being Element of L st ex y being Element of L st y is_maximal_wrt AR -below x,AR holds [x,x] in AR ) holds AR is satisfying_SI proofend; :: Exercise 1.23 (ii) ( 3 => 4 ) theorem :: WAYBEL_4:59 for L being complete LATTICE for AR being auxiliary(ii) auxiliary(iii) Relation of L st AR is satisfying_INT holds for x being Element of L holds AR -below x is_directed_wrt AR proofend; :: Exercise 1.23 (ii) ( 4 => 3 ) theorem :: WAYBEL_4:60 for L being complete LATTICE for AR being Relation of L st ( for x being Element of L holds AR -below x is_directed_wrt AR ) holds AR is satisfying_INT proofend; :: Exercise 1.23 (iii) p.51 theorem Th61: :: WAYBEL_4:61 for L being complete LATTICE for R being auxiliary(i) auxiliary(ii) auxiliary(iii) approximating Relation of L st R is satisfying_INT holds R is satisfying_SI proofend; registration let L be complete LATTICE; cluster auxiliary approximating satisfying_INT -> auxiliary approximating satisfying_SI for Element of bool [: the carrier of L, the carrier of L:]; coherence for b1 being auxiliary approximating Relation of L st b1 is satisfying_INT holds b1 is satisfying_SI by Th61; end;