environ vocabulary WAYBEL_0, ORDERS_1, FUNCT_1, RELAT_1, FUNCT_4, QUANTAL1, RELAT_2, ORDINAL2, LATTICES, REALSET1, PRE_TOPC, YELLOW_0, BHSP_3, FUNCOP_1, BOOLE, LATTICE3, SEQM_3, WAYBEL_2, WAYBEL_3, TARSKI, FILTER_0, SUBSET_1, ORDERS_2, ZFMISC_1, FINSET_1, YELLOW_1, FUNCT_3, FRAENKEL, LATTICE2, OPPCAT_1, WAYBEL_5, ZF_REFLE, PBOOLE, YELLOW_2, FUNCT_6, CARD_3, PRALG_1, FINSEQ_4, WAYBEL_6, HAHNBAN; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, NAT_1, FINSET_1, RELAT_1, ORDINAL1, RELAT_2, REALSET1, STRUCT_0, ORDERS_1, PRE_TOPC, CARD_3, FRAENKEL, LATTICE3, FUNCT_1, FUNCT_2, FUNCT_3, FUNCT_6, PBOOLE, PRALG_1, PRALG_2, YELLOW_0, YELLOW_1, WAYBEL_0, WAYBEL_1, YELLOW_2, YELLOW_4, WAYBEL_2, WAYBEL_3, WAYBEL_4, WAYBEL_5, BORSUK_1, YELLOW_7, FUNCT_7; constructors WAYBEL_5, WAYBEL_4, NAT_1, RELAT_2, BORSUK_1, YELLOW_4, ORDERS_3, WAYBEL_1, WAYBEL_2, WAYBEL_3, PRALG_2, FUNCT_7, MEMBERED; clusters SUBSET_1, WAYBEL_0, WAYBEL_2, WAYBEL_3, YELLOW_0, STRUCT_0, ORDERS_1, LATTICE3, PBOOLE, FINSET_1, WAYBEL_1, WAYBEL_5, PRALG_1, YELLOW_7, YELLOW_4, RELSET_1, ARYTM_3, XBOOLE_0, FRAENKEL, MEMBERED, ZFMISC_1, FUNCT_2, PARTFUN1; requirements NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve x,y,Y,Z for set, L for LATTICE, l for Element of L, n,k for Nat; :: Preliminaries scheme NonUniqExD1 { Z() ->non empty RelStr, X() -> Subset of Z(), Y() -> non empty Subset of Z(), P[set,set] }: ex f being Function of X(),Y() st for e be Element of Z() st e in X() ex u be Element of Z() st u in Y() & u = f.e & P[e,u] provided for e be Element of Z() st e in X() ex u be Element of Z() st u in Y() & P[e,u]; definition let L be LATTICE; let A be non empty Subset of L; let f be Function of A,A; let n be Element of NAT; redefine func iter (f,n) -> Function of A,A; end; definition let L be LATTICE; let C,D be non empty Subset of L; let f be Function of C,D; let c be Element of C; redefine func f.c -> Element of L; end; definition let L be non empty Poset; cluster -> filtered directed Chain of L; end; definition cluster strict continuous distributive lower-bounded LATTICE; end; theorem :: WAYBEL_6:1 for S,T being Semilattice, f being map of S,T holds f is meet-preserving iff for x,y being Element of S holds f.(x "/\" y) = f. x "/\" f.y; theorem :: WAYBEL_6:2 for S,T being sup-Semilattice, f being map of S,T holds f is join-preserving iff for x,y being Element of S holds f.(x "\/" y) = f. x "\/" f.y; theorem :: WAYBEL_6:3 for S,T being LATTICE, f being map of S,T st T is distributive & f is meet-preserving join-preserving one-to-one holds S is distributive; definition let S,T be complete LATTICE; cluster sups-preserving map of S,T; end; theorem :: WAYBEL_6:4 for S,T being complete LATTICE, f being sups-preserving map of S,T st T is meet-continuous & f is meet-preserving one-to-one holds S is meet-continuous; begin :: Open sets definition ::def 3.1, p.68 let L be non empty reflexive RelStr, X be Subset of L; attr X is Open means :: WAYBEL_6:def 1 for x be Element of L st x in X ex y be Element of L st y in X & y << x; end; theorem :: WAYBEL_6:5 for L be up-complete LATTICE, X be upper Subset of L holds X is Open iff for x be Element of L st x in X holds waybelow x meets X; theorem :: WAYBEL_6:6 ::3.2, p.68 for L be up-complete LATTICE, X be upper Subset of L holds X is Open iff X = union {wayabove x where x is Element of L : x in X}; definition let L be up-complete lower-bounded LATTICE; cluster Open Filter of L; end; theorem :: WAYBEL_6:7 for L be lower-bounded continuous LATTICE, x be Element of L holds (wayabove x) is Open; theorem :: WAYBEL_6:8 ::3.3, p.68 for L be lower-bounded continuous LATTICE, x,y be Element of L st x << y holds ex F be Open Filter of L st y in F & F c= wayabove x; theorem :: WAYBEL_6:9 ::3.4, p.69 for L being complete LATTICE, X being Open upper Subset of L holds for x being Element of L st x in (X`) ex m being Element of L st x <= m & m is_maximal_in (X`); begin :: Irreducible elements definition ::def 3.5, p.69 let G be non empty RelStr, g be Element of G; attr g is meet-irreducible means :: WAYBEL_6:def 2 for x,y being Element of G st g = x "/\" y holds x = g or y = g; synonym g is irreducible; end; definition let G be non empty RelStr, g be Element of G; attr g is join-irreducible means :: WAYBEL_6:def 3 for x,y being Element of G st g = x "\/" y holds x = g or y = g; end; definition let L be non empty RelStr; func IRR L -> Subset of L means :: WAYBEL_6:def 4 for x be Element of L holds x in it iff x is irreducible; end; theorem :: WAYBEL_6:10 for L being upper-bounded antisymmetric with_infima non empty RelStr holds Top L is irreducible; definition let L be upper-bounded antisymmetric with_infima non empty RelStr; cluster irreducible Element of L; end; theorem :: WAYBEL_6:11 for L being Semilattice, x being Element of L holds x is irreducible iff for A being finite non empty Subset of L st x = inf A holds x in A; theorem :: WAYBEL_6:12 for L be LATTICE,l be Element of L st (uparrow l \ {l}) is Filter of L holds l is irreducible; theorem :: WAYBEL_6:13 ::3.6, p.69 for L be LATTICE, p be Element of L, F be Filter of L st p is_maximal_in (F`) holds p is irreducible; theorem :: WAYBEL_6:14 ::3.7, p.69 for L be lower-bounded continuous LATTICE, x,y be Element of L st not y <= x holds ex p be Element of L st p is irreducible & x <= p & not y <= p; begin :: Order generating sets definition ::def 3.8, p.70 let L be non empty RelStr, X be Subset of L; attr X is order-generating means :: WAYBEL_6:def 5 for x be Element of L holds ex_inf_of (uparrow x) /\ X,L & x = inf ((uparrow x) /\ X); end; theorem :: WAYBEL_6:15 ::3.9 (1-2), p.70 for L be up-complete lower-bounded LATTICE, X be Subset of L holds X is order-generating iff for l being Element of L ex Y be Subset of X st l = "/\" (Y,L); theorem :: WAYBEL_6:16 ::3.9 (1-3), p.70 for L be up-complete lower-bounded LATTICE, X be Subset of L holds X is order-generating iff for Y be Subset of L st X c= Y & for Z be Subset of Y holds "/\" (Z,L) in Y holds the carrier of L = Y; theorem :: WAYBEL_6:17 ::3.9 (1-4), p.70 for L be up-complete lower-bounded LATTICE, X be Subset of L holds X is order-generating iff (for l1,l2 be Element of L st not l2 <= l1 ex p be Element of L st p in X & l1 <= p & not l2 <= p); theorem :: WAYBEL_6:18 ::3.10, p.70 for L be lower-bounded continuous LATTICE, X be Subset of L st X = IRR L \ { Top L} holds X is order-generating; theorem :: WAYBEL_6:19 for L being lower-bounded continuous LATTICE, X,Y being Subset of L st X is order-generating & X c= Y holds Y is order-generating; begin :: Prime elements definition ::def 3.11, p.70 let L be non empty RelStr; let l be Element of L; attr l is prime means :: WAYBEL_6:def 6 for x,y be Element of L st x "/\" y <= l holds x <= l or y <= l; end; definition let L be non empty RelStr; func PRIME L -> Subset of L means :: WAYBEL_6:def 7 for x be Element of L holds x in it iff x is prime; end; definition let L be non empty RelStr; let l be Element of L; attr l is co-prime means :: WAYBEL_6:def 8 l~ is prime; end; theorem :: WAYBEL_6:20 for L being upper-bounded antisymmetric non empty RelStr holds Top L is prime; theorem :: WAYBEL_6:21 for L being lower-bounded antisymmetric non empty RelStr holds Bottom L is co-prime; definition let L be upper-bounded antisymmetric non empty RelStr; cluster prime Element of L; end; theorem :: WAYBEL_6:22 for L being Semilattice, l being Element of L holds l is prime iff for A being finite non empty Subset of L st l >= inf A ex a being Element of L st a in A & l >= a; theorem :: WAYBEL_6:23 for L being sup-Semilattice, x being Element of L holds x is co-prime iff for A being finite non empty Subset of L st x <= sup A ex a being Element of L st a in A & x <= a; theorem :: WAYBEL_6:24 for L being LATTICE, l being Element of L st l is prime holds l is irreducible; theorem :: WAYBEL_6:25 ::3.12 (1-2), p.70 for l holds l is prime iff for x being set, f being map of L,BoolePoset {x} st (for p be Element of L holds f.p = {} iff p <= l) holds f is meet-preserving join-preserving; theorem :: WAYBEL_6:26 ::3.12 (1-3), p.70 for L being upper-bounded LATTICE, l being Element of L st l <> Top L holds l is prime iff (downarrow l)` is Filter of L; theorem :: WAYBEL_6:27 ::3.12 (1-4), p.70 for L being distributive LATTICE for l being Element of L holds l is prime iff l is irreducible; theorem :: WAYBEL_6:28 for L being distributive LATTICE holds PRIME L = IRR L; theorem :: WAYBEL_6:29 ::3.12 (1-5), p.70 for L being Boolean LATTICE for l being Element of L st l <> Top L holds l is prime iff for x be Element of L st x > l holds x = Top L; theorem :: WAYBEL_6:30 ::3.12 (1-6), p.70 for L being continuous distributive lower-bounded LATTICE for l being Element of L st l <> Top L holds l is prime iff ex F being Open Filter of L st l is_maximal_in (F`); theorem :: WAYBEL_6:31 for L being RelStr, X being Subset of L holds chi(X, the carrier of L) is map of L, BoolePoset {{}}; theorem :: WAYBEL_6:32 for L being non empty RelStr, p,x being Element of L holds chi((downarrow p)`,the carrier of L).x = {} iff x <= p; theorem :: WAYBEL_6:33 for L being upper-bounded LATTICE, f being map of L,BoolePoset {{}}, p being prime Element of L st chi((downarrow p)`,the carrier of L) = f holds f is meet-preserving join-preserving; theorem :: WAYBEL_6:34 ::3.13, p.71 for L being complete LATTICE st PRIME L is order-generating holds L is distributive meet-continuous; theorem :: WAYBEL_6:35 ::3.14 (1-3), p.71 for L being lower-bounded continuous LATTICE holds L is distributive iff PRIME L is order-generating; theorem :: WAYBEL_6:36 ::3.14 (1-2), p.71 for L being lower-bounded continuous LATTICE holds L is distributive iff L is Heyting; theorem :: WAYBEL_6:37 for L being continuous complete LATTICE st for l being Element of L ex X being Subset of L st l = sup X & for x being Element of L st x in X holds x is co-prime for l being Element of L holds l = "\/"((waybelow l) /\ PRIME(L opp), L); theorem :: WAYBEL_6:38 ::3.15 (2-1), p.72 for L being complete LATTICE holds L is completely-distributive iff L is continuous & for l being Element of L ex X being Subset of L st l = sup X & for x being Element of L st x in X holds x is co-prime; theorem :: WAYBEL_6:39 ::3.15 (2-3), p.72 for L being complete LATTICE holds L is completely-distributive iff L is distributive continuous & L opp is continuous;