The Mizar abstract of WAYBEL30

Journal of Formalized Mathematics
Volume 12, 2000
University of Bialystok
Copyright (c) 2000 Association of Mizar Users
The abstract of the Mizar article:: Meet Continuous Lattices Revisited
by
Artur Kornilowicz
Received January 6, 2000
MML identifier: WAYBEL30
[ Mizar article, MML identifier index ]
environ

 vocabulary BOOLE, TARSKI, RELAT_2, ORDERS_1, QUANTAL1, YELLOW_1, WAYBEL_0,
      FILTER_2, LATTICE3, ORDINAL2, YELLOW_0, LATTICES, WAYBEL_2, REALSET1,
      YELLOW_9, WAYBEL11, BHSP_3, WAYBEL_9, PRE_TOPC, PROB_1, WAYBEL19,
      PRELAMB, CANTOR_1, SETFAM_1, DIRAF, SUBSET_1, FINSET_1, COMPTS_1,
      YELLOW_6, TOPS_1, WAYBEL29, YELLOW13, WAYBEL21, RELAT_1, PARTFUN1,
      FUNCT_3, FUNCT_1, TOPS_2, WAYBEL_3, RLVECT_3, TDLAT_3, CONNSP_2,
      FILTER_0, WAYBEL_8, WAYBEL_6, WAYBEL30;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, FUNCT_1,
      FUNCT_2, FUNCT_3, STRUCT_0, FINSET_1, REALSET1, ORDERS_1, PRE_TOPC,
      TOPS_1, TOPS_2, COMPTS_1, CONNSP_2, TDLAT_3, LATTICE3, BORSUK_1,
      CANTOR_1, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_1, YELLOW_3, YELLOW_4,
      WAYBEL_2, WAYBEL_3, YELLOW_6, YELLOW_8, WAYBEL_6, WAYBEL_8, WAYBEL_9,
      WAYBEL11, YELLOW_9, WAYBEL19, WAYBEL21, YELLOW13, WAYBEL29;
 constructors CANTOR_1, GROUP_1, TOPS_1, TOPS_2, TDLAT_3, YELLOW_4, YELLOW_8,
      WAYBEL_1, WAYBEL_6, WAYBEL_8, WAYBEL19, ORDERS_3, URYSOHN1, WAYBEL21,
      YELLOW13, WAYBEL29, MEMBERED;
 clusters STRUCT_0, FINSET_1, BORSUK_1, SUBSET_1, TEX_1, TOPS_1, CANTOR_1,
      LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_3, YELLOW_4, YELLOW_6,
      WAYBEL_0, WAYBEL_2, WAYBEL_3, WAYBEL_8, WAYBEL10, WAYBEL11, WAYBEL14,
      YELLOW_9, WAYBEL19, YELLOW12, WAYBEL_4, RELSET_1, YELLOW13, MEMBERED,
      ZFMISC_1;
 requirements BOOLE, SUBSET;


begin

theorem :: WAYBEL30:1
 for x being set, D being non empty set holds
  x /\ union D = union {x /\ d where d is Element of D: not contradiction};

theorem :: WAYBEL30:2
 for R being non empty reflexive transitive RelStr,
     D being non empty directed Subset of InclPoset Ids R holds
   union D is Ideal of R;

:: Exercise 2.16 (i), p. 16
definition let R be non empty reflexive transitive RelStr;
 cluster InclPoset Ids R -> up-complete;
end;

theorem :: WAYBEL30:3
 for R being non empty reflexive transitive RelStr,
     D being non empty directed Subset of InclPoset Ids R holds
  sup D = union D;

