Journal of Formalized Mathematics
Volume 10, 1998
University of Bialystok
Copyright (c) 1998 Association of Mizar Users

The abstract of the Mizar article:

Bases of Continuous Lattices

by
Robert Milewski

Received November 28, 1998

MML identifier: WAYBEL23
[ Mizar article, MML identifier index ]


environ

 vocabulary ORDERS_1, WAYBEL_8, WAYBEL_3, BOOLE, WAYBEL_0, COMPTS_1, RELAT_2,
      YELLOW_1, TARSKI, FILTER_2, YELLOW_0, ORDINAL2, LATTICE3, LATTICES,
      FINSET_1, CAT_1, BHSP_3, QUANTAL1, FILTER_0, PRE_TOPC, CARD_1, SETFAM_1,
      ORDINAL1, SUBSET_1, REALSET1, FUNCT_1, WELLORD2, RELAT_1, SEQM_3,
      YELLOW_2, WAYBEL_1, WELLORD1, SGRAPH1, WAYBEL23, RLVECT_3;
 notation TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, REALSET1, FUNCT_1,
      STRUCT_0, FUNCT_2, FINSET_1, ORDINAL1, ORDINAL2, CARD_1, PRE_TOPC,
      ORDERS_1, CANTOR_1, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_0,
      WAYBEL_1, WAYBEL_3, WAYBEL_8;
 constructors TOPS_2, CANTOR_1, LATTICE3, ORDERS_3, YELLOW_3, WAYBEL_1,
      WAYBEL_3, WAYBEL_8;
 clusters STRUCT_0, FINSET_1, CARD_1, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2,
      WAYBEL_0, WAYBEL_3, WAYBEL_7, WAYBEL_8, WAYBEL14, RELSET_1, SUBSET_1,
      XBOOLE_0;
 requirements SUBSET, BOOLE;


begin  :: Preliminaries

  theorem :: WAYBEL23:1
   for L be non empty Poset
   for x be Element of L holds
    compactbelow x = waybelow x /\ the carrier of CompactSublatt L;

  definition
   let L be non empty reflexive transitive RelStr;
   let X be Subset of InclPoset Ids L;
   redefine func union X -> Subset of L;
  end;

  theorem :: WAYBEL23:2
   for L be non empty RelStr
   for X,Y be Subset of L st X c= Y holds
    finsups X c= finsups Y;

  theorem :: WAYBEL23:3
   for L be non empty transitive RelStr
   for S be sups-inheriting non empty full SubRelStr of L
   for X be Subset of L
   for Y be Subset of S st X = Y holds
    finsups X c= finsups Y;

  theorem :: WAYBEL23:4
     for L be complete transitive antisymmetric (non empty RelStr)
   for S be sups-inheriting non empty full SubRelStr of L
   for X be Subset of L
   for Y be Subset of S st X = Y holds
    finsups X = finsups Y;

  theorem :: WAYBEL23:5
   for L be complete sup-Semilattice
   for S be join-inheriting non empty full SubRelStr of L
    st Bottom L in the carrier of S
   for X be Subset of L
   for Y be Subset of S st X = Y holds
    finsups Y c= finsups X;

  theorem :: WAYBEL23:6
   for L be lower-bounded sup-Semilattice
   for X be Subset of InclPoset Ids L holds
    sup X = downarrow finsups union X;

  theorem :: WAYBEL23:7
   for L be reflexive transitive RelStr
   for X be Subset of L holds
    downarrow downarrow X = downarrow X;

  theorem :: WAYBEL23:8
     for L be reflexive transitive RelStr
   for X be Subset of L holds
    uparrow uparrow X = uparrow X;

  theorem :: WAYBEL23:9
     for L be non empty reflexive transitive RelStr
   for x be Element of L holds
    downarrow downarrow x = downarrow x;

  theorem :: WAYBEL23:10
     for L be non empty reflexive transitive RelStr
   for x be Element of L holds
    uparrow uparrow x = uparrow x;

  theorem :: WAYBEL23:11
   for L be non empty RelStr
   for S be non empty SubRelStr of L
   for X be Subset of L
   for Y be Subset of S st X = Y holds
    downarrow Y c= downarrow X;

  theorem :: WAYBEL23:12
   for L be non empty RelStr
   for S be non empty SubRelStr of L
   for X be Subset of L
   for Y be Subset of S st X = Y holds
    uparrow Y c= uparrow X;

  theorem :: WAYBEL23:13
     for L be non empty RelStr
   for S be non empty SubRelStr of L
   for x be Element of L
   for y be Element of S st x = y holds
    downarrow y c= downarrow x;

  theorem :: WAYBEL23:14
     for L be non empty RelStr
   for S be non empty SubRelStr of L
   for x be Element of L
   for y be Element of S st x = y holds
    uparrow y c= uparrow x;

