Volume 8, 1996

University of Bialystok

Copyright (c) 1996 Association of Mizar Users

### The abstract of the Mizar article:

### Meet -- Continuous Lattices

**by****Artur Kornilowicz**- Received October 10, 1996
- MML identifier: WAYBEL_2

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCT_1, RELAT_1, RELAT_2, LATTICE3, ORDERS_1, SUBSET_1, QUANTAL1, BOOLE, WAYBEL_0, YELLOW_0, LATTICES, ORDINAL2, FUNCT_5, TARSKI, MCART_1, PRE_TOPC, SEQM_3, REALSET1, BHSP_3, FINSET_1, WELLORD1, CAT_1, YELLOW_2, FINSUB_1, WELLORD2, YELLOW_1, FILTER_2, LATTICE2, WAYBEL_1, WAYBEL_2; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELSET_1, FINSUB_1, FUNCT_1, TOLER_1, FINSET_1, PARTFUN1, FUNCT_2, PRE_TOPC, STRUCT_0, REALSET1, ORDERS_1, ORDERS_3, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, YELLOW_3, YELLOW_4; constructors FINSUB_1, ORDERS_3, YELLOW_3, YELLOW_4, WAYBEL_1, TOLER_1, MEMBERED, PRE_TOPC; clusters STRUCT_0, LATTICE3, FINSET_1, WAYBEL_0, YELLOW_0, YELLOW_2, YELLOW_3, YELLOW_4, WAYBEL_1, RELSET_1, FINSUB_1, SUBSET_1, RELAT_1, FUNCT_2, PARTFUN1; requirements SUBSET, BOOLE; begin :: Preliminaries definition let X, Y be non empty set, f be Function of X, Y, Z be non empty Subset of X; cluster f.:Z -> non empty; end; definition cluster reflexive connected -> with_infima with_suprema (non empty RelStr); end; definition let C be Chain; cluster [#]C -> directed; end; theorem :: WAYBEL_2:1 for L being up-complete Semilattice for D being non empty directed Subset of L, x being Element of L holds ex_sup_of {x} "/\" D,L; theorem :: WAYBEL_2:2 for L being up-complete sup-Semilattice for D being non empty directed Subset of L, x being Element of L holds ex_sup_of {x} "\/" D,L; theorem :: WAYBEL_2:3 for L being up-complete sup-Semilattice for A, B being non empty directed Subset of L holds A is_<=_than sup (A "\/" B); theorem :: WAYBEL_2:4 for L being up-complete sup-Semilattice for A, B being non empty directed Subset of L holds sup (A "\/" B) = sup A "\/" sup B; theorem :: WAYBEL_2:5 for L being up-complete Semilattice for D being non empty directed Subset of [:L,L:] holds { sup ({x} "/\" proj2 D) where x is Element of L : x in proj1 D } = { sup X where X is non empty directed Subset of L: ex x being Element of L st X = {x} "/\" proj2 D & x in proj1 D }; theorem :: WAYBEL_2:6 for L being Semilattice, D being non empty directed Subset of [:L,L:] holds union {X where X is non empty directed Subset of L: ex x being Element of L st X = {x} "/\" proj2 D & x in proj1 D} = proj1 D "/\" proj2 D; theorem :: WAYBEL_2:7 for L being up-complete Semilattice for D being non empty directed Subset of [:L,L:] holds ex_sup_of union {X where X is non empty directed Subset of L: ex x being Element of L st X = {x} "/\" proj2 D & x in proj1 D},L; theorem :: WAYBEL_2:8 for L being up-complete Semilattice for D being non empty directed Subset of [:L,L:] holds ex_sup_of {sup X where X is non empty directed Subset of L: ex x being Element of L st X = {x} "/\" proj2 D & x in proj1 D},L; theorem :: WAYBEL_2:9 for L being up-complete Semilattice for D being non empty directed Subset of [:L,L:] holds "\/" ({ sup X where X is non empty directed Subset of L: ex x being Element of L st X = {x} "/\" proj2 D & x in proj1 D },L) <= "\/" (union {X where X is non empty directed Subset of L: ex x being Element of L st X = {x} "/\" proj2 D & x in proj1 D},L); theorem :: WAYBEL_2:10 for L being up-complete Semilattice for D being non empty directed Subset of [:L,L:] holds "\/" ({ sup X where X is non empty directed Subset of L: ex x being Element of L st X = {x} "/\" proj2 D & x in proj1 D},L) = "\/" (union {X where X is non empty directed Subset of L: ex x being Element of L st X = {x} "/\" proj2 D & x in proj1 D},L); definition let S, T be up-complete (non empty reflexive RelStr); cluster [:S,T:] -> up-complete; end; theorem :: WAYBEL_2:11 for S, T being non empty reflexive antisymmetric RelStr st [:S,T:] is up-complete holds S is up-complete & T is up-complete; theorem :: WAYBEL_2:12 for L being up-complete antisymmetric (non empty reflexive RelStr) for D being non empty directed Subset of [:L,L:] holds sup D = [sup proj1 D,sup proj2 D]; theorem :: WAYBEL_2:13 for S1, S2 being RelStr, D being Subset of S1 for f being map of S1,S2 st f is monotone holds f.:(downarrow D) c= downarrow (f.:D); theorem :: WAYBEL_2:14 for S1, S2 being RelStr, D being Subset of S1 for f being map of S1,S2 st f is monotone holds f.:(uparrow D) c= uparrow (f.:D); definition cluster trivial -> distributive complemented (non empty reflexive RelStr); end; definition cluster strict non empty trivial LATTICE; end; theorem :: WAYBEL_2:15 for H being distributive complete LATTICE for a being Element of H, X being finite Subset of H holds sup ({a} "/\" X) = a "/\" sup X; theorem :: WAYBEL_2:16 for H being distributive complete LATTICE for a being Element of H, X being finite Subset of H holds inf ({a} "\/" X) = a "\/" inf X; theorem :: WAYBEL_2:17 for H being complete distributive LATTICE, a being Element of H for X being finite Subset of H holds a "/\" preserves_sup_of X; begin :: The Properties of Nets scheme ExNet { L() -> non empty RelStr, N() -> prenet of L(), F(set) -> Element of L()} : ex M being prenet of L() st the RelStr of M = the RelStr of N() & for i being Element of M holds (the mapping of M).i = F((the mapping of N()).i); theorem :: WAYBEL_2:18 for L being non empty RelStr for N being prenet of L st N is eventually-directed holds rng netmap (N,L) is directed; theorem :: WAYBEL_2:19 for L being non empty reflexive RelStr, D being non empty directed Subset of L for n being Function of D, the carrier of L holds NetStr (#D,(the InternalRel of L)|_2 D,n#) is prenet of L; theorem :: WAYBEL_2:20 for L being non empty reflexive RelStr, D being non empty directed Subset of L for n being Function of D, the carrier of L, N being prenet of L st n = id D & N = NetStr (#D,(the InternalRel of L)|_2 D,n#) holds N is eventually-directed ; definition let L be non empty RelStr, N be NetStr over L; func sup N -> Element of L equals :: WAYBEL_2:def 1 Sup the mapping of N; end; definition let L be non empty RelStr, J be set, f be Function of J,the carrier of L; func FinSups f -> prenet of L means :: WAYBEL_2:def 2 ex g being Function of Fin J, the carrier of L st for x being Element of Fin J holds g.x = sup (f.:x) & it = NetStr (# Fin J, RelIncl Fin J, g #); end; theorem :: WAYBEL_2:21 for L being non empty RelStr, J, x being set for f being Function of J,the carrier of L holds x is Element of FinSups f iff x is Element of Fin J; definition let L be complete antisymmetric (non empty reflexive RelStr), J be set, f be Function of J,the carrier of L; cluster FinSups f -> monotone; end; definition let L be non empty RelStr, x be Element of L, N be non empty NetStr over L; func x "/\" N -> strict NetStr over L means :: WAYBEL_2:def 3 the RelStr of it = the RelStr of N & for i being Element of it ex y being Element of L st y = (the mapping of N).i & (the mapping of it).i = x "/\" y; end; theorem :: WAYBEL_2:22 for L being non empty RelStr, N being non empty NetStr over L for x being Element of L, y being set holds y is Element of N iff y is Element of x "/\" N; definition let L be non empty RelStr, x be Element of L, N be non empty NetStr over L; cluster x "/\" N -> non empty; end; definition let L be non empty RelStr, x be Element of L, N be prenet of L; cluster x "/\" N -> directed; end; theorem :: WAYBEL_2:23 for L being non empty RelStr, x being Element of L for F being non empty NetStr over L holds rng (the mapping of x "/\" F) = {x} "/\" rng the mapping of F; theorem :: WAYBEL_2:24 for L being non empty RelStr, J being set for f being Function of J,the carrier of L st for x being set holds ex_sup_of f.:x,L holds rng netmap(FinSups f,L) c= finsups rng f; theorem :: WAYBEL_2:25 for L being non empty reflexive antisymmetric RelStr, J being set for f being Function of J,the carrier of L holds rng f c= rng netmap (FinSups f,L); theorem :: WAYBEL_2:26 for L being non empty reflexive antisymmetric RelStr, J being set for f being Function of J,the carrier of L st ex_sup_of rng f,L & ex_sup_of rng netmap (FinSups f,L),L & for x being Element of Fin J holds ex_sup_of f.:x,L holds Sup f = sup FinSups f; theorem :: WAYBEL_2:27 for L being with_infima antisymmetric transitive RelStr, N being prenet of L for x being Element of L st N is eventually-directed holds x "/\" N is eventually-directed; theorem :: WAYBEL_2:28 for L being up-complete Semilattice st for x being Element of L, E being non empty directed Subset of L st x <= sup E holds x <= sup ({x} "/\" E) holds for D being non empty directed Subset of L, x being Element of L holds x "/\" sup D = sup ({x} "/\" D); theorem :: WAYBEL_2:29 for L being with_suprema Poset st for X being directed Subset of L, x being Element of L holds x "/\" sup X = sup ({x} "/\" X) holds for X being Subset of L, x being Element of L st ex_sup_of X,L holds x "/\" sup X = sup ({x} "/\" finsups X); theorem :: WAYBEL_2:30 for L being up-complete LATTICE st for X being Subset of L, x being Element of L holds x "/\" sup X = sup ({x} "/\" finsups X) holds for X being non empty directed Subset of L, x being Element of L holds x "/\" sup X = sup ({x} "/\" X); begin :: On the inf and sup operation definition let L be non empty RelStr; func inf_op L -> map of [:L,L:], L means :: WAYBEL_2:def 4 for x, y being Element of L holds it.[x,y] = x "/\" y; end; theorem :: WAYBEL_2:31 for L being non empty RelStr, x being Element of [:L,L:] holds (inf_op L).x = x`1 "/\" x`2; definition let L be with_infima transitive antisymmetric RelStr; cluster inf_op L -> monotone; end; theorem :: WAYBEL_2:32 for S being non empty RelStr, D1, D2 being Subset of S holds (inf_op S).:[:D1,D2:] = D1 "/\" D2; theorem :: WAYBEL_2:33 for L being up-complete Semilattice for D being non empty directed Subset of [:L,L:] holds sup ((inf_op L).:D) = sup (proj1 D "/\" proj2 D); definition let L be non empty RelStr; func sup_op L -> map of [:L,L:], L means :: WAYBEL_2:def 5 for x, y being Element of L holds it.[x,y] = x "\/" y; end; theorem :: WAYBEL_2:34 for L being non empty RelStr, x being Element of [:L,L:] holds (sup_op L).x = x`1 "\/" x`2; definition let L be with_suprema transitive antisymmetric RelStr; cluster sup_op L -> monotone; end; theorem :: WAYBEL_2:35 for S being non empty RelStr, D1, D2 being Subset of S holds (sup_op S).:[:D1,D2:] = D1 "\/" D2; theorem :: WAYBEL_2:36 for L being complete (non empty Poset) for D being non empty filtered Subset of [:L,L:] holds inf ((sup_op L).:D) = inf (proj1 D "\/" proj2 D); begin :: Meet-continuous lattices :: Def 4.1, s.30 definition let R be non empty reflexive RelStr; attr R is satisfying_MC means :: WAYBEL_2:def 6 for x being Element of R, D being non empty directed Subset of R holds x "/\" sup D = sup ({x} "/\" D); end; definition let R be non empty reflexive RelStr; attr R is meet-continuous means :: WAYBEL_2:def 7 R is up-complete satisfying_MC; end; definition cluster trivial -> satisfying_MC (non empty reflexive RelStr); end; definition cluster meet-continuous -> up-complete satisfying_MC (non empty reflexive RelStr); cluster up-complete satisfying_MC -> meet-continuous (non empty reflexive RelStr); end; definition cluster strict non empty trivial LATTICE; end; theorem :: WAYBEL_2:37 for S being non empty reflexive RelStr st for X being Subset of S, x being Element of S holds x "/\" sup X = "\/"({x"/\"y where y is Element of S: y in X},S) holds S is satisfying_MC; :: Th 4.2, s.30, 1 => 2 theorem :: WAYBEL_2:38 for L being up-complete Semilattice st SupMap L is meet-preserving holds for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2); definition let L be up-complete sup-Semilattice; cluster SupMap L -> join-preserving; end; :: Th 4.2, s.30, 2 => 1 theorem :: WAYBEL_2:39 for L being up-complete Semilattice st for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) holds SupMap L is meet-preserving; :: Th 4.2, s.30, 2 => 3 theorem :: WAYBEL_2:40 for L being up-complete Semilattice st for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) holds for D1, D2 be directed non empty Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2); :: Th 4.2, s.30, 4 => 7 theorem :: WAYBEL_2:41 for L being non empty reflexive RelStr st L is satisfying_MC holds for x being Element of L, N being non empty prenet of L st N is eventually-directed holds x "/\" sup N = sup ({x} "/\" rng netmap (N,L)); :: Th 4.2, s.30, 7 => 4 theorem :: WAYBEL_2:42 for L being non empty reflexive RelStr st for x being Element of L, N being prenet of L st N is eventually-directed holds x "/\" sup N = sup ({x} "/\" rng netmap (N,L)) holds L is satisfying_MC; :: Th 4.2, s.30, 6 => 3 theorem :: WAYBEL_2:43 for L being up-complete antisymmetric (non empty reflexive RelStr) st inf_op L is directed-sups-preserving holds for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2); :: Th 4.2, s.30, 3 => 4 theorem :: WAYBEL_2:44 for L being non empty reflexive antisymmetric RelStr st for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) holds L is satisfying_MC; :: Th 4.2, s.30, MC => 5 theorem :: WAYBEL_2:45 for L being satisfying_MC with_infima antisymmetric (non empty reflexive RelStr) holds for x being Element of L, D being non empty directed Subset of L st x <= sup D holds x = sup ({x} "/\" D); :: Th 4.2, s.30, 5 => 6 theorem :: WAYBEL_2:46 for L being up-complete Semilattice st for x being Element of L, E being non empty directed Subset of L st x <= sup E holds x <= sup ({x} "/\" E) holds inf_op L is directed-sups-preserving; :: Th 4.2, s.30, 7 => 8 theorem :: WAYBEL_2:47 for L being complete antisymmetric (non empty reflexive RelStr) st for x being Element of L, N being prenet of L st N is eventually-directed holds x "/\" sup N = sup ({x} "/\" rng netmap (N,L)) holds for x being Element of L, J being set, f being Function of J,the carrier of L holds x "/\" Sup f = sup(x "/\" FinSups f); :: Th 4.2, s.30, 8 => 7 theorem :: WAYBEL_2:48 for L being complete Semilattice st for x being Element of L, J being set, f being Function of J,the carrier of L holds x "/\" Sup f = sup (x "/\" FinSups f) holds for x being Element of L, N being prenet of L st N is eventually-directed holds x "/\" sup N = sup ({x} "/\" rng netmap (N,L)); :: Th 4.2, s.30, 4 <=> 1 theorem :: WAYBEL_2:49 for L being up-complete LATTICE holds L is meet-continuous iff SupMap L is meet-preserving join-preserving; definition let L be meet-continuous LATTICE; cluster SupMap L -> meet-preserving join-preserving; end; :: Th 4.2, s.30, 4 <=> 2 theorem :: WAYBEL_2:50 for L being up-complete LATTICE holds L is meet-continuous iff for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2); :: Th 4.2, s.30, 4 <=> 3 theorem :: WAYBEL_2:51 for L being up-complete LATTICE holds L is meet-continuous iff for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2); :: Th 4.2, s.30, 4 <=> 5 theorem :: WAYBEL_2:52 for L being up-complete LATTICE holds L is meet-continuous iff for x being Element of L, D being non empty directed Subset of L st x <= sup D holds x = sup ({x} "/\" D); :: Th 4.2, s.30, 4 <=> 6 theorem :: WAYBEL_2:53 for L being up-complete Semilattice holds L is meet-continuous iff inf_op L is directed-sups-preserving; definition let L be meet-continuous Semilattice; cluster inf_op L -> directed-sups-preserving; end; :: Th 4.2, s.30, 4 <=> 7 theorem :: WAYBEL_2:54 for L being up-complete Semilattice holds L is meet-continuous iff for x being Element of L, N being non empty prenet of L st N is eventually-directed holds x "/\" sup N = sup ({x} "/\" rng netmap (N,L)); :: Th 4.2, s.30, 4 <=> 8 theorem :: WAYBEL_2:55 for L being complete Semilattice holds L is meet-continuous iff for x being Element of L, J being set for f being Function of J,the carrier of L holds x "/\" Sup f = sup(x "/\" FinSups f); definition let L be meet-continuous Semilattice, x be Element of L; cluster x "/\" -> directed-sups-preserving; end; :: Remark 4.3 s.31 theorem :: WAYBEL_2:56 for H being complete (non empty Poset) holds H is Heyting iff H is meet-continuous distributive; definition cluster complete Heyting -> meet-continuous distributive (non empty Poset); cluster complete meet-continuous distributive -> Heyting (non empty Poset); end;

Back to top