:: More on the Algebraic and Arithmetic Lattices
:: by Robert Milewski
::
:: Received October 29, 1997
:: Copyright (c) 1997-2017 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 ORDERS_2, CAT_1, YELLOW_0, STRUCT_0, TARSKI, WELLORD1, XBOOLE_0,
FUNCT_1, FUNCT_2, RELAT_1, SUBSET_1, YELLOW_1, WAYBEL_0, XXREAL_0,
LATTICES, RELAT_2, WAYBEL_1, GROUP_6, SEQM_3, WAYBEL_8, RCOMP_1,
FINSET_1, LATTICE3, WAYBEL_3, ORDINAL2, YELLOW_2, CARD_FIL, BINOP_1,
EQREL_1, REWRITE1, WAYBEL_6, ARYTM_0, INT_2, ARYTM_3, XBOOLEAN, WAYBEL_5,
WAYBEL15;
notations TARSKI, XBOOLE_0, SUBSET_1, WELLORD1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, FINSET_1, DOMAIN_1, STRUCT_0, ORDERS_2, QUANTAL1, LATTICE3,
YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_7, WAYBEL_0, WAYBEL_1, WAYBEL_3,
WAYBEL_5, WAYBEL_6, WAYBEL_8;
constructors DOMAIN_1, TOLER_1, QUANTAL1, ORDERS_3, WAYBEL_1, WAYBEL_3,
WAYBEL_5, WAYBEL_6, WAYBEL_8, RELSET_1;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, STRUCT_0,
LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_2,
WAYBEL_3, WAYBEL_5, WAYBEL_8, WAYBEL10, SUBSET_1;
requirements SUBSET, BOOLE;
begin :: Preliminaries
theorem :: WAYBEL15:1
for R be RelStr for S be full SubRelStr of R
for T be full SubRelStr of S holds T is full SubRelStr of R;
theorem :: WAYBEL15:2
for X be set for a be Element of BoolePoset X holds uparrow a = {Y
where Y is Subset of X : a c= Y};
theorem :: WAYBEL15:3
for L be upper-bounded non empty antisymmetric RelStr for a be Element
of L holds Top L <= a implies a = Top L;
theorem :: WAYBEL15:4
for S,T be non empty Poset for g be Function of S,T for d be
Function of T,S holds g is onto & [g,d] is Galois implies T,Image d
are_isomorphic;
theorem :: WAYBEL15:5
for L1,L2,L3 be non empty Poset for g1 be Function of L1,L2 for
g2 be Function of L2,L3 for d1 be Function of L2,L1 for d2 be Function of L3,L2
st [g1,d1] is Galois & [g2,d2] is Galois holds [g2*g1,d1*d2] is Galois;
theorem :: WAYBEL15:6
for L1,L2 be non empty Poset for f be Function of L1,L2 for f1 be
Function of L2,L1 st f1 = (f qua Function)" & f is isomorphic holds [f,f1] is
Galois & [f1,f] is Galois;
theorem :: WAYBEL15:7
for X be set holds BoolePoset X is arithmetic;
registration
let X be set;
cluster BoolePoset X -> arithmetic;
end;
theorem :: WAYBEL15:8
for L1,L2 be up-complete non empty Poset for f be Function of
L1,L2 st f is isomorphic for x be Element of L1 holds f.:(waybelow x) =
waybelow f.x;
theorem :: WAYBEL15:9
for L1,L2 be non empty Poset st L1,L2 are_isomorphic & L1 is
continuous holds L2 is continuous;
theorem :: WAYBEL15:10
for L1,L2 be LATTICE st L1,L2 are_isomorphic & L1 is
lower-bounded arithmetic holds L2 is arithmetic;
theorem :: WAYBEL15:11
for L1,L2,L3 be non empty Poset for f be Function of L1,L2 for g
be Function of L2,L3 st f is directed-sups-preserving & g is
directed-sups-preserving holds g*f is directed-sups-preserving;
begin :: Maps Preserving Sup's and Inf's
theorem :: WAYBEL15:12
for L1,L2 be non empty RelStr for f be Function of L1,L2 for X be
Subset of Image f holds (inclusion f).:X = X;
theorem :: WAYBEL15:13
for X be set for c be Function of BoolePoset X,BoolePoset X st c
is idempotent directed-sups-preserving holds inclusion c is
directed-sups-preserving;
theorem :: WAYBEL15:14 :: THEOREM 2.10.
for L be continuous complete LATTICE for p be kernel Function of
L,L st p is directed-sups-preserving holds Image p is continuous LATTICE;
theorem :: WAYBEL15:15 :: THEOREM 2.14.
for L be continuous complete LATTICE for p be projection
Function of L,L st p is directed-sups-preserving holds Image p is continuous
LATTICE;
theorem :: WAYBEL15:16 :: THEOREM 4.16. (1) iff (2)
for L be lower-bounded LATTICE holds L is continuous iff ex A be
arithmetic lower-bounded LATTICE, g be Function of A,L st g is onto & g is
infs-preserving & g is directed-sups-preserving;
theorem :: WAYBEL15:17 :: THEOREM 4.16. (1) iff (3)
for L be lower-bounded LATTICE holds L is continuous iff ex A be
algebraic lower-bounded LATTICE, g be Function of A,L st g is onto & g is
infs-preserving & g is directed-sups-preserving;
theorem :: WAYBEL15:18 :: THEOREM 4.16. (1) iff (4)
for L be lower-bounded LATTICE holds ( L is continuous implies ex X be
non empty set, p be projection Function of BoolePoset X,BoolePoset X st p is
directed-sups-preserving & L,Image p are_isomorphic ) & (( ex X be set, p be
projection Function of BoolePoset X,BoolePoset X st p is
directed-sups-preserving & L,Image p are_isomorphic ) implies L is continuous )
;
begin :: Atoms Elements
theorem :: WAYBEL15:19
for L be non empty RelStr for x be Element of L holds x in PRIME (L
opp) iff x is co-prime;
definition
let L be non empty RelStr;
let a be Element of L;
attr a is atom means
:: WAYBEL15:def 1
Bottom L < a & for b be Element of L st Bottom L < b & b <= a holds b = a;
end;
definition
let L be non empty RelStr;
func ATOM L -> Subset of L means
:: WAYBEL15:def 2
for x be Element of L holds x in it iff x is atom;
end;
theorem :: WAYBEL15:20
for L be Boolean LATTICE for a be Element of L holds a is atom
iff a is co-prime & a <> Bottom L;
registration
let L be Boolean LATTICE;
cluster atom -> co-prime for Element of L;
end;
theorem :: WAYBEL15:21
for L be Boolean LATTICE holds ATOM L = (PRIME (L opp)) \ {Bottom L};
theorem :: WAYBEL15:22
for L be Boolean LATTICE for x,a be Element of L st a is atom holds a
<= x iff not a <= 'not' x;
theorem :: WAYBEL15:23
for L be complete Boolean LATTICE for X be Subset of L for x be
Element of L holds x "/\" sup X = "\/"({x"/\"y where y is Element of L: y in X}
,L);
theorem :: WAYBEL15:24
for L be lower-bounded with_infima antisymmetric non empty
RelStr for x,y be Element of L st x is atom & y is atom & x <> y holds x "/\" y
= Bottom L;
theorem :: WAYBEL15:25
for L be complete Boolean LATTICE for x be Element of L for A be
Subset of L st A c= ATOM L holds x in A iff x is atom & x <= sup A;
theorem :: WAYBEL15:26
for L be complete Boolean LATTICE for X,Y be Subset of L st X c=
ATOM L & Y c= ATOM L holds X c= Y iff sup X <= sup Y;
begin :: More on the Boolean Lattice
theorem :: WAYBEL15:27
for L be Boolean LATTICE holds L is arithmetic iff ex X be set st L,
BoolePoset X are_isomorphic;
theorem :: WAYBEL15:28 :: THEOREM 4.18. (2) iff (3)
for L be Boolean LATTICE holds L is arithmetic iff L is algebraic;
theorem :: WAYBEL15:29 :: THEOREM 4.18. (2) iff (4)
for L be Boolean LATTICE holds L is arithmetic iff L is continuous;
theorem :: WAYBEL15:30 :: THEOREM 4.18. (2) iff (5)
for L be Boolean LATTICE holds L is arithmetic iff L is continuous & L
opp is continuous;
theorem :: WAYBEL15:31 :: THEOREM 4.18. (2) iff (6)
for L be Boolean LATTICE holds L is arithmetic iff L is
completely-distributive;
theorem :: WAYBEL15:32 :: THEOREM 4.18. (2) iff (7)
for L be Boolean LATTICE holds L is arithmetic iff ( L is complete &
for x be Element of L ex X be Subset of L st X c= ATOM L & x = sup X );