begin  :: Relational Subsets

  definition
   let L be non empty RelStr;
   let S be Subset of L;
   attr S is meet-closed means
:: WAYBEL23:def 1
    subrelstr S is meet-inheriting;
  end;

  definition
   let L be non empty RelStr;
   let S be Subset of L;
   attr S is join-closed means
:: WAYBEL23:def 2
    subrelstr S is join-inheriting;
  end;

  definition
   let L be non empty RelStr;
   let S be Subset of L;
   attr S is infs-closed means
:: WAYBEL23:def 3
    subrelstr S is infs-inheriting;
  end;

  definition
   let L be non empty RelStr;
   let S be Subset of L;
   attr S is sups-closed means
:: WAYBEL23:def 4
    subrelstr S is sups-inheriting;
  end;

  definition
   let L be non empty RelStr;
   cluster infs-closed -> meet-closed Subset of L;
   cluster sups-closed -> join-closed Subset of L;
  end;

  definition
   let L be non empty RelStr;
   cluster infs-closed sups-closed non empty Subset of L;
  end;

  theorem :: WAYBEL23:15
   for L be non empty RelStr
   for S be Subset of L holds
    S is meet-closed iff
    for x,y be Element of L st x in S & y in S & ex_inf_of {x,y},L
     holds inf {x,y} in S;

  theorem :: WAYBEL23:16
   for L be non empty RelStr
   for S be Subset of L holds
    S is join-closed iff
    for x,y be Element of L st x in S & y in S & ex_sup_of {x,y},L
     holds sup {x,y} in S;

  theorem :: WAYBEL23:17
     for L be antisymmetric with_infima RelStr
   for S be Subset of L holds
    S is meet-closed iff
    for x,y be Element of L st x in S & y in S holds inf {x,y} in S;

  theorem :: WAYBEL23:18
   for L be antisymmetric with_suprema RelStr
   for S be Subset of L holds
    S is join-closed iff
    for x,y be Element of L st x in S & y in S holds sup {x,y} in S;

  theorem :: WAYBEL23:19
     for L be non empty RelStr
   for S be Subset of L holds
    S is infs-closed iff
    for X be Subset of S st ex_inf_of X,L holds "/\"(X,L) in S;

  theorem :: WAYBEL23:20
     for L be non empty RelStr
   for S be Subset of L holds
    S is sups-closed iff
    for X be Subset of S st ex_sup_of X,L holds "\/"(X,L) in S;

  theorem :: WAYBEL23:21
   for L be non empty transitive RelStr
   for S be infs-closed non empty Subset of L
   for X be Subset of S st ex_inf_of X,L holds
    ex_inf_of X,subrelstr S & "/\"(X,subrelstr S) = "/\"(X,L);

  theorem :: WAYBEL23:22
   for L be non empty transitive RelStr
   for S be sups-closed non empty Subset of L
   for X be Subset of S st ex_sup_of X,L holds
    ex_sup_of X,subrelstr S & "\/"(X,subrelstr S) = "\/"(X,L);

  theorem :: WAYBEL23:23
     for L be non empty transitive RelStr
   for S be meet-closed non empty Subset of L
   for x,y be Element of S st ex_inf_of {x,y},L holds
    ex_inf_of {x,y},subrelstr S & "/\"({x,y},subrelstr S) = "/\"({x,y},L);

  theorem :: WAYBEL23:24
     for L be non empty transitive RelStr
   for S be join-closed non empty Subset of L
   for x,y be Element of S st ex_sup_of {x,y},L holds
    ex_sup_of {x,y},subrelstr S & "\/"({x,y},subrelstr S) = "\/"({x,y},L);

  theorem :: WAYBEL23:25
   for L be with_infima antisymmetric transitive RelStr
   for S be non empty meet-closed Subset of L holds
    subrelstr S is with_infima;

  theorem :: WAYBEL23:26
   for L be with_suprema antisymmetric transitive RelStr
   for S be non empty join-closed Subset of L holds
    subrelstr S is with_suprema;

  definition
   let L be with_infima antisymmetric transitive RelStr;
   let S be non empty meet-closed Subset of L;
   cluster subrelstr S -> with_infima;
  end;

  definition
   let L be with_suprema antisymmetric transitive RelStr;
   let S be non empty join-closed Subset of L;
   cluster subrelstr S -> with_suprema;
  end;

  theorem :: WAYBEL23:27
     for L be complete transitive antisymmetric (non empty RelStr)
   for S be infs-closed non empty Subset of L
   for X be Subset of S holds
    "/\"(X,subrelstr S) = "/\"(X,L);

  theorem :: WAYBEL23:28
     for L be complete transitive antisymmetric (non empty RelStr)
   for S be sups-closed non empty Subset of L
   for X be Subset of S holds
    "\/"(X,subrelstr S) = "\/"(X,L);

  theorem :: WAYBEL23:29
   for L be Semilattice
   for S be meet-closed Subset of L holds
    S is filtered;

  theorem :: WAYBEL23:30
   for L be sup-Semilattice
   for S be join-closed Subset of L holds
    S is directed;

  definition
   let L be Semilattice;
   cluster meet-closed -> filtered Subset of L;
  end;

  definition
   let L be sup-Semilattice;
   cluster join-closed -> directed Subset of L;
  end;

  theorem :: WAYBEL23:31
     for L be Semilattice
   for S be upper non empty Subset of L holds
    S is Filter of L iff S is meet-closed;

  theorem :: WAYBEL23:32
     for L be sup-Semilattice
   for S be lower non empty Subset of L holds
    S is Ideal of L iff S is join-closed;

  theorem :: WAYBEL23:33
   for L be non empty RelStr
   for S1,S2 be join-closed Subset of L holds
    S1 /\ S2 is join-closed;

  theorem :: WAYBEL23:34
     for L be non empty RelStr
   for S1,S2 be meet-closed Subset of L holds
    S1 /\ S2 is meet-closed;

  theorem :: WAYBEL23:35
   for L be sup-Semilattice
   for x be Element of L holds
    downarrow x is join-closed;

  theorem :: WAYBEL23:36
   for L be Semilattice
   for x be Element of L holds
    downarrow x is meet-closed;

  theorem :: WAYBEL23:37
   for L be sup-Semilattice
   for x be Element of L holds
    uparrow x is join-closed;

  theorem :: WAYBEL23:38
   for L be Semilattice
   for x be Element of L holds
    uparrow x is meet-closed;

  definition
   let L be sup-Semilattice;
   let x be Element of L;
   cluster downarrow x -> join-closed;
   cluster uparrow x -> join-closed;
  end;

  definition
   let L be Semilattice;
   let x be Element of L;
   cluster downarrow x -> meet-closed;
   cluster uparrow x -> meet-closed;
  end;

  theorem :: WAYBEL23:39
   for L be sup-Semilattice
   for x be Element of L holds
    waybelow x is join-closed;

  theorem :: WAYBEL23:40
   for L be Semilattice
   for x be Element of L holds
    waybelow x is meet-closed;

  theorem :: WAYBEL23:41
   for L be sup-Semilattice
   for x be Element of L holds
    wayabove x is join-closed;

  definition
   let L be sup-Semilattice;
   let x be Element of L;
   cluster waybelow x -> join-closed;
   cluster wayabove x -> join-closed;
  end;

  definition
   let L be Semilattice;
   let x be Element of L;
   cluster waybelow x -> meet-closed;
  end;

