:: The Equational Characterization of Continuous Lattices :: by Mariusz \.Zynel :: :: Received October 25, 1996 :: Copyright (c) 1996-2012 Association of Mizar Users begin Lm1: for L being continuous Semilattice for x being Element of L holds ( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds waybelow x c= I ) ) proofend; Lm2: for L being up-complete Semilattice st ( for x being Element of L holds ( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds waybelow x c= I ) ) ) holds L is continuous proofend; theorem :: WAYBEL_5:1 for L being up-complete Semilattice holds ( L is continuous iff for x being Element of L holds ( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds waybelow x c= I ) ) ) by Lm1, Lm2; Lm3: for L being up-complete Semilattice st L is continuous holds for x being Element of L ex I being Ideal of L st ( x <= sup I & ( for J being Ideal of L st x <= sup J holds I c= J ) ) proofend; Lm4: for L being up-complete Semilattice st ( for x being Element of L ex I being Ideal of L st ( x <= sup I & ( for J being Ideal of L st x <= sup J holds I c= J ) ) ) holds L is continuous proofend; theorem :: WAYBEL_5:2 for L being up-complete Semilattice holds ( L is continuous iff for x being Element of L ex I being Ideal of L st ( x <= sup I & ( for J being Ideal of L st x <= sup J holds I c= J ) ) ) by Lm3, Lm4; theorem :: WAYBEL_5:3 for L being lower-bounded continuous sup-Semilattice holds SupMap L is upper_adjoint proofend; theorem :: WAYBEL_5:4 for L being lower-bounded up-complete LATTICE st SupMap L is upper_adjoint holds L is continuous proofend; theorem :: WAYBEL_5:5 for L being complete Semilattice st SupMap L is infs-preserving & SupMap L is sups-preserving holds SupMap L is upper_adjoint proofend; :: Corollary 2.2 can be found in WAYBEL_4. definition let J, D be set ; let K be ManySortedSet of J; mode DoubleIndexedSet of K,D is ManySortedFunction of K,J --> D; end; definition let J be set ; let K be ManySortedSet of J; let S be 1-sorted ; mode DoubleIndexedSet of K,S is DoubleIndexedSet of K, the carrier of S; end; theorem Th6: :: WAYBEL_5:6 for J, D being set for K being ManySortedSet of J for F being DoubleIndexedSet of K,D for j being set st j in J holds F . j is Function of (K . j),D proofend; definition let J, D be non empty set ; let K be ManySortedSet of J; let F be DoubleIndexedSet of K,D; let j be Element of J; :: original:. redefine funcF . j -> Function of (K . j),D; coherence F . j is Function of (K . j),D by Th6; end; registration let J, D be non empty set ; let K be V9() ManySortedSet of J; let F be DoubleIndexedSet of K,D; let j be Element of J; cluster proj2 (F . j) -> non empty ; correctness coherence not rng (F . j) is empty ; ; end; registration let J be set ; let D be non empty set ; let K be V9() ManySortedSet of J; cluster -> V9() for ManySortedFunction of K,J --> D; correctness coherence for b1 being DoubleIndexedSet of K,D holds b1 is V9(); proofend; end; theorem :: WAYBEL_5:7 for F being Function-yielding Function for f being set st f in dom (Frege F) holds f is Function ; theorem Th8: :: WAYBEL_5:8 for F being Function-yielding Function for f being Function st f in dom (Frege F) holds ( dom f = dom F & dom F = dom ((Frege F) . f) ) proofend; theorem Th9: :: WAYBEL_5:9 for F being Function-yielding Function for f being Function st f in dom (Frege F) holds for i being set st i in dom F holds ( f . i in dom (F . i) & ((Frege F) . f) . i = (F . i) . (f . i) & (F . i) . (f . i) in rng ((Frege F) . f) ) proofend; theorem Th10: :: WAYBEL_5:10 for J, D being set for K being ManySortedSet of J for F being DoubleIndexedSet of K,D for f being Function st f in dom (Frege F) holds (Frege F) . f is Function of J,D proofend; Lm5: for J, D being set for K being ManySortedSet of J for F being DoubleIndexedSet of K,D for f being Function st f in dom (Frege F) holds for j being set st j in J holds ( ((Frege F) . f) . j = (F . j) . (f . j) & (F . j) . (f . j) in rng ((Frege F) . f) ) proofend; Lm6: for J being set for K being ManySortedSet of J for D being non empty set for F being DoubleIndexedSet of K,D for f being Function st f in dom (Frege F) holds for j being set st j in J holds f . j in K . j proofend; registration let f be non-empty Function; cluster doms f -> non-empty ; correctness coherence doms f is non-empty ; proofend; end; definition let J, D be set ; let K be ManySortedSet of J; let F be DoubleIndexedSet of K,D; :: original:Frege redefine func Frege F -> DoubleIndexedSet of (product (doms F)) --> J,D; coherence Frege F is DoubleIndexedSet of (product (doms F)) --> J,D proofend; end; definition let J, D be non empty set ; let K be V9() ManySortedSet of J; let F be DoubleIndexedSet of K,D; let G be DoubleIndexedSet of (product (doms F)) --> J,D; let f be Element of product (doms F); :: original:. redefine funcG . f -> Function of J,D; coherence G . f is Function of J,D proofend; end; definition let L be non empty RelStr ; let F be Function-yielding Function; func \// (F,L) -> Function of (dom F), the carrier of L means :Def1: :: WAYBEL_5:def 1 for x being set st x in dom F holds it . x = \\/ ((F . x),L); existence ex b1 being Function of (dom F), the carrier of L st for x being set st x in dom F holds b1 . x = \\/ ((F . x),L) proofend; uniqueness for b1, b2 being Function of (dom F), the carrier of L st ( for x being set st x in dom F holds b1 . x = \\/ ((F . x),L) ) & ( for x being set st x in dom F holds b2 . x = \\/ ((F . x),L) ) holds b1 = b2 proofend; func /\\ (F,L) -> Function of (dom F), the carrier of L means :Def2: :: WAYBEL_5:def 2 for x being set st x in dom F holds it . x = //\ ((F . x),L); existence ex b1 being Function of (dom F), the carrier of L st for x being set st x in dom F holds b1 . x = //\ ((F . x),L) proofend; uniqueness for b1, b2 being Function of (dom F), the carrier of L st ( for x being set st x in dom F holds b1 . x = //\ ((F . x),L) ) & ( for x being set st x in dom F holds b2 . x = //\ ((F . x),L) ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines \// WAYBEL_5:def_1_:_ for L being non empty RelStr for F being Function-yielding Function for b3 being Function of (dom F), the carrier of L holds ( b3 = \// (F,L) iff for x being set st x in dom F holds b3 . x = \\/ ((F . x),L) ); :: deftheorem Def2 defines /\\ WAYBEL_5:def_2_:_ for L being non empty RelStr for F being Function-yielding Function for b3 being Function of (dom F), the carrier of L holds ( b3 = /\\ (F,L) iff for x being set st x in dom F holds b3 . x = //\ ((F . x),L) ); notation let J be set ; let K be ManySortedSet of J; let L be non empty RelStr ; let F be DoubleIndexedSet of K,L; synonym Sups F for \// (K,J); synonym Infs F for /\\ (K,J); end; notation let I, J be set ; let L be non empty RelStr ; let F be DoubleIndexedSet of I --> J,L; synonym Sups F for \// (J,I); synonym Infs F for /\\ (J,I); end; theorem Th11: :: WAYBEL_5:11 for L being non empty RelStr for F, G being Function-yielding Function st dom F = dom G & ( for x being set st x in dom F holds \\/ ((F . x),L) = \\/ ((G . x),L) ) holds \// (F,L) = \// (G,L) proofend; theorem Th12: :: WAYBEL_5:12 for L being non empty RelStr for F, G being Function-yielding Function st dom F = dom G & ( for x being set st x in dom F holds //\ ((F . x),L) = //\ ((G . x),L) ) holds /\\ (F,L) = /\\ (G,L) proofend; theorem Th13: :: WAYBEL_5:13 for y being set for L being non empty RelStr for F being Function-yielding Function holds ( ( y in rng (\// (F,L)) implies ex x being set st ( x in dom F & y = \\/ ((F . x),L) ) ) & ( ex x being set st ( x in dom F & y = \\/ ((F . x),L) ) implies y in rng (\// (F,L)) ) & ( y in rng (/\\ (F,L)) implies ex x being set st ( x in dom F & y = //\ ((F . x),L) ) ) & ( ex x being set st ( x in dom F & y = //\ ((F . x),L) ) implies y in rng (/\\ (F,L)) ) ) proofend; theorem Th14: :: WAYBEL_5:14 for x being set for L being non empty RelStr for J being non empty set for K being ManySortedSet of J for F being DoubleIndexedSet of K,L holds ( ( x in rng (Sups ) implies ex j being Element of J st x = Sup ) & ( ex j being Element of J st x = Sup implies x in rng (Sups ) ) & ( x in rng (Infs ) implies ex j being Element of J st x = Inf ) & ( ex j being Element of J st x = Inf implies x in rng (Infs ) ) ) proofend; registration let J be non empty set ; let K be ManySortedSet of J; let L be non empty RelStr ; let F be DoubleIndexedSet of K,L; cluster proj2 (Sups ) -> non empty ; correctness coherence not rng (Sups ) is empty ; ; cluster proj2 (Infs ) -> non empty ; correctness coherence not rng (Infs ) is empty ; ; end; Lm7: for L being complete LATTICE for J being non empty set for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L for f being set holds ( f is Element of product (doms F) iff f in dom (Frege F) ) proofend; theorem Th15: :: WAYBEL_5:15 for L being complete LATTICE for a being Element of L for F being Function-yielding Function st ( for f being Function st f in dom (Frege F) holds //\ (((Frege F) . f),L) <= a ) holds Sup <= a proofend; theorem Th16: :: WAYBEL_5:16 for L being complete LATTICE for J being non empty set for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L holds Inf >= Sup proofend; theorem Th17: :: WAYBEL_5:17 for L being complete LATTICE for a, b being Element of L st L is continuous & ( for c being Element of L st c << a holds c <= b ) holds a <= b proofend; Lm8: for L being complete LATTICE st L is continuous holds for J being non empty set for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds Inf = Sup proofend; theorem Th18: :: WAYBEL_5:18 for L being complete LATTICE st ( for J being non empty set st J in the_universe_of the carrier of L holds for K being V9() ManySortedSet of J st ( for j being Element of J holds K . j in the_universe_of the carrier of L ) holds for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds Inf = Sup ) holds L is continuous proofend; Lm9: for L being complete LATTICE st ( for J being non empty set for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds Inf = Sup ) holds L is continuous proofend; theorem :: WAYBEL_5:19 for L being complete LATTICE holds ( L is continuous iff for J being non empty set for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds Inf = Sup ) by Lm8, Lm9; definition let J, K, D be non empty set ; let F be Function of [:J,K:],D; :: original:curry redefine func curry F -> DoubleIndexedSet of J --> K,D; coherence curry F is DoubleIndexedSet of J --> K,D proofend; end; theorem Th20: :: WAYBEL_5:20 for J, K, D being non empty set for j being Element of J for k being Element of K for F being Function of [:J,K:],D holds ( dom (curry F) = J & dom ((curry F) . j) = K & F . (j,k) = ((curry F) . j) . k ) proofend; Lm10: for L being complete LATTICE st ( for J, K being non empty set for F being Function of [:J,K:], the carrier of L st ( for j being Element of J holds rng ((curry F) . j) is directed ) holds Inf = Sup ) holds L is continuous proofend; theorem :: WAYBEL_5:21 for L being complete LATTICE holds ( L is continuous iff for J, K being non empty set for F being Function of [:J,K:], the carrier of L st ( for j being Element of J holds rng ((curry F) . j) is directed ) holds Inf = Sup ) by Lm8, Lm10; Lm11: for J, K being non empty set for f being Function st f in Funcs (J,(Fin K)) holds for j being Element of J holds f . j is finite Subset of K proofend; Lm12: for L being complete LATTICE for J, K, D being non empty set for j being Element of J for F being Function of [:J,K:],D for f being V9() ManySortedSet of J st f in Funcs (J,(Fin K)) holds for G being DoubleIndexedSet of f,L st ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) holds rng (G . j) is finite Subset of (rng ((curry F) . j)) proofend; theorem Th22: :: WAYBEL_5:22 for L being complete LATTICE for J, K being non empty set for F being Function of [:J,K:], the carrier of L for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of J st ( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st ( ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) & a = Inf ) ) } holds Inf >= sup X proofend; Lm13: for L being complete LATTICE st L is continuous holds for J, K being non empty set for F being Function of [:J,K:], the carrier of L for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of J st ( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st ( ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) & a = Inf ) ) } holds Inf = sup X proofend; Lm14: for L being complete LATTICE st ( for J, K being non empty set for F being Function of [:J,K:], the carrier of L for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of J st ( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st ( ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) & a = Inf ) ) } holds Inf = sup X ) holds L is continuous proofend; theorem :: WAYBEL_5:23 for L being complete LATTICE holds ( L is continuous iff for J, K being non empty set for F being Function of [:J,K:], the carrier of L for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of J st ( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st ( ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) & a = Inf ) ) } holds Inf = sup X ) by Lm13, Lm14; begin definition let L be non empty RelStr ; attrL is completely-distributive means :Def3: :: WAYBEL_5:def 3 ( L is complete & ( for J being non empty set for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L holds Inf = Sup ) ); end; :: deftheorem Def3 defines completely-distributive WAYBEL_5:def_3_:_ for L being non empty RelStr holds ( L is completely-distributive iff ( L is complete & ( for J being non empty set for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L holds Inf = Sup ) ) ); registration cluster1 -element reflexive transitive antisymmetric -> 1 -element completely-distributive for RelStr ; coherence for b1 being 1 -element Poset holds b1 is completely-distributive proofend; end; registration cluster non empty total reflexive transitive antisymmetric with_suprema with_infima completely-distributive for RelStr ; existence ex b1 being LATTICE st b1 is completely-distributive proofend; end; theorem Th24: :: WAYBEL_5:24 for L being completely-distributive LATTICE holds L is continuous proofend; registration cluster reflexive transitive antisymmetric with_suprema with_infima completely-distributive -> complete continuous for RelStr ; correctness coherence for b1 being LATTICE st b1 is completely-distributive holds ( b1 is complete & b1 is continuous ); by Def3, Th24; end; theorem Th25: :: WAYBEL_5:25 for L being non empty transitive antisymmetric with_infima RelStr for x being Element of L for X, Y being Subset of L st ex_sup_of X,L & ex_sup_of Y,L & Y = { (x "/\" y) where y is Element of L : y in X } holds x "/\" (sup X) >= sup Y proofend; Lm15: for L being completely-distributive LATTICE for X being non empty Subset of L for x being Element of L holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) proofend; theorem Th26: :: WAYBEL_5:26 for L being completely-distributive LATTICE for X being Subset of L for x being Element of L holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) proofend; registration cluster reflexive transitive antisymmetric with_suprema with_infima completely-distributive -> Heyting for RelStr ; correctness coherence for b1 being LATTICE st b1 is completely-distributive holds b1 is Heyting ; proofend; end; begin definition let L be non empty RelStr ; mode CLSubFrame of L is non empty full infs-inheriting directed-sups-inheriting SubRelStr of L; end; theorem Th27: :: WAYBEL_5:27 for L being complete LATTICE for J being non empty set for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds rng (Infs ) is directed proofend; theorem :: WAYBEL_5:28 for L being complete LATTICE st L is continuous holds for S being CLSubFrame of L holds S is continuous LATTICE proofend; theorem Th29: :: WAYBEL_5:29 for L being complete LATTICE for S being non empty Poset st ex g being Function of L,S st ( g is infs-preserving & g is onto ) holds S is complete LATTICE proofend; notation let J, y be set ; synonym J => y for J --> y; end; registration let J, y be set ; clusterJ => y -> J -defined total for J -defined Function; coherence for b1 being J -defined Function st b1 = J => y holds b1 is total ; end; definition let A, B, J be set ; let f be Function of A,B; :: original:=> redefine funcJ => f -> ManySortedFunction of J --> A,J --> B; coherence J => f is ManySortedFunction of J --> A,J --> B proofend; end; theorem Th30: :: WAYBEL_5:30 for J being non empty set for A, B being set for f being Function of A,B for g being Function of B,A st g * f = id A holds (J => g) ** (J => f) = id (J --> A) proofend; theorem Th31: :: WAYBEL_5:31 for J, A being non empty set for B being set for K being ManySortedSet of J for F being DoubleIndexedSet of K,A for f being Function of A,B holds (J => f) ** F is DoubleIndexedSet of K,B proofend; theorem Th32: :: WAYBEL_5:32 for J, A, B being non empty set for K being ManySortedSet of J for F being DoubleIndexedSet of K,A for f being Function of A,B holds doms ((J => f) ** F) = doms F proofend; theorem :: WAYBEL_5:33 for L being complete LATTICE st L is continuous holds for S being non empty Poset st ex g being Function of L,S st ( g is infs-preserving & g is directed-sups-preserving & g is onto ) holds S is continuous LATTICE proofend;