:: On the Order-consistent Topology of Complete and Uncomplete
:: Lattices
::  by Ewa Gr\c{a}dzka
::
:: Received May 23, 2000
:: Copyright (c) 2000-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, WAYBEL_9, WAYBEL_0, SUBSET_1, CANTOR_1, WAYBEL11,
      STRUCT_0, REWRITE1, PRELAMB, YELLOW_9, PRE_TOPC, RELAT_2, ORDINAL2,
      CONNSP_2, ZFMISC_1, TARSKI, SETFAM_1, XXREAL_0, RLVECT_3, WAYBEL19,
      RCOMP_1, FINSET_1, YELLOW_2, RELAT_1, TOPS_1, LATTICE3, YELLOW_0,
      FUNCT_1, ORDERS_2, LATTICES, SEQM_3, YELLOW_6, CARD_FIL, EQREL_1, PROB_1,
      T_0TOPSP, ARYTM_3, WAYBEL_7, WAYBEL32, CARD_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FINSET_1,
      SETFAM_1, FUNCT_2, DOMAIN_1, STRUCT_0, ORDERS_2, LATTICE3, PRE_TOPC,
      TOPS_1, CONNSP_2, T_0TOPSP, YELLOW_0, WAYBEL_0, CANTOR_1, YELLOW_2,
      WAYBEL_2, YELLOW_6, WAYBEL_9, RELSET_1, WAYBEL11, WAYBEL19, YELLOW_9;
 constructors DOMAIN_1, TOPS_1, TOPS_2, CONNSP_2, LATTICE3, CANTOR_1, WAYBEL_1,
      WAYBEL11, YELLOW_9, RELSET_1, WAYBEL_2;
 registrations SUBSET_1, FUNCT_1, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0,
      WAYBEL_3, YELLOW_6, WAYBEL11, YELLOW_9, WAYBEL21, YELLOW14, WAYBEL29,
      TOPS_1, CARD_1, ORDINAL1, RELSET_1;
 requirements SUBSET, BOOLE;


begin

definition
  let T be non empty TopRelStr;
  attr T is upper means
:: WAYBEL32:def 1

  the set of all (downarrow x)` where x is Element of T is prebasis of T;
end;

registration
  cluster Scott up-complete strict for TopLattice;
end;

definition
  let T be TopSpace-like non empty reflexive TopRelStr;
  attr T is order_consistent means
:: WAYBEL32:def 2

  for x being Element of T holds downarrow x = Cl {x} &
  for N being eventually-directed net of T st x = sup N
  for V being a_neighborhood of x holds N is_eventually_in V;
end;

registration
  cluster  -> upper for 1-element reflexive TopSpace-like TopRelStr;
end;

registration
  cluster upper trivial up-complete strict for TopLattice;
end;

theorem :: WAYBEL32:1
  for T being upper up-complete non empty TopPoset
  for A being Subset of T st A is open holds A is upper;

theorem :: WAYBEL32:2
  for T being up-complete non empty TopPoset holds
  T is upper implies T is order_consistent;

theorem :: WAYBEL32:3
  for R being up-complete non empty reflexive transitive antisymmetric
  RelStr ex T being TopAugmentation of R st T is Scott;

theorem :: WAYBEL32:4
  for R being up-complete non empty Poset
  for T being TopAugmentation of R holds T is Scott implies T is correct;

registration
  let R be up-complete non empty reflexive transitive antisymmetric RelStr;
  cluster Scott -> correct for TopAugmentation of R;
end;

registration
  let R be up-complete non empty reflexive transitive antisymmetric RelStr;
  cluster Scott correct for TopAugmentation of R;
end;

theorem :: WAYBEL32:5   :: Remark 1.4 (ii)
  for T being Scott up-complete non empty reflexive transitive antisymmetric
  TopRelStr, x being Element of T holds Cl {x} = downarrow x;

theorem :: WAYBEL32:6
  for T being up-complete Scott non empty TopPoset holds
  T is order_consistent;

theorem :: WAYBEL32:7
  for R being /\-complete Semilattice, Z be net of R, D be Subset of R st
  D = the set of all "/\"({Z.k where k is Element of Z: k >= j},R)
  where j is Element of Z holds D is non empty directed;

theorem :: WAYBEL32:8
  for R being /\-complete Semilattice, S being Subset of R,
  a being Element of R holds a in S implies "/\"(S,R) <= a;

theorem :: WAYBEL32:9
  for R being /\-complete Semilattice, N being monotone reflexive net of R
  holds lim_inf N = sup N;

theorem :: WAYBEL32:10
  for R being /\-complete Semilattice for S being Subset of R
  holds S in the topology of ConvergenceSpace Scott-Convergence R
  iff S is inaccessible upper;

theorem :: WAYBEL32:11
  for R being /\-complete up-complete Semilattice,
  T being TopAugmentation of R st the topology of T = sigma R holds T is Scott;

registration
  let R be /\-complete up-complete Semilattice;
  cluster strict Scott correct for TopAugmentation of R;
end;

theorem :: WAYBEL32:12
  for S being up-complete /\-complete Semilattice,
  T being Scott TopAugmentation of S holds sigma S = the topology of T;

theorem :: WAYBEL32:13     :: Remark 1.4 (iii)
  for T being Scott up-complete non empty reflexive transitive antisymmetric
  TopRelStr holds T is T_0-TopSpace;

registration
  let R be up-complete non empty reflexive transitive antisymmetric RelStr;
  cluster -> up-complete for TopAugmentation of R;
end;

theorem :: WAYBEL32:14
  for R being up-complete non empty reflexive transitive antisymmetric
  RelStr for T being Scott TopAugmentation of R, x being Element of T,
  A being upper Subset of T st not x in A
  holds (downarrow x)` is a_neighborhood of A;