begin  :: About Bases of Continuous Lattices

  definition
   let T be TopStruct;
   func weight T -> Cardinal equals
:: WAYBEL23:def 5
      meet {Card B where B is Basis of T : not contradiction};
  end;

  definition
   let T be TopStruct;
   attr T is second-countable means
:: WAYBEL23:def 6
      weight T c= omega;
  end;

  definition  :: DEFINITION 4.1
   let L be continuous sup-Semilattice;
   mode CLbasis of L -> Subset of L means
:: WAYBEL23:def 7
    it is join-closed &
    for x be Element of L holds x = sup (waybelow x /\ it);
  end;

  definition
   let L be non empty RelStr;
   let S be Subset of L;
   attr S is with_bottom means
:: WAYBEL23:def 8
    Bottom L in S;
  end;

  definition
   let L be non empty RelStr;
   let S be Subset of L;
   attr S is with_top means
:: WAYBEL23:def 9
    Top L in S;
  end;

  definition
   let L be non empty RelStr;
   cluster with_bottom -> non empty Subset of L;
  end;

  definition
   let L be non empty RelStr;
   cluster with_top -> non empty Subset of L;
  end;

  definition
   let L be non empty RelStr;
   cluster with_bottom Subset of L;
   cluster with_top Subset of L;
  end;

  definition
   let L be continuous sup-Semilattice;
   cluster with_bottom CLbasis of L;
   cluster with_top CLbasis of L;
  end;

  theorem :: WAYBEL23:42
   for L be lower-bounded antisymmetric non empty RelStr
   for S be with_bottom Subset of L holds
    subrelstr S is lower-bounded;

  definition
   let L be lower-bounded antisymmetric non empty RelStr;
   let S be with_bottom Subset of L;
   cluster subrelstr S -> lower-bounded;
  end;

  definition
   let L be continuous sup-Semilattice;
   cluster -> join-closed CLbasis of L;
  end;

  definition
   cluster bounded non trivial (continuous LATTICE);
  end;

  definition
   let L be lower-bounded non trivial (continuous sup-Semilattice);
   cluster -> non empty CLbasis of L;
  end;

  theorem :: WAYBEL23:43
   for L be sup-Semilattice holds
    the carrier of CompactSublatt L is join-closed Subset of L;

  theorem :: WAYBEL23:44   :: Under 4.1 (i)
   for L be algebraic lower-bounded LATTICE holds
    the carrier of CompactSublatt L is with_bottom CLbasis of L;

  theorem :: WAYBEL23:45  :: Under 4.1 (ii)
     for L be continuous lower-bounded sup-Semilattice
    st the carrier of CompactSublatt L is CLbasis of L holds
     L is algebraic;

  theorem :: WAYBEL23:46  :: PROPOSITION 4.2. (1) iff (2)
   for L be continuous lower-bounded LATTICE
   for B be join-closed Subset of L holds
    B is CLbasis of L iff
    for x,y be Element of L st not y <= x
     ex b be Element of L st b in B & not b <= x & b << y;

  theorem :: WAYBEL23:47  :: PROPOSITION 4.2. (1) iff (3)
   for L be continuous lower-bounded LATTICE
   for B be join-closed Subset of L st Bottom L in B holds
    B is CLbasis of L iff
    for x,y be Element of L st x << y
     ex b be Element of L st b in B & x <= b & b << y;

  theorem :: WAYBEL23:48   :: PROPOSITION 4.2. (1) iff (4)
   for L be continuous lower-bounded LATTICE
   for B be join-closed Subset of L st Bottom L in B holds
    B is CLbasis of L iff
    (the carrier of CompactSublatt L c= B &
     for x,y be Element of L st not y <= x
      ex b be Element of L st b in B & not b <= x & b <= y);

  theorem :: WAYBEL23:49  :: PROPOSITION 4.2. (1) iff (5)
     for L be continuous lower-bounded LATTICE
   for B be join-closed Subset of L st Bottom L in B holds
    B is CLbasis of L iff
    for x,y be Element of L st not y <= x
     ex b be Element of L st b in B & not b <= x & b <= y;

  theorem :: WAYBEL23:50
   for L be lower-bounded sup-Semilattice
   for S be non empty full SubRelStr of L
    st Bottom
