The abstract of the Mizar article:

Weights of Continuous Lattices

by

Robert Milewski

Received January 6, 2000

MML identifier: WAYBEL31

[ Mizar article, MML identifier index ]

environ

 vocabulary ORDERS_1, SETFAM_1, WAYBEL_0, TARSKI, LATTICES, ORDINAL2, WAYBEL23,
      YELLOW_1, YELLOW_0, WAYBEL_8, CARD_1, ORDINAL1, SUBSET_1, PRE_TOPC,
      CANTOR_1, WAYBEL_3, BOOLE, FINSET_1, TSP_1, FUNCT_1, RELAT_1, WAYBEL11,
      YELLOW_9, WAYBEL19, PRELAMB, DIRAF, PROB_1, COMPTS_1, QUANTAL1, LATTICE3,
      REALSET1, RELAT_2, FILTER_2, FINSEQ_1, MATRIX_2, BHSP_3, FINSEQ_4,
      WAYBEL_9, WELLORD1, CAT_1, WAYBEL31, RLVECT_3;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, STRUCT_0, FINSET_1,
      RELSET_1, GROUP_1, RELAT_1, REALSET1, FUNCT_1, FUNCT_2, FINSEQ_1,
      FINSEQ_2, FINSEQ_4, MATRIX_2, ORDINAL1, CARD_1, PRE_TOPC, TSP_1, TOPS_2,
      CANTOR_1, ORDERS_1, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_9,
      WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_8, WAYBEL_9, WAYBEL11, WAYBEL19,
      WAYBEL23;
 constructors NAT_1, GROUP_1, FINSEQ_4, MATRIX_2, TSP_1, TOPS_2, CANTOR_1,
      URYSOHN1, ORDERS_3, YELLOW_9, WAYBEL_1, WAYBEL_8, WAYBEL11, WAYBEL19,
      WAYBEL23, MEMBERED;
 clusters STRUCT_0, RELSET_1, FINSET_1, FINSEQ_1, CARD_1, TSP_1, SUBSET_1,
      CANTOR_1, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_3, YELLOW_9,
      YELLOW11, YELLOW13, YELLOW15, WAYBEL_0, WAYBEL_3, WAYBEL_4, WAYBEL_8,
      WAYBEL14, WAYBEL19, WAYBEL23, WAYBEL25, WAYBEL30, ZFMISC_1;
 requirements NUMERALS, BOOLE, SUBSET;


begin

  scheme UparrowUnion{L1()->RelStr,P[set]}:
   for S be Subset-Family of L1() st
    S = { X where X is Subset of L1() : P[X] } holds
     uparrow union S = union { uparrow X where X is Subset of L1() : P[X] };

  scheme DownarrowUnion{L1()->RelStr,P[set]}:
   for S be Subset-Family of L1() st
    S = { X where X is Subset of L1() : P[X] } holds
     downarrow union S = union { downarrow X where X is Subset of L1() : P[X]};

  definition
   let L1 be lower-bounded continuous sup-Semilattice;
   let B1 be with_bottom CLbasis of L1;
   cluster InclPoset Ids subrelstr B1 -> algebraic;
  end;

  definition  :: DEFINITION 4.5
   let L1 be continuous sup-Semilattice;
   func CLweight L1 -> Cardinal equals
:: WAYBEL31:def 1
    meet {Card B1 where B1 is with_bottom CLbasis of L1 : not contradiction};
  end;

  theorem :: WAYBEL31:1
   for T be TopStruct
   for b be Basis of T holds
    weight T c= Card b;

  theorem :: WAYBEL31:2
   for T be TopStruct
   ex b be Basis of T st
    Card b = weight T;

  theorem :: WAYBEL31:3
   for L1 be continuous sup-Semilattice
   for B1 be with_bottom CLbasis of L1 holds
    CLweight L1 c= Card B1;

  theorem :: WAYBEL31:4
   for L1 be continuous sup-Semilattice
   ex B1 be with_bottom CLbasis of L1 st
    Card B1 = CLweight L1;

  theorem :: WAYBEL31:5   :: Under 4.5.
   for L1 be algebraic lower-bounded LATTICE holds
    CLweight L1 = Card the carrier of CompactSublatt L1;

  theorem :: WAYBEL31:6
   for T be non empty TopSpace
   for L1 be continuous sup-Semilattice st
    InclPoset the topology of T = L1
   for B1 be with_bottom CLbasis of L1 holds
    B1 is Basis of T;

  theorem :: WAYBEL31:7
   for T be non empty TopSpace
   for L1 be continuous lower-bounded LATTICE st
    InclPoset the topology of T = L1
   for B1 be Basis of T
   for B2 be Subset of L1 st B1 = B2 holds
    finsups B2 is with_bottom CLbasis of L1;

  theorem :: WAYBEL31:8   :: PROPOSITION 4.6 (i)
   for T be T_0 non empty TopSpace
   for L1 be continuous lower-bounded sup-Semilattice st
    InclPoset the topology of T = L1 holds
     T is infinite implies weight T = CLweight L1;

  theorem :: WAYBEL31:9   :: PROPOSITION 4.6 (ii) (a)
   for T be T_0 non empty TopSpace
   for L1 be continuous sup-Semilattice st
    InclPoset the topology of T = L1 holds
     Card the carrier of T c= Card the carrier of L1;

  theorem :: WAYBEL31:10  :: PROPOSITION 4.6 (ii) (b)
   for T be T_0 non empty TopSpace st T is finite holds
    weight T = Card the carrier of T;

  theorem :: WAYBEL31:11   :: PROPOSITION 4.6 (ii) (c)
   for T be TopStruct
   for L1 be continuous lower-bounded LATTICE st
    InclPoset the topology of T = L1 & T is finite holds
     CLweight L1 = Card the carrier of L1;

  theorem :: WAYBEL31:12
   for L1 be continuous lower-bounded sup-Semilattice
   for T1 be Scott TopAugmentation of L1
   for T2 be Lawson correct TopAugmentation of L1
   for B2 be Basis of T2 holds
    { uparrow V where V is Subset of T2 : V in B2 } is Basis of T1;

