The abstract of the Mizar article:

Introduction to Meet-Continuous Topological Lattices

by

Artur Kornilowicz

Received November 3, 1998

MML identifier: YELLOW13

[ Mizar article, MML identifier index ]

environ

 vocabulary FINSET_1, REALSET1, ORDERS_1, WAYBEL_9, URYSOHN1, PRE_TOPC, BOOLE,
      COMPTS_1, SUBSET_1, NATTRA_1, TSP_1, RELAT_2, WAYBEL_0, RELAT_1, SEQM_3,
      FUNCT_1, YELLOW_2, YELLOW_1, FILTER_2, ORDINAL2, YELLOW_0, WELLORD1,
      WAYBEL_1, SGRAPH1, BHSP_3, LATTICES, LATTICE3, TDLAT_3, CANTOR_1,
      SETFAM_1, RLVECT_3, TOPS_1, CONNSP_2, PRELAMB, TARSKI, WAYBEL_2,
      YELLOW13;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
      FINSET_1, STRUCT_0, ORDERS_1, PRE_TOPC, TOPS_1, GROUP_1, COMPTS_1,
      TDLAT_2, TDLAT_3, TSP_1, LATTICE3, CANTOR_1, REALSET1, BORSUK_1,
      URYSOHN1, YELLOW_0, WAYBEL_0, YELLOW_1, ORDERS_3, WAYBEL_1, YELLOW_2,
      YELLOW_3, WAYBEL_2, YELLOW_8, WAYBEL_9;
 constructors CANTOR_1, TOPS_1, TDLAT_2, TDLAT_3, TSP_1, URYSOHN1, YELLOW_8,
      WAYBEL_1, WAYBEL_3, YELLOW_9, ORDERS_3, GROUP_1, LATTICE3, XCMPLX_0,
      MEMBERED;
 clusters STRUCT_0, TOPS_1, FINSET_1, REALSET1, TDLAT_3, TEX_1, YELLOW_0,
      YELLOW_1, YELLOW_2, WAYBEL_0, WAYBEL_1, WAYBEL_3, YELLOW_8, YELLOW_9,
      WAYBEL11, WAYBEL12, YELLOW11, YELLOW12, BORSUK_1, RELSET_1, SUBSET_1,
      RLVECT_2, XREAL_0, MEMBERED, ZFMISC_1;
 requirements SUBSET, BOOLE;


begin  :: Preliminaries

definition let S be finite 1-sorted;
 cluster the carrier of S -> finite;
end;

definition let S be trivial 1-sorted;
 cluster the carrier of S -> trivial;
end;

definition
 cluster trivial -> finite set;
end;

definition
 cluster trivial -> finite 1-sorted;
end;

definition
 cluster non trivial -> non empty 1-sorted;
end;

definition
 cluster strict non empty trivial 1-sorted;

 cluster strict non empty trivial RelStr;

 cluster strict non empty trivial TopRelStr;
end;

theorem :: YELLOW13:1
 for T being being_T1 (non empty TopSpace),
     A being finite Subset of T holds A is closed;

definition let T be being_T1 (non empty TopSpace);
 cluster finite -> closed Subset of T;
end;

