The abstract of the Mizar article:

Algebraic and Arithmetic Lattices. Part II

by

Robert Milewski

Received October 29, 1997

MML identifier: WAYBEL15

[ Mizar article, MML identifier index ]

environ

 vocabulary ORDERS_1, CAT_1, YELLOW_0, WELLORD1, PRE_TOPC, SGRAPH1, FUNCT_1,
      RELAT_1, YELLOW_1, WAYBEL_0, LATTICES, RELAT_2, WAYBEL_1, GROUP_6,
      SEQM_3, WAYBEL_8, COMPTS_1, FINSET_1, BOOLE, LATTICE3, QUANTAL1,
      WAYBEL_3, ORDINAL2, YELLOW_2, FILTER_2, BINOP_1, BHSP_3, WAYBEL_6,
      OPPCAT_1, FILTER_0, ZF_LANG, WAYBEL_5, WAYBEL15;
 notation TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, WELLORD1, FUNCT_1, FUNCT_2,
      FINSET_1, STRUCT_0, ORDERS_1, PRE_TOPC, QUANTAL1, GRCAT_1, LATTICE3,
      YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_7, WAYBEL_0, WAYBEL_1, WAYBEL_3,
      WAYBEL_5, WAYBEL_6, WAYBEL_8;
 constructors ORDERS_3, TOLER_1, QUANTAL1, TOPS_2, GRCAT_1, YELLOW_3, WAYBEL_1,
      WAYBEL_3, WAYBEL_5, WAYBEL_6, WAYBEL_8;
 clusters STRUCT_0, RELSET_1, FINSET_1, FUNCT_1, LATTICE3, YELLOW_0, YELLOW_2,
      WAYBEL_0, WAYBEL_1, WAYBEL_2, WAYBEL_3, WAYBEL_5, WAYBEL_8, WAYBEL10,
      SUBSET_1, XBOOLE_0;
 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 1-sorted, Y,Z be non empty 1-sorted
   for f be map of X,Y
   for g be map of Y,Z
      holds
    f is onto & g is onto implies g*f is onto;

  theorem :: WAYBEL15:3
   for X be 1-sorted
   for Y be Subset of X holds
    (id X).:Y = Y;

  theorem :: WAYBEL15:4
     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:5
     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:6
   for S,T be non empty Poset
   for g be map of S,T
   for d be map of T,S
      holds
    g is onto & [g,d] is Galois implies T,Image d are_isomorphic;

  theorem :: WAYBEL15:7
   for L1,L2,L3 be non empty Poset
   for g1 be map of L1,L2
   for g2 be map of L2,L3
   for d1 be map of L2,L1
   for d2 be map of L3,L2
      st [g1,d1] is Galois & [g2,d2] is Galois holds
    [g2*g1,d1*d2] is Galois;

  theorem :: WAYBEL15:8
   for L1,L2 be non empty Poset
   for f be map of L1,L2
   for f1 be map of L2,L1 st f1 = (f qua Function)" & f is isomorphic holds
    [f,f1] is Galois & [f1,f] is Galois;

  theorem :: WAYBEL15:9
   for X be set holds BoolePoset X is arithmetic;

  definition
   let X be set;
   cluster BoolePoset X -> arithmetic;
  end;

  theorem :: WAYBEL15:10
   for L1,L2 be up-complete (non empty Poset)
   for f be map of L1,L2 st f is isomorphic
   for x be Element of L1 holds
    f.:(waybelow x) = waybelow f.x;

  theorem :: WAYBEL15:11
   for L1,L2 be non empty Poset
    st L1,L2 are_isomorphic & L1 is continuous holds
     L2 is continuous;

  theorem :: WAYBEL15:12
   for L1,L2 be LATTICE
    st L1,L2 are_isomorphic & L1 is lower-bounded arithmetic holds
     L2 is arithmetic;

  theorem :: WAYBEL15:13
   for L1,L2,L3 be non empty Poset
   for f be map of L1,L2
   for g be map 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:14
   for L1,L2 be non empty RelStr
   for f be map of L1,L2
   for X be Subset of Image f holds
    (inclusion f).:X = X;

  theorem :: WAYBEL15:15
   for X be set
   for c be map of BoolePoset X,BoolePoset X st
     c is idempotent directed-sups-preserving holds
    inclusion c is directed-sups-preserving;

  theorem :: WAYBEL15:16  :: THEOREM 2.10.
   for L be continuous complete LATTICE
   for p be kernel map of L,L st p is directed-sups-preserving holds
    Image p is continuous LATTICE;

  theorem :: WAYBEL15:17  :: THEOREM 2.14.
   for L be continuous complete LATTICE
   for p be projection map of L,L st p is directed-sups-preserving holds
    Image p is continuous LATTICE;

  theorem :: WAYBEL15:18  :: 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 map of A,L st
     g is onto & g is infs-preserving & g is directed-sups-preserving;

  theorem :: WAYBEL15:19  :: 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 map of A,L st
     g is onto & g is infs-preserving & g is directed-sups-preserving;

  theorem :: WAYBEL15:20  :: 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 map of BoolePoset X,BoolePoset X st
     p is directed-sups-preserving & L,Image p are_isomorphic ) &

    (( ex X be set, p be projection map 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:21
     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;

canceled;

  theorem :: WAYBEL15:23
   for L be Boolean LATTICE
   for a be Element of L holds
    a is atom iff a is co-prime & a <> Bottom L;

  definition
   let L be Boolean LATTICE;
   cluster atom -> co-prime Element of L;
  end;

  theorem :: WAYBEL15:24
     for L be Boolean LATTICE holds
    ATOM L = (PRIME (L opp)) \ {Bottom L};

  theorem :: WAYBEL15:25
     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:26
   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:27
   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:28
   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:29
   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:30  :: THEOREM 4.18. (2) iff (1)
     for L be Boolean LATTICE holds
    L is arithmetic iff ex X be set st L,BoolePoset X are_isomorphic;

  theorem :: WAYBEL15:31  :: THEOREM 4.18. (2) iff (3)
     for L be Boolean LATTICE holds
    L is arithmetic iff L is algebraic;

  theorem :: WAYBEL15:32  :: THEOREM 4.18. (2) iff (4)
     for L be Boolean LATTICE holds
    L is arithmetic iff L is continuous;

  theorem :: WAYBEL15:33  :: 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:34  :: THEOREM 4.18. (2) iff (6)
     for L be Boolean LATTICE holds
    L is arithmetic iff L is completely-distributive;

  theorem :: WAYBEL15:35  :: 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 );