L in the carrier of S & the carrier of S is join-closed Subset of L
   for x be Element of L holds
    waybelow x /\ (the carrier of S) is Ideal of S;

  definition
   let L be non empty reflexive transitive RelStr;
   let S be non empty full SubRelStr of L;
   func supMap S -> map of InclPoset(Ids S), L means
:: WAYBEL23:def 10
    for I be Ideal of S holds it.I = "\/"(I,L);
  end;

  definition
   let L be non empty reflexive transitive RelStr;
   let S be non empty full SubRelStr of L;
   func idsMap S -> map of InclPoset(Ids S), InclPoset(Ids L) means
:: WAYBEL23:def 11
    for I be Ideal of S
    ex J be Subset of L st
     I = J & it.I = downarrow J;
  end;

  definition
   let L be reflexive RelStr;
   let B be Subset of L;
   cluster subrelstr B -> reflexive;
  end;

  definition
   let L be transitive RelStr;
   let B be Subset of L;
   cluster subrelstr B -> transitive;
  end;

  definition
   let L be antisymmetric RelStr;
   let B be Subset of L;
   cluster subrelstr B -> antisymmetric;
  end;

  definition
   let L be lower-bounded continuous sup-Semilattice;
   let B be with_bottom CLbasis of L;
   func baseMap B -> map of L, InclPoset(Ids subrelstr B) means