canceled;

  theorem :: WAYBEL31:14
   for L1 be up-complete (non empty Poset) st L1 is finite
   for x be Element of L1 holds
    x in compactbelow x;

  theorem :: WAYBEL31:15
   for L1 be finite LATTICE holds
    L1 is arithmetic;

  definition
   cluster finite -> arithmetic LATTICE;
  end;

  definition
   cluster trivial reflexive transitive antisymmetric with_suprema with_infima
    lower-bounded non empty finite strict RelStr;
  end;

  theorem :: WAYBEL31:16
   for L1 be finite LATTICE
   for B1 be with_bottom CLbasis of L1 holds
    Card B1 = CLweight L1 iff B1 = the carrier of CompactSublatt L1;

  definition
   let L1 be non empty reflexive RelStr;
   let A be Subset of L1;
   let a be Element of L1;
   func Way_Up(a,A) -> Subset of L1 equals
:: WAYBEL31:def 2
    wayabove a \ uparrow A;
  end;

  theorem :: WAYBEL31:17
     for L1 be non empty reflexive RelStr
   for a be Element of L1 holds
    Way_Up(a,{}(L1)) = wayabove a;

  theorem :: WAYBEL31:18
     for L1 be non empty Poset
   for A be Subset of L1
   for a be Element of L1 st a in uparrow A holds
    Way_Up(a,A) = {};

  theorem :: WAYBEL31:19
   for L1 be non empty finite reflexive transitive RelStr holds
    Ids L1 is finite;

  theorem :: WAYBEL31:20
   for L1 be continuous lower-bounded sup-Semilattice st L1 is infinite
   for B1 be with_bottom CLbasis of L1 holds
    B1 is infinite;

canceled 2;

  theorem :: WAYBEL31:23
     for L1 be complete (non empty Poset)
   for x be Element of L1 holds
    x is compact implies x = inf wayabove x;

  theorem :: WAYBEL31:24
   for L1 be continuous lower-bounded sup-Semilattice st L1 is infinite
   for B1 be with_bottom CLbasis of L1 holds
    Card { Way_Up(a,A) where a is Element of L1, A is finite Subset of L1 :
           a in B1 & A c= B1 } c= Card B1;

  theorem :: WAYBEL31:25
   for T be Lawson (complete TopLattice)
   for X be finite Subset of T holds
    (uparrow X)` is open & (downarrow X)` is open;

  theorem :: WAYBEL31:26
   for L1 be continuous lower-bounded sup-Semilattice
   for T be Lawson correct TopAugmentation of L1 holds
   for B1 be with_bottom CLbasis of L1 holds
    { Way_Up(a,A) where a is Element of L1, A is finite Subset of L1 :
           a in B1 & A c= B1 } is Basis of T;

  theorem :: WAYBEL31:27
   for L1 be continuous lower-bounded sup-Semilattice
   for T be Scott TopAugmentation of L1
   for b be Basis of T holds
    { wayabove inf u where u is Subset of T : u in b } is Basis of T;

  theorem :: WAYBEL31:28
   for L1 be continuous lower-bounded sup-Semilattice
   for T be Scott TopAugmentation of L1
   for B1 be Basis of T st B1 is infinite holds
    { inf u where u is Subset of T : u in B1 } is infinite;

  theorem :: WAYBEL31:29   :: THEOREM 4.7 (1)=(2)
   for L1 be continuous lower-bounded sup-Semilattice
   for T be Scott TopAugmentation of L1 holds
    CLweight L1 = weight T;

  theorem :: WAYBEL31:30  :: THEOREM 4.7 (1)=(3)
     for L1 be continuous lower-bounded sup-Semilattice
   for T be Lawson correct TopAugmentation of L1 holds
    CLweight L1 = weight T;

  theorem :: WAYBEL31:31
   for L1,L2 be non empty RelStr st L1,L2 are_isomorphic holds
    Card the carrier of L1 = Card the carrier of L2;

  theorem :: WAYBEL31:32  :: THEOREM 4.7 (1)=(4)
     for L1 be continuous lower-bounded sup-Semilattice
   for B1 be with_bottom CLbasis of L1 st Card B1 = CLweight L1 holds
    CLweight L1 = CLweight InclPoset Ids subrelstr B1;

  definition
   let L1 be continuous lower-bounded sup-Semilattice;
   cluster InclPoset sigma L1 -> with_suprema continuous;
  end;

  theorem :: WAYBEL31:33  :: THEOREM 4.7 (5)
     for L1 be continuous lower-bounded sup-Semilattice holds
    CLweight L1 c= CLweight InclPoset sigma L1;

  theorem :: WAYBEL31:34  :: THEOREM 4.7 (6)
     for L1 be continuous lower-bounded sup-Semilattice st L1 is infinite holds
    CLweight L1 = CLweight InclPoset sigma L1;