theorem :: WAYBEL32:15     ::Remark 1.4 (iv)
  for R being up-complete non empty reflexive transitive antisymmetric
  TopRelStr for T being Scott TopAugmentation of R, S being upper Subset of T
  ex F being Subset-Family of T st S = meet F &
  for X being Subset of T st X in F holds X is a_neighborhood of S;

theorem :: WAYBEL32:16    ::Remark 1.4 (v)
  for T being Scott up-complete non empty reflexive transitive antisymmetric
  TopRelStr, S being Subset of T holds S is open iff S is upper property(S);

theorem :: WAYBEL32:17
  for R being up-complete non empty reflexive transitive antisymmetric
  TopRelStr, S being non empty directed Subset of R,
  a being Element of R holds a in S implies a <= "\/"(S, R);

::Remark 1.4 (vi)

registration
  let T be up-complete non empty reflexive transitive antisymmetric
  TopRelStr;
  cluster lower -> property(S) for Subset of T;
end;

theorem :: WAYBEL32:18
  for T being finite up-complete non empty Poset,
  S being Subset of T holds S is inaccessible;

theorem :: WAYBEL32:19
  for R being complete connected LATTICE,
  T being Scott TopAugmentation of R, x being Element of T holds
  (downarrow x)` is open;

theorem :: WAYBEL32:20
  for R being complete connected LATTICE,
  T being Scott TopAugmentation of R, S being Subset of T holds
  S is open iff S = the carrier of T or S in the set of all (downarrow x)`
  where x is Element of T;

registration
  let R be up-complete non empty Poset;
  cluster order_consistent for correct TopAugmentation of R;
end;

registration
  cluster order_consistent complete for TopLattice;
end;

theorem :: WAYBEL32:21
  for R being non empty TopRelStr for A being Subset of R holds
  (for x being Element of R holds downarrow x = Cl {x}) implies
  (A is open implies A is upper);

theorem :: WAYBEL32:22
  for R being non empty TopRelStr for A being Subset of R holds
  (for x being Element of R holds downarrow x = Cl {x}) implies
  for A being Subset of R st A is closed holds A is lower;

definition
  let S be non empty 1-sorted, R be non empty RelStr,
  f be Function of the carrier of R,the carrier of S;
  func R*'f -> strict non empty NetStr over S means
:: WAYBEL32:def 3

  the RelStr of it = the RelStr of R & the mapping of it = f;
end;

registration
  let S be non empty 1-sorted, R be non empty transitive RelStr,
  f be Function of the carrier of R,the carrier of S;
  cluster R*'f -> transitive;
end;

registration
  let S be non empty 1-sorted, R be non empty directed RelStr,
  f be Function of the carrier of R,the carrier of S;
  cluster R*'f -> directed;
end;

definition
  let R be non empty RelStr, N be prenet of R;
  func inf_net N -> strict prenet of R means
:: WAYBEL32:def 4

  ex f being Function of N,R st it = N*'f & for i being Element of N holds
  f.i = "/\"({N.k where k is Element of N: k >= i},R);
end;

registration
  let R be non empty RelStr, N be net of R;
  cluster inf_net N -> transitive;
end;

registration
  let R be non empty RelStr, N be net of R;
  cluster inf_net N -> directed;
end;

registration
  let R be /\-complete non empty reflexive antisymmetric RelStr,
  N be net of R;
  cluster inf_net N -> monotone;
end;

registration
  let R be /\-complete non empty reflexive antisymmetric RelStr,
  N be net of R;
  cluster inf_net N -> eventually-directed;
end;

theorem :: WAYBEL32:23
  for R being non empty RelStr, N being net of R
  holds rng the mapping of (inf_net N) =
  the set of all "/\"({N.i where i is Element of N: i >= j},R) where
  j is Element of N;

theorem :: WAYBEL32:24
  for R being up-complete /\-complete LATTICE, N being net of R holds
  sup inf_net N = lim_inf N;

theorem :: WAYBEL32:25
  for R being up-complete /\-complete LATTICE, N being net of R,
  i being Element of N holds sup inf_net N = lim_inf (N|i);

theorem :: WAYBEL32:26
  for R being /\-complete Semilattice, N being net of R,
  V being upper Subset of R holds
  inf_net N is_eventually_in V implies N is_eventually_in V;

theorem :: WAYBEL32:27
  for R being /\-complete Semilattice, N being net of R,
  V being lower Subset of R holds
  N is_eventually_in V implies inf_net N is_eventually_in V;

theorem :: WAYBEL32:28
  for R being order_consistent up-complete /\-complete non empty TopLattice
  for N being net of R, x being Element of R holds
  x <= lim_inf N implies x is_a_cluster_point_of N;

theorem :: WAYBEL32:29
  for R being order_consistent up-complete /\-complete non empty TopLattice
  for N being eventually-directed net of R, x being Element of R holds
  x <= lim_inf N iff x is_a_cluster_point_of N;