:: WAYBEL23:def 12
    for x be Element of L holds it.x = waybelow x /\ B;
  end;

  theorem :: WAYBEL23:51
   for L be non empty reflexive transitive RelStr
   for S be non empty full SubRelStr of L holds
    dom supMap S = Ids S & rng supMap S is Subset of L;

  theorem :: WAYBEL23:52
   for L be non empty reflexive transitive RelStr
   for S be non empty full SubRelStr of L
   for x be set holds
    x in dom supMap S iff x is Ideal of S;

  theorem :: WAYBEL23:53
   for L be non empty reflexive transitive RelStr
   for S be non empty full SubRelStr of L holds
    dom idsMap S = Ids S & rng idsMap S is Subset of Ids L;

  theorem :: WAYBEL23:54
   for L be non empty reflexive transitive RelStr
   for S be non empty full SubRelStr of L
   for x be set holds
    x in dom idsMap S iff x is Ideal of S;

  theorem :: WAYBEL23:55
   for L be non empty reflexive transitive RelStr
   for S be non empty full SubRelStr of L
   for x be set holds
    x in rng idsMap S implies x is Ideal of L;

  theorem :: WAYBEL23:56
   for L be lower-bounded continuous sup-Semilattice
   for B be with_bottom CLbasis of L holds
    dom baseMap B = the carrier of L &
    rng baseMap B is Subset of Ids subrelstr B;

  theorem :: WAYBEL23:57
     for L be lower-bounded continuous sup-Semilattice
   for B be with_bottom CLbasis of L
   for x be set holds
    x in rng baseMap B implies x is Ideal of subrelstr B;

  theorem :: WAYBEL23:58
   for L be up-complete (non empty Poset)
   for S be non empty full SubRelStr of L holds
    supMap S is monotone;

  theorem :: WAYBEL23:59
   for L be non empty reflexive transitive RelStr
   for S be non empty full SubRelStr of L holds
    idsMap S is monotone;

  theorem :: WAYBEL23:60
   for L be lower-bounded continuous sup-Semilattice
   for B be with_bottom CLbasis of L holds
    baseMap B is monotone;

  definition
   let L be up-complete (non empty Poset);
   let S be non empty full SubRelStr of L;
   cluster supMap S -> monotone;
  end;

  definition
   let L be non empty reflexive transitive RelStr;
   let S be non empty full SubRelStr of L;
   cluster idsMap S -> monotone;
  end;

  definition
   let L be lower-bounded continuous sup-Semilattice;
   let B be with_bottom CLbasis of L;
   cluster baseMap B -> monotone;
  end;

  theorem :: WAYBEL23:61
   for L be lower-bounded (continuous sup-Semilattice)
   for B be with_bottom CLbasis of L holds
    idsMap (subrelstr B) is sups-preserving;

  theorem :: WAYBEL23:62
   for L be up-complete (non empty Poset)
   for S be non empty full SubRelStr of L holds
    supMap S = (SupMap L)*(idsMap S);

  theorem :: WAYBEL23:63   :: PROPOSITION 4.3.(i)
   for L be lower-bounded continuous sup-Semilattice
   for B be with_bottom CLbasis of L holds
    [supMap subrelstr B,baseMap B] is Galois;

  theorem :: WAYBEL23:64   :: PROPOSITION 4.3.(ii)
   for L be lower-bounded continuous sup-Semilattice
   for B be with_bottom CLbasis of L holds
    supMap subrelstr B is upper_adjoint & baseMap B is lower_adjoint;

  theorem :: WAYBEL23:65   :: PROPOSITION 4.3.(iii)
   for L be lower-bounded (continuous sup-Semilattice)
   for B be with_bottom CLbasis of L holds
    rng supMap subrelstr B = the carrier of L;

  theorem :: WAYBEL23:66   :: PROPOSITION 4.3.(iv)
   for L be lower-bounded (continuous sup-Semilattice)
   for B be with_bottom CLbasis of L holds
    supMap (subrelstr B) is infs-preserving sups-preserving;

  theorem :: WAYBEL23:67
   for L be lower-bounded continuous sup-Semilattice
   for B be with_bottom CLbasis of L holds
    baseMap B is sups-preserving;

   definition
    let L be lower-bounded continuous sup-Semilattice;
    let B be with_bottom CLbasis of L;
    cluster supMap subrelstr B -> infs-preserving sups-preserving;
    cluster baseMap B -> sups-preserving;
   end;