theorem :: WAYBEL30:4
 for R being Semilattice,
     D being non empty directed Subset of InclPoset Ids R,
     x being Element of InclPoset Ids R holds
   sup ({x} "/\" D) = union {x /\ d where d is Element of D: not contradiction}
;

:: Exercise 4.8 (i), p. 33
definition let R be Semilattice;
 cluster InclPoset Ids R -> satisfying_MC;
end;

definition let R be non empty trivial RelStr;
 cluster -> trivial TopAugmentation of R;
end;

theorem :: WAYBEL30:5
   for S being Scott complete TopLattice, T being complete LATTICE,
     A being Scott TopAugmentation of T
   st the RelStr of S = the RelStr of T holds
  the TopRelStr of A = the TopRelStr of S;

theorem :: WAYBEL30:6
   for N being Lawson complete TopLattice, T being complete LATTICE,
     A being Lawson correct TopAugmentation of T
   st the RelStr of N = the RelStr of T holds
  the TopRelStr of A = the TopRelStr of N;

theorem :: WAYBEL30:7
   for N being Lawson complete TopLattice
  for S being Scott TopAugmentation of N
   for A being Subset of N, J being Subset of S st A = J & J is closed holds
  A is closed;

definition let A be complete LATTICE;
 cluster lambda A -> non empty;
end;

definition let S be Scott complete TopLattice;
 cluster InclPoset sigma S -> complete non trivial;
end;

definition let N be Lawson complete TopLattice;
 cluster InclPoset sigma N -> complete non trivial;
 cluster InclPoset lambda N -> complete non trivial;
end;

theorem :: WAYBEL30:8
 for T being non empty reflexive RelStr holds
 sigma T c= {W\uparrow F where W, F is Subset of T: W in sigma T & F is finite}
;

theorem :: WAYBEL30:9
 for N being Lawson complete TopLattice holds lambda N = the topology of N;

theorem :: WAYBEL30:10
 for N being Lawson complete TopLattice holds sigma N c= lambda N;

theorem :: WAYBEL30:11
   for M, N being complete LATTICE st the RelStr of M = the RelStr of N holds
  lambda M = lambda N;

theorem :: WAYBEL30:12
 for N being Lawson complete TopLattice, X being Subset of N holds
  X in lambda N iff X is open;

definition
 cluster trivial TopSpace-like -> Scott (reflexive non empty TopRelStr);
end;

definition
 cluster trivial -> Lawson (complete TopLattice);
end;

definition
 cluster strict continuous lower-bounded meet-continuous Scott
  (complete TopLattice);
end;

definition
 cluster strict continuous compact Hausdorff Lawson (complete TopLattice);
end;

theorem :: WAYBEL30:13
 for N being meet-continuous LATTICE, A being Subset of N st
  A has_the_property_(S) holds uparrow A has_the_property_(S);

definition let N be meet-continuous LATTICE,
               A be property(S) Subset of N;
 cluster uparrow A -> property(S);
end;

:: Proposition 2.1 (i), p. 153
theorem :: WAYBEL30:14
 for N being meet-continuous Lawson (complete TopLattice),
     S being Scott TopAugmentation of N,
     A being Subset of N st A in lambda N holds
  uparrow A in sigma S;

theorem :: WAYBEL30:15
 for N being meet-continuous Lawson (complete TopLattice)
  for S being Scott TopAugmentation of N
   for A being Subset of N, J being Subset of S st A = J holds
  A is open implies uparrow J is open;

theorem :: WAYBEL30:16
 for N being meet-continuous Lawson (complete TopLattice)
  for S being Scott TopAugmentation of N
   for x being Point of S, y being Point of N
    for J being Basis of y st x = y holds
  {uparrow A where A is Subset of N: A in J} is Basis of x;

:: Proposition 2.1 (ii), p. 153
theorem :: WAYBEL30:17
 for N being meet-continuous Lawson (complete TopLattice)
  for S being Scott TopAugmentation of N
   for X being upper Subset of N, Y being Subset of S st X = Y
  holds Int X = Int Y;

:: Proposition 2.1 (iii), p. 153
theorem :: WAYBEL30:18
   for N being meet-continuous Lawson (complete TopLattice)
  for S being Scott TopAugmentation of N
   for X being lower Subset of N, Y being Subset of S st X = Y
  holds Cl X = Cl Y;

theorem :: WAYBEL30:19
 for M, N being complete LATTICE,
     LM being Lawson correct TopAugmentation of M,
     LN being Lawson correct TopAugmentation of N st
   InclPoset sigma N is continuous holds
  the topology of [:LM,LN qua TopSpace:] = lambda [:M,N:];

:: Proposition 2.2, p. 153
theorem :: WAYBEL30:20
 for M, N being complete LATTICE,
     P being Lawson correct TopAugmentation of [:M,N:],
     Q being Lawson correct TopAugmentation of M,
     R being Lawson correct TopAugmentation of N st
   InclPoset sigma N is continuous holds
  the TopStruct of P = [:Q,R qua TopSpace:];

:: Theorem 2.3, p. 153, first conjunct
theorem :: WAYBEL30:21
 for N being meet-continuous Lawson (complete TopLattice),
     x being Element of N
  holds x"/\" is continuous;

definition let N be meet-continuous Lawson (complete TopLattice),
               x be Element of N;
 cluster x"/\" -> continuous;
end;

:: Theorem 2.3, p. 153, second conjunct
theorem :: WAYBEL30:22
 for N being meet-continuous Lawson (complete TopLattice)
  st InclPoset sigma N is continuous holds N is topological_semilattice;

:: Proposition 2.4, p. 153
theorem :: WAYBEL30:23
   for N being meet-continuous Lawson (complete TopLattice)
  st InclPoset sigma N is continuous holds
 N is Hausdorff iff
  for X being Subset of [:N,N qua TopSpace:] st
   X = the InternalRel of N holds X is closed;

:: Definition 2.5, p. 154
definition let N be non empty reflexive RelStr,
               X be Subset of N;
 func X^0 -> Subset of N equals
:: WAYBEL30:def 1
  { u where u is Element of N : for D being non empty directed Subset of N
      st u <= sup D holds X meets D };
end;

definition let N be non empty reflexive antisymmetric RelStr,
               X be empty Subset of N;
 cluster X^0 -> empty;
end;

theorem :: WAYBEL30:24
   for N being non empty reflexive RelStr, A, J being Subset of N st A c= J
  holds A^0 c= J^0;

:: Remark 2.6 (i), p. 154
theorem :: WAYBEL30:25
 for N being non empty reflexive RelStr, x being Element of N holds
  (uparrow x)^0 = wayabove x;

:: Remark 2.6 (ii), p. 154
theorem :: WAYBEL30:26
 for N being Scott TopLattice, X being upper Subset of N holds Int X c= X^0;

:: Lemma 2.7 (i), p. 154
theorem :: WAYBEL30:27
 for N being non empty reflexive RelStr, X, Y being Subset of N holds
  (X^0) \/ (Y^0) c= (X \/ Y)^0;

:: Lemma 2.7 (ii), p. 154
theorem :: WAYBEL30:28
 for N being meet-continuous LATTICE, X, Y being upper Subset of N holds
  (X^0) \/ (Y^0) = (X \/ Y)^0;

:: Lemma 2.8, p. 154
theorem :: WAYBEL30:29
 for S being meet-continuous Scott TopLattice, F being finite Subset of S holds
  Int uparrow F c= union { wayabove x where x is Element of S : x in F };

:: Theorem 2.9, p. 154
theorem :: WAYBEL30:30
 for N being Lawson (complete TopLattice)
  holds N is continuous iff N is meet-continuous Hausdorff;

definition
 cluster continuous Lawson -> Hausdorff (complete TopLattice);
 cluster meet-continuous Lawson Hausdorff -> continuous (complete TopLattice);
end;

:: Definition 2.10, p. 155
definition let N be non empty TopRelStr;
 attr N is with_small_semilattices means
:: WAYBEL30:def 2
    for x being Point of N ex J being basis of x st
   for A being Subset of N st A in J holds subrelstr A is meet-inheriting;
 attr N is with_compact_semilattices means
:: WAYBEL30:def 3
    for x being Point of N ex J being basis of x st
   for A being Subset of N st A in J holds subrelstr A is meet-inheriting &
    A is compact;
 attr N is with_open_semilattices means
:: WAYBEL30:def 4
  for x being Point of N ex J being Basis of x st
   for A being Subset of N st A in J holds subrelstr A is meet-inheriting;
end;

definition
 cluster with_open_semilattices -> with_small_semilattices
                                   (non empty TopSpace-like TopRelStr);

 cluster with_compact_semilattices -> with_small_semilattices
                                      (non empty TopSpace-like TopRelStr);

 cluster anti-discrete -> with_small_semilattices with_open_semilattices
                                                   (non empty TopRelStr);

 cluster reflexive trivial TopSpace-like ->
                             with_compact_semilattices (non empty TopRelStr);
end;

definition
 cluster strict trivial lower TopLattice;
end;

theorem :: WAYBEL30:31
 for N being topological_semilattice (with_infima TopPoset),
     C being Subset of N st subrelstr C is meet-inheriting holds
  subrelstr Cl C is meet-inheriting;

:: Theorem 2.11, p. 155
theorem :: WAYBEL30:32
 for N being meet-continuous Lawson (complete TopLattice)
  for S being Scott TopAugmentation of N holds
  (for x being Point of S ex J being Basis of x st
   for W being Subset of S st W in J holds W is Filter of S) iff
  N is with_open_semilattices;

:: Theorem 2.12, p. 155,  r => l
theorem :: WAYBEL30:33
 for N being Lawson (complete TopLattice)
  for S being Scott TopAugmentation of N
   for x being Element of N holds
  {inf A where A is Subset of S : x in A & A in sigma S} c=
   {inf J where J is Subset of N : x in J & J in lambda N};

:: Theorem 2.12, p. 155
theorem :: WAYBEL30:34
 for N being meet-continuous Lawson (complete TopLattice)
  for S being Scott TopAugmentation of N
   for x being Element of N holds
  {inf A where A is Subset of S : x in A & A in sigma S} =
  {inf J where J is Subset of N : x in J & J in lambda N};

:: Theorem 2.13, p. 155,  1 <=> 2
theorem :: WAYBEL30:35
 for N being meet-continuous Lawson (complete TopLattice) holds
  N is continuous iff
   N is with_open_semilattices & InclPoset sigma N is continuous;

definition
 cluster continuous -> with_open_semilattices (Lawson complete TopLattice);
end;

definition let N be continuous Lawson (complete TopLattice);
 cluster InclPoset sigma N -> continuous;
end;

:: Theorem 2.13, p. 155,  1 => 3
theorem :: WAYBEL30:36
   for N being continuous Lawson (complete TopLattice) holds
  N is compact Hausdorff topological_semilattice with_open_semilattices;

:: Theorem 2.13, p. 155,  3 => 3'
theorem :: WAYBEL30:37
   for N being Hausdorff topological_semilattice with_open_semilattices
  Lawson (complete TopLattice) holds
   N is with_compact_semilattices;

:: Theorem 2.13, p. 155,  3' => 4
theorem :: WAYBEL30:38
   for N being meet-continuous Hausdorff Lawson (complete TopLattice),
     x being Element of N holds
   x = "\/"({inf V where V is Subset of N: x in V & V in lambda N},N);

:: Theorem 2.13, p. 155,  1 <=> 4
theorem :: WAYBEL30:39
   for N being meet-continuous Lawson (complete TopLattice) holds
  N is continuous iff
   for x being Element of N holds
    x = "\/"({inf V where V is Subset of N: x in V & V in lambda N},N);

:: Exercise 2.16, p. 156,  1 <=> 2
theorem :: WAYBEL30:40
 for N being meet-continuous Lawson (complete TopLattice) holds
  N is algebraic iff
  N is with_open_semilattices & InclPoset sigma N is algebraic;

definition let N be meet-continuous algebraic Lawson (complete TopLattice);
 cluster InclPoset sigma N -> algebraic;
end;
The abstract of the Mizar article:

Meet Continuous Lattices Revisited
