The abstract of the Mizar article:

Algebraic and Arithmetic Lattices. Part I

by

Robert Milewski

Received March 4, 1997

MML identifier: WAYBEL13

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_1, RELAT_1, RELAT_2, ORDERS_1, WAYBEL_8, COMPTS_1, YELLOW_0,
      LATTICE3, FILTER_2, SUBSET_1, LATTICES, WAYBEL_0, WAYBEL_5, GROUP_6,
      WAYBEL10, YELLOW_1, FINSET_1, SETFAM_1, BHSP_3, BOOLE, CAT_1, WELLORD2,
      QUANTAL1, TARSKI, ORDINAL2, PRE_TOPC, WAYBEL_3, SEQM_3, PBOOLE, CARD_3,
      WELLORD1, WAYBEL_1, YELLOW_2;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, SETFAM_1, FINSET_1,
      STRUCT_0, RELAT_1, ORDERS_1, FUNCT_1, FUNCT_2, PRE_TOPC, PBOOLE,
      LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_0, WAYBEL_1, WAYBEL_3,
      WAYBEL_5, WAYBEL_8, WAYBEL10, GRCAT_1;
 constructors DOMAIN_1, QUANTAL1, ORDERS_3, YELLOW_3, WAYBEL_1, WAYBEL_3,
      WAYBEL_8, WAYBEL10, GRCAT_1;
 clusters STRUCT_0, FINSET_1, LATTICE3, YELLOW_0, YELLOW_2, WAYBEL_0, WAYBEL_1,
      WAYBEL_3, WAYBEL_8, WAYBEL10, RELSET_1, SUBSET_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin :: Preliminaries

  scheme LambdaCD{A()->non empty set,C[set],F(set)->set,G(set)->set}:
   ex f being Function st dom f = A() &
    for x be Element of A() holds
     (C[x] implies f.x = F(x)) & (not C[x] implies f.x = G(x));

  theorem :: WAYBEL13:1
   for L be non empty reflexive transitive RelStr
   for x,y be Element of L holds
    x <= y implies compactbelow x c= compactbelow y;

  theorem :: WAYBEL13:2
   for L be non empty reflexive RelStr
   for x be Element of L holds
    compactbelow x is Subset of CompactSublatt L;

  theorem :: WAYBEL13:3
   for L be RelStr
   for S be SubRelStr of L
   for X be Subset of S holds X is Subset of L;

  theorem :: WAYBEL13:4
   for L be with_suprema non empty reflexive transitive RelStr holds
    the carrier of L is Ideal of L;

  theorem :: WAYBEL13:5
   for L1 be lower-bounded non empty reflexive antisymmetric RelStr
   for L2 be non empty reflexive antisymmetric RelStr
    st the RelStr of L1 = the RelStr of L2 & L1 is up-complete
     holds
    the carrier of CompactSublatt L1 = the carrier of CompactSublatt L2;

begin :: Algebraic and Arithmetic Lattices

  theorem :: WAYBEL13:6  :: COROLLARY 4.10.
   for L be algebraic lower-bounded LATTICE
   for S be CLSubFrame of L holds S is algebraic;

  theorem :: WAYBEL13:7  :: EXAMPLES 4.11.(2)
   for X,E be set
   for L be CLSubFrame of BoolePoset X holds
    E in the carrier of CompactSublatt L
       iff
    ( ex F be Element of BoolePoset X st
      F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E );

  theorem :: WAYBEL13:8
   for L be lower-bounded sup-Semilattice holds
    InclPoset Ids L is CLSubFrame of BoolePoset the carrier of L;

  definition
   let L be non empty reflexive transitive RelStr;
   cluster principal Ideal of L;
  end;

  theorem :: WAYBEL13:9
   for L be lower-bounded sup-Semilattice
   for X be non empty directed Subset of InclPoset Ids L holds
    sup X = union X;

  theorem :: WAYBEL13:10   :: PROPOSITION 4.12.(i)
   for S be lower-bounded sup-Semilattice holds
    InclPoset Ids S is algebraic;

  theorem :: WAYBEL13:11   :: PROPOSITION 4.12.(i)
   for S be lower-bounded sup-Semilattice
   for x be Element of InclPoset Ids S holds
    x is compact iff x is principal Ideal of S;

  theorem :: WAYBEL13:12
   for S be lower-bounded sup-Semilattice
   for x be Element of InclPoset Ids S holds
    x is compact iff ex a be Element of S st x = downarrow a;

  theorem :: WAYBEL13:13  :: PROPOSITION 4.12.(ii)
     for L be lower-bounded sup-Semilattice
   for f be map of L, CompactSublatt InclPoset Ids L st
    for x be Element of L holds f.x = downarrow x holds
     f is isomorphic;

  theorem :: WAYBEL13:14  :: PROPOSITION 4.12.(iii)
     for S be lower-bounded LATTICE holds
    InclPoset Ids S is arithmetic;

  theorem :: WAYBEL13:15   :: PROPOSITION 4.12.(iv)
   for L be lower-bounded sup-Semilattice
    holds
    CompactSublatt L is lower-bounded sup-Semilattice;

  theorem :: WAYBEL13:16  :: PROPOSITION 4.12.(v)
   for L be algebraic lower-bounded sup-Semilattice
   for f be map of L,InclPoset Ids CompactSublatt L st
    for x be Element of L holds f.x = compactbelow x holds
     f is isomorphic;

  theorem :: WAYBEL13:17  :: PROPOSITION 4.12.(vi)
     for L be algebraic lower-bounded sup-Semilattice
   for x be Element of L holds
    compactbelow x is principal Ideal of CompactSublatt L iff x is compact;

