:: The Equational Characterization of Continuous Lattices :: by Mariusz \.Zynel :: :: Received October 25, 1996 :: Copyright (c) 1996-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies WAYBEL_0, ORDINAL2, SUBSET_1, WAYBEL_3, CARD_FIL, XXREAL_0, TARSKI, XBOOLE_0, YELLOW_0, LATTICE3, LATTICES, YELLOW_2, WAYBEL_1, YELLOW_1, RELAT_1, FUNCT_1, STRUCT_0, REWRITE1, PBOOLE, FUNCOP_1, FUNCT_6, CARD_3, FINSEQ_4, ORDERS_2, YELLOW_6, CLASSES1, CLASSES2, ZFMISC_1, FUNCT_5, EQREL_1, FUNCT_2, FINSUB_1, FINSET_1, ORDERS_1, RELAT_2, LATTICE2, CAT_1, XBOOLEAN, PARTFUN1, MEMBER_1, SEQM_3, WAYBEL_5, CARD_1; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, FINSET_1, FINSUB_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_4, FUNCT_5, FUNCT_6, FUNCOP_1, ORDERS_1, DOMAIN_1, STRUCT_0, ORDERS_2, LATTICE3, CARD_3, PBOOLE, PRALG_1, PRALG_2, MSUALG_3, CLASSES1, CLASSES2, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_0, WAYBEL_3, YELLOW_6; constructors FINSUB_1, CLASSES1, CLASSES2, BORSUK_1, LATTICE3, PRALG_1, PRALG_2, MSUALG_3, ORDERS_3, WAYBEL_1, WAYBEL_3, YELLOW_6, FUNCT_5, XTUPLE_0; registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FUNCOP_1, FUNCT_4, FINSET_1, CARD_3, CLASSES2, PBOOLE, STRUCT_0, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_3, YELLOW_6, PRALG_1, RELAT_1; requirements SUBSET, BOOLE; begin :: The Continuity of Lattices reserve x, y, i for object, L for up-complete Semilattice; theorem :: WAYBEL_5:1 ::Theorem 2.1 (1) iff (2) 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; theorem :: WAYBEL_5:2 ::Theorem 2.1 (1) iff (3) 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; theorem :: WAYBEL_5:3 ::Theorem 2.1 (1) implies (4) for L being continuous lower-bounded sup-Semilattice holds SupMap L is upper_adjoint; theorem :: WAYBEL_5:4 ::Theorem 2.1 (4) implies (1) for L being up-complete lower-bounded LATTICE holds SupMap L is upper_adjoint implies L is continuous; theorem :: WAYBEL_5:5 ::Theorem 2.1 (5) implies (4) for L being complete Semilattice holds SupMap L is infs-preserving sups-preserving implies SupMap L is upper_adjoint; :: Corollary 2.2 can be found in WAYBEL_4. definition let J, D be set, K be ManySortedSet of J; mode DoubleIndexedSet of K, D is ManySortedFunction of K, (J --> D); end; definition let J be set, K be ManySortedSet of J, S be 1-sorted; mode DoubleIndexedSet of K, S is DoubleIndexedSet of K, the carrier of S; end; theorem :: WAYBEL_5:6 for J, D being set, 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; definition let J, D be non empty set, K be ManySortedSet of J; let F be DoubleIndexedSet of K, D; let j be Element of J; redefine func F.j -> Function of K.j, D; end; registration let J, D be non empty set, K be non-empty ManySortedSet of J; let F be DoubleIndexedSet of K, D; let j be Element of J; cluster rng(F.j) -> non empty; end; registration let J be set, D be non empty set; let K be non-empty ManySortedSet of J; cluster -> non-empty for DoubleIndexedSet of K, D; end; registration let F be Function-yielding Function; cluster dom Frege F -> functional; end; ::$CT theorem :: 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); theorem :: WAYBEL_5:9 for F being Function-yielding Function for f being Function st f in dom Frege F 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); theorem :: WAYBEL_5:10 for J, D being set, 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; registration let f be non-empty Function-yielding Function; cluster doms f -> non-empty; end; definition let J, D be set, K be ManySortedSet of J; let F be DoubleIndexedSet of K, D; redefine func Frege F -> DoubleIndexedSet of (product doms F --> J), D; end; definition let J, D be non empty set, K be non-empty 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; redefine func G.f -> Function of J, D; 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 :: WAYBEL_5:def 1 for x st x in dom F holds it.x = \\/(F.x, L); func /\\(F, L) -> Function of dom F, the carrier of L means :: WAYBEL_5:def 2 for x st x in dom F holds it.x = //\(F.x, L); end; notation let J be set, K be ManySortedSet of J, L be non empty RelStr; let F be DoubleIndexedSet of K, L; synonym Sups F for \//(F, L); synonym Infs F for /\\(F, L); end; notation let I, J be set, L be non empty RelStr; let F be DoubleIndexedSet of (I --> J), L; synonym Sups F for \//(F, L); synonym Infs F for /\\(F, L); end; theorem :: WAYBEL_5:11 for L being non empty RelStr for F, G being Function-yielding Function st dom F = dom G & (for x st x in dom F holds \\/(F.x, L) = \\/(G.x, L )) holds \//(F, L) = \//(G, L); theorem :: WAYBEL_5:12 for L being non empty RelStr for F, G being Function-yielding Function st dom F = dom G & (for x st x in dom F holds //\(F.x, L) = //\(G.x, L )) holds /\\(F, L) = /\\(G, L); theorem :: WAYBEL_5:13 for L being non empty RelStr for F being Function-yielding Function holds (y in rng \//(F, L) iff ex x st x in dom F & y = \\/(F.x, L)) & (y in rng /\\(F, L) iff ex x st x in dom F & y = //\(F.x, L)); theorem :: WAYBEL_5:14 for L being non empty RelStr for J being non empty set, K being ManySortedSet of J for F being DoubleIndexedSet of K, L holds (x in rng Sups F iff ex j being Element of J st x = Sup(F.j)) & (x in rng Infs F iff ex j being Element of J st x = Inf(F.j)); registration let J be non empty set, K be ManySortedSet of J, L be non empty RelStr; let F be DoubleIndexedSet of K, L; cluster rng Sups F -> non empty; cluster rng Infs F -> non empty; end; reserve L for complete LATTICE, a, b, c for Element of L, J for non empty set, K for non-empty ManySortedSet of J; theorem :: WAYBEL_5:15 for F being Function-yielding Function holds (for f being Function st f in dom Frege F holds //\((Frege F).f, L) <= a) implies Sup /\\( Frege F, L) <= a; theorem :: WAYBEL_5:16 for F being DoubleIndexedSet of K, L holds Inf Sups F >= Sup Infs Frege F; theorem :: WAYBEL_5:17 (L is continuous & for c st c << a holds c <= b) implies a <= b; theorem :: WAYBEL_5:18 ::Theorem 2.3 (2) implies (1) (for J being non empty set st J in the_universe_of the carrier of L for K being non-empty ManySortedSet of J st for j being Element of J holds K.j in the_universe_of the carrier of L for F being DoubleIndexedSet of K, L st for j being Element of J holds rng(F.j) is directed holds Inf Sups F = Sup Infs Frege F) implies L is continuous; theorem :: WAYBEL_5:19 ::Theorem 2.3 (1) iff (2) L is continuous iff for J, K for F being DoubleIndexedSet of K, L st for j being Element of J holds rng(F.j) is directed holds Inf Sups F = Sup Infs Frege F; definition let J, K, D be non empty set; let F be Function of [:J, K:], D; redefine func curry F -> DoubleIndexedSet of (J --> K), D; end; reserve J, K, D for non empty set, j for Element of J, k for Element of K; theorem :: WAYBEL_5:20 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; theorem :: WAYBEL_5:21 ::Theorem 2.3 (1) iff (2') 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 Sups curry F = Sup Infs Frege curry F; theorem :: WAYBEL_5:22 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 non-empty ManySortedSet of J st f in Funcs(J, Fin K) & ex G being DoubleIndexedSet of f, L st (for j, x st x in f.j holds (G.j).x = F.(j, x)) & a = Inf Sups G} holds Inf Sups curry F >= sup X; theorem :: WAYBEL_5:23 ::Theorem 2.3 (1) iff (3) L is continuous iff for J, K 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 non-empty ManySortedSet of J st f in Funcs(J, Fin K) & ex G being DoubleIndexedSet of f, L st (for j, x st x in f.j holds (G.j).x = F.(j, x)) & a = Inf Sups G} holds Inf Sups curry F = sup X; begin :: Completely-Distributive Lattices definition let L be non empty RelStr; attr L is completely-distributive means :: WAYBEL_5:def 3 L is complete & for J being non empty set, K being non-empty ManySortedSet of J for F being DoubleIndexedSet of K, L holds Inf Sups F = Sup Infs Frege F; end; reserve J for non empty set, K for non-empty ManySortedSet of J; registration cluster -> completely-distributive for 1-element Poset; end; registration cluster completely-distributive for LATTICE; end; theorem :: WAYBEL_5:24 ::Corollary 2.5 for L being completely-distributive LATTICE holds L is continuous; registration cluster completely-distributive -> complete continuous for LATTICE; end; theorem :: WAYBEL_5:25 for L being non empty antisymmetric transitive 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; theorem :: 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); registration cluster completely-distributive -> Heyting for LATTICE; end; :: For distributivity confer WAYBEL_1. begin :: SubFrames of Continuous Lattices definition let L be non empty RelStr; mode CLSubFrame of L is infs-inheriting directed-sups-inheriting non empty full SubRelStr of L; end; theorem :: WAYBEL_5:27 for F being DoubleIndexedSet of K, L st for j being Element of J holds rng(F.j) is directed holds rng Infs Frege F is directed; theorem :: WAYBEL_5:28 ::Theorem 2.7 (ii) L is continuous implies for S being CLSubFrame of L holds S is continuous LATTICE; theorem :: WAYBEL_5:29 for S being non empty Poset st ex g being Function of L, S st g is infs-preserving onto holds S is complete LATTICE; notation let J be set, y be set; synonym J => y for J --> y; end; registration let J be set, y be set; cluster J => y -> total for J-defined Function; end; definition let A, B, J be set, f be Function of A, B; redefine func J => f -> ManySortedFunction of (J --> A), (J --> B); end; theorem :: WAYBEL_5:30 for A, B being set for f being Function of A, B, g being Function of B, A st g*f = id A holds (J => g)**(J => f) = id (J --> A); theorem :: WAYBEL_5:31 for J, A being non empty set, B being set, 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; theorem :: WAYBEL_5:32 for J, A, B being non empty set, 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; theorem :: WAYBEL_5:33 ::Theorem 2.7 (iii) L is continuous implies for S being non empty Poset st ex g being Function of L, S st g is infs-preserving directed-sups-preserving & g is onto holds S is continuous LATTICE;