:: Bases of Continuous Lattices
::  by Robert Milewski
::
:: Received November 28, 1998
:: Copyright (c) 1998-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, ORDERS_2, SUBSET_1, WAYBEL_8, WAYBEL_3, STRUCT_0,
      TARSKI, WAYBEL_0, XXREAL_0, RCOMP_1, RELAT_2, YELLOW_1, CARD_FIL,
      YELLOW_0, ORDINAL2, LATTICE3, EQREL_1, FINSET_1, CAT_1, REWRITE1,
      LATTICES, PRE_TOPC, CARD_1, SETFAM_1, RLVECT_3, ORDINAL1, XXREAL_2,
      ZFMISC_1, FUNCT_1, WELLORD2, RELAT_1, SEQM_3, YELLOW_2, WAYBEL_1,
      WELLORD1, FUNCT_2, WAYBEL23;
 notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, FUNCT_1, RELSET_1, PARTFUN1,
      FUNCT_2, DOMAIN_1, ORDERS_1, STRUCT_0, FINSET_1, ORDINAL1, CARD_1,
      PRE_TOPC, ORDERS_2, CANTOR_1, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2,
      WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_8;
 constructors DOMAIN_1, CANTOR_1, ORDERS_3, WAYBEL_8, RELSET_1, WAYBEL20,
      TOPS_2;
 registrations RELSET_1, FINSET_1, CARD_1, STRUCT_0, LATTICE3, YELLOW_0,
      WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_3, WAYBEL_7, WAYBEL_8, WAYBEL14;
 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;

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

registration
  let L be non empty RelStr;
  cluster infs-closed sups-closed non empty for 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;

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

registration
  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
;

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

registration
  let L be sup-Semilattice;
  cluster join-closed -> directed for 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;

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

registration
  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;

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

registration
  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 the set of all card B where B is Basis of T ;
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;

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

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

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

registration
  let L be continuous sup-Semilattice;
  cluster with_bottom for CLbasis of L;
  cluster with_top for 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;

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

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

registration
  cluster bounded non trivial for continuous LATTICE;
end;

registration
  let L be lower-bounded non trivial continuous sup-Semilattice;
  cluster -> non empty for 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 -> Function 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 -> Function 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;

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

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

registration
  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 -> Function 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;

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

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

registration
  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;

registration
  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;

theorem :: WAYBEL23:68  :: 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) = the set of all  downarrow b where b is Element of subrelstr B;

theorem :: WAYBEL23:69 :: 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:70
  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:71 :: 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:72 :: 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;

theorem :: WAYBEL23:73 :: WAYBEL31:1, AK, 21.02.2006
  for T be TopStruct for b be Basis of T holds weight T c= card b;

theorem :: WAYBEL23:74 :: WAYBEL31:1, AK, 21.02.2006
  for T be TopStruct ex b be Basis of T st card b = weight T;