begin :: Maps

  theorem :: WAYBEL13:18
   for L1,L2 be non empty RelStr
   for X be Subset of L1, x be Element of L1
   for f be map of L1,L2 st f is isomorphic holds
    x is_<=_than X iff f.x is_<=_than f.:X;

  theorem :: WAYBEL13:19
   for L1,L2 be non empty RelStr
   for X be Subset of L1, x be Element of L1
   for f be map of L1,L2 st f is isomorphic holds
    x is_>=_than X iff f.x is_>=_than f.:X;

  theorem :: WAYBEL13:20
   for L1,L2 be non empty antisymmetric RelStr
   for f be map of L1,L2 holds
    f is isomorphic implies f is infs-preserving sups-preserving;

  definition
   let L1,L2 be non empty antisymmetric RelStr;
   cluster isomorphic -> infs-preserving sups-preserving map of L1,L2;
  end;

  theorem :: WAYBEL13:21
   for L1,L2,L3 be non empty transitive antisymmetric RelStr
   for f be map of L1,L2 st f is infs-preserving holds
    L2 is full infs-inheriting SubRelStr of L3 & L3 is complete implies
     ex g be map of L1,L3 st f = g & g is infs-preserving;

  theorem :: WAYBEL13:22
   for L1,L2,L3 be non empty transitive antisymmetric RelStr
   for f be map of L1,L2 st f is monotone directed-sups-preserving holds
    L2 is full directed-sups-inheriting SubRelStr of L3 & L3 is complete
      implies
     ex g be map of L1,L3 st f = g & g is directed-sups-preserving;

  theorem :: WAYBEL13:23
   for L be lower-bounded sup-Semilattice holds
    InclPoset Ids CompactSublatt L is CLSubFrame of
     BoolePoset the carrier of CompactSublatt L;

  theorem :: WAYBEL13:24  :: COROLLARY 4.13.
   for L be algebraic lower-bounded LATTICE
   ex g be map of L,BoolePoset the carrier of CompactSublatt L st
    g is infs-preserving & g is directed-sups-preserving & g is one-to-one &
   for x be Element of L holds g.x = compactbelow x;

  theorem :: WAYBEL13:25 :: PROPOSITION 4.14.
     for I be non empty set
   for J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I
    st for i be Element of I holds J.i is algebraic lower-bounded LATTICE
     holds
    product J is algebraic lower-bounded LATTICE;

  theorem :: WAYBEL13:26
   for L1,L2 be non empty RelStr st the RelStr of L1 = the RelStr of L2 holds
    L1,L2 are_isomorphic;

  theorem :: WAYBEL13:27
   for L1,L2 be up-complete (non empty Poset)
   for f be map of L1,L2 st f is isomorphic
   for x,y be Element of L1 holds
    x << y iff f.x << f.y;

  theorem :: WAYBEL13:28
   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
    x is compact iff f.x is compact;

  theorem :: WAYBEL13:29
   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.:(compactbelow x) = compactbelow f.x;

  theorem :: WAYBEL13:30
   for L1,L2 be non empty Poset
    st L1,L2 are_isomorphic & L1 is up-complete
     holds L2 is up-complete;

  theorem :: WAYBEL13:31
   for L1,L2 be non empty Poset
    st L1,L2 are_isomorphic & L1 is complete satisfying_axiom_K
     holds L2 is satisfying_axiom_K;

  theorem :: WAYBEL13:32
   for L1,L2 be sup-Semilattice
    st L1,L2 are_isomorphic & L1 is lower-bounded algebraic
     holds L2 is algebraic;

  theorem :: WAYBEL13:33
     for L be continuous lower-bounded sup-Semilattice holds
    SupMap L is infs-preserving sups-preserving;

  theorem :: WAYBEL13:34  :: THEOREM 4.15. (1) iff (2)
     for L be lower-bounded LATTICE holds
    ( L is algebraic implies
    ex X be non empty set,
       S be full SubRelStr of BoolePoset X st
     S is infs-inheriting & S is directed-sups-inheriting &
      L,S are_isomorphic ) &

    (( ex X be set, S be full SubRelStr of BoolePoset X st
      S is infs-inheriting & S is directed-sups-inheriting &
      L,S are_isomorphic ) implies L is algebraic );

  theorem :: WAYBEL13:35  :: THEOREM 4.15. (1) iff (3)
     for L be lower-bounded LATTICE holds
    ( L is algebraic implies
    ex X be non empty set,
       c be closure map of BoolePoset X,BoolePoset X st
     c is directed-sups-preserving & L,Image c are_isomorphic ) &

    (( ex X be set, c be closure map of BoolePoset X,BoolePoset X st
     c is directed-sups-preserving & L,Image c are_isomorphic ) implies
     L is algebraic );