definition let T be compact TopStruct;
 cluster [#]T -> compact;
end;

definition
 cluster strict non empty trivial TopSpace;
end;

definition
 cluster finite being_T1 -> discrete (non empty TopSpace);
end;

definition
 cluster finite -> compact TopSpace;
end;

theorem :: YELLOW13:2
 for T being discrete non empty TopSpace holds T is_T4;

theorem :: YELLOW13:3
 for T being discrete non empty TopSpace holds T is_T3;

theorem :: YELLOW13:4
 for T being discrete non empty TopSpace holds T is_T2;

theorem :: YELLOW13:5
 for T being discrete non empty TopSpace holds T is_T1;

definition
 cluster discrete non empty -> being_T4 being_T3 being_T2 being_T1 TopSpace;
end;

definition
 cluster being_T4 being_T1 -> being_T3 (non empty TopSpace);
end;

definition
 cluster being_T3 being_T1 -> being_T2 (non empty TopSpace);
end;

definition
 cluster being_T2 -> being_T1 TopSpace;
end;

definition
 cluster being_T1 -> T_0 TopSpace;
end;

theorem :: YELLOW13:6
 for S being reflexive RelStr, T being reflexive transitive RelStr,
     f being map of S, T, X being Subset of S
  holds downarrow (f.:X) c= downarrow (f.:downarrow X);

theorem :: YELLOW13:7
   for S being reflexive RelStr, T being reflexive transitive RelStr,
     f being map of S, T, X being Subset of S st f is monotone
 holds downarrow (f.:X) = downarrow (f.:downarrow X);

theorem :: YELLOW13:8
 for N being non empty Poset holds IdsMap N is one-to-one;

definition let N be non empty Poset;
 cluster IdsMap N -> one-to-one;
end;

theorem :: YELLOW13:9
 for N being finite LATTICE holds SupMap N is one-to-one;

definition let N be finite LATTICE;
 cluster SupMap N -> one-to-one;
end;

theorem :: YELLOW13:10
   for N being finite LATTICE holds N, InclPoset Ids N are_isomorphic;

theorem :: YELLOW13:11
 for N being complete (non empty Poset), x being Element of N,
     X being non empty Subset of N holds x"/\" preserves_inf_of X;

theorem :: YELLOW13:12
 for N being complete (non empty Poset), x being Element of N holds
  x"/\" is meet-preserving;

definition let N be complete (non empty Poset),
               x be Element of N;
 cluster x"/\" -> meet-preserving;
end;


begin  :: On the basis of topological spaces

theorem :: YELLOW13:13
   for T being anti-discrete non empty TopStruct, p being Point of T holds
  {the carrier of T} is Basis of p;

theorem :: YELLOW13:14
   for T being anti-discrete non empty TopStruct, p being Point of T,
     D being Basis of p holds D = {the carrier of T};

theorem :: YELLOW13:15
   for T being non empty TopSpace, P being Basis of T, p being Point of T holds
  {A where A is Subset of T: A in P & p in A} is Basis of p;

theorem :: YELLOW13:16
   for T being non empty TopStruct, A being Subset of T, p being Point of T
   holds
  p in Cl A iff
  for K being Basis of p, Q being Subset of T st Q in K holds A meets Q;

theorem :: YELLOW13:17
   for T being non empty TopStruct, A being Subset of T, p being Point of T
   holds
  p in Cl A iff
  ex K being Basis of p st for Q being Subset of T st Q in K holds A meets Q;

definition let T be TopStruct, p be Point of T;
 mode basis of p -> Subset-Family of T means
:: YELLOW13:def 1
  for A being Subset of T st p in Int A ex P being Subset of T st
   P in it & p in Int P & P c= A;
end;

definition let T be non empty TopSpace, p be Point of T;
 redefine mode basis of p means
:: YELLOW13:def 2
    for A being a_neighborhood of p ex P being a_neighborhood of p st
   P in it & P c= A;
end;

theorem :: YELLOW13:18
 for T being TopStruct, p being Point of T holds
  bool the carrier of T is basis of p;

theorem :: YELLOW13:19
 for T being non empty TopSpace, p being Point of T, P being basis of p holds
  P is non empty;

definition let T be non empty TopSpace, p be Point of T;
 cluster -> non empty basis of p;
end;

definition let T be TopStruct, p be Point of T;
 cluster non empty basis of p;
end;

definition let T be TopStruct, p be Point of T, P be basis of p;
 attr P is correct means
:: YELLOW13:def 3
  for A being Subset of T holds A in P iff p in Int A;
end;

definition let T be TopStruct, p be Point of T;
 cluster correct basis of p;
end;

theorem :: YELLOW13:20
   for T being TopStruct, p being Point of T holds
  {A where A is Subset of T: p in Int A} is correct basis of p;

definition let T be non empty TopSpace, p be Point of T;
 cluster non empty correct basis of p;
end;

theorem :: YELLOW13:21
   for T being anti-discrete non empty TopStruct, p being Point of T holds
  {the carrier of T} is correct basis of p;

theorem :: YELLOW13:22
   for T being anti-discrete non empty TopStruct, p being Point of T,
     D being correct basis of p holds D = {the carrier of T};

theorem :: YELLOW13:23
   for T being non empty TopSpace, p being Point of T,
     P being Basis of p holds P is basis of p;

definition let T be TopStruct;
 mode basis of T -> Subset-Family of T means
:: YELLOW13:def 4
  for p being Point of T holds it is basis of p;
end;

theorem :: YELLOW13:24
 for T being TopStruct holds bool the carrier of T is basis of T;

theorem :: YELLOW13:25
 for T being non empty TopSpace, P being basis of T holds P is non empty;

definition let T be non empty TopSpace;
 cluster -> non empty basis of T;
end;

definition let T be TopStruct;
 cluster non empty basis of T;
end;

theorem :: YELLOW13:26
   for T being non empty TopSpace, P being basis of T holds
  the topology of T c= UniCl Int P;

theorem :: YELLOW13:27
   for T being TopSpace, P being Basis of T holds P is basis of T;

definition let T be non empty TopSpace-like TopRelStr;
 attr T is topological_semilattice means
:: YELLOW13:def 5
  for f being map of [:T,T qua TopSpace:], T st f = inf_op T
   holds f is continuous;
end;

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

definition
 cluster reflexive trivial non empty TopSpace-like TopRelStr;
end;

theorem :: YELLOW13:28
 for T being topological_semilattice (non empty TopSpace-like TopRelStr),
     x being Element of T holds
  x"/\" is continuous;

definition let T be topological_semilattice(non empty TopSpace-like TopRelStr),
               x be Element of T;
 cluster x"/\" -> continuous;
end;