canceled;

  theorem :: WAYBEL23:69   :: PROPOSITION 4.3.(vi)
   for L be lower-bounded (continuous sup-Semilattice)
   for B be with_bottom CLbasis of L holds
    the carrier of CompactSublatt InclPoset(Ids subrelstr B) =
     { downarrow b where b is Element of subrelstr B : not contradiction };

  theorem :: WAYBEL23:70  :: PROPOSITION 4.3.(vii)
     for L be lower-bounded (continuous sup-Semilattice)
   for B be with_bottom CLbasis of L holds
    CompactSublatt InclPoset(Ids subrelstr B),subrelstr B are_isomorphic;

  theorem :: WAYBEL23:71
   for L be continuous lower-bounded LATTICE
   for B be with_bottom CLbasis of L st
    for B1 be with_bottom CLbasis of L holds B c= B1
   for J be Element of InclPoset Ids subrelstr B holds
    J = waybelow "\/"(J,L) /\ B;

  theorem :: WAYBEL23:72  :: PROPOSITION 4.4. (1) iff (2)
     for L be continuous lower-bounded LATTICE holds
    L is algebraic iff
     the carrier of CompactSublatt L is with_bottom CLbasis of L &
     for B be with_bottom CLbasis of L holds
      the carrier of CompactSublatt L c= B;

  theorem :: WAYBEL23:73  :: PROPOSITION 4.4. (1) iff (3)
     for L be continuous lower-bounded LATTICE holds
    L is algebraic iff
     ex B be with_bottom CLbasis of L st
     for B1 be with_bottom CLbasis of L holds B c= B1;


Back to top