:: Meet Continuous Lattices Revisited
:: by Artur Korni{\l}owicz
::
:: Received January 6, 2000
:: Copyright (c) 2000-2012 Association of Mizar Users


begin

theorem Th1: :: WAYBEL30:1
for x being set
for D being non empty set holds x /\ (union D) = union  {  (x /\ d) where d is Element of D : verum  }
proofend;

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

Lm1: now__::_thesis:_for_R_being_non_empty_reflexive_transitive_RelStr_
for_D_being_non_empty_directed_Subset_of_(InclPoset_(Ids_R))
for_UD_being_Element_of_(InclPoset_(Ids_R))_st_UD_=_union_D_holds_
D_is_<=_than_UD
let R be non empty reflexive transitive RelStr ; ::_thesis: for D being non empty directed Subset of (InclPoset (Ids R))
for UD being Element of (InclPoset (Ids R)) st UD = union D holds
D is_<=_than UD
let D be non empty directed Subset of (InclPoset (Ids R)); ::_thesis: for UD being Element of (InclPoset (Ids R)) st UD = union D holds
D is_<=_than UD
let UD be Element of (InclPoset (Ids R)); ::_thesis: ( UD = union D implies D is_<=_than UD )
assume A1: UD = union D ; ::_thesis: D is_<=_than UD
thus  D is_<=_than UD ::_thesis: verum
proof
let d be Element of (InclPoset (Ids R)); :: according toLATTICE3:def_9 ::_thesis: ( not d in D or d <= UD )
assume A2: d in D ; ::_thesis: d <= UD
 d c= UD
proof
let a be set ; :: according toTARSKI:def_3 ::_thesis: ( not a in d or a in UD )
assume  a in d ; ::_thesis: a in UD
hence  a in UD by A1, A2, TARSKI:def_4; ::_thesis: verum
end;
hence  d <= UD by YELLOW_1:3; ::_thesis: verum
end;
end;

Lm2: now__::_thesis:_for_R_being_non_empty_reflexive_transitive_RelStr_
for_D_being_non_empty_directed_Subset_of_(InclPoset_(Ids_R))
for_UD_being_Element_of_(InclPoset_(Ids_R))_st_UD_=_union_D_holds_
for_b_being_Element_of_(InclPoset_(Ids_R))_st_b_is_>=_than_D_holds_
UD_<=_b
let R be non empty reflexive transitive RelStr ; ::_thesis: for D being non empty directed Subset of (InclPoset (Ids R))
for UD being Element of (InclPoset (Ids R)) st UD = union D holds
for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds
UD <= b
let D be non empty directed Subset of (InclPoset (Ids R)); ::_thesis: for UD being Element of (InclPoset (Ids R)) st UD = union D holds
for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds
UD <= b
let UD be Element of (InclPoset (Ids R)); ::_thesis: ( UD = union D implies for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds
UD <= b )
assume A1: UD = union D ; ::_thesis: for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds
UD <= b
thus  for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds
UD <= b ::_thesis: verum
proof
let b be Element of (InclPoset (Ids R)); ::_thesis: ( b is_>=_than D implies UD <= b )
assume A2: for a being Element of (InclPoset (Ids R)) st a in D holds
b >= a ; :: according toLATTICE3:def_9 ::_thesis: UD <= b
 UD c= b
proof
let x be set ; :: according toTARSKI:def_3 ::_thesis: ( not x in UD or x in b )
assume  x in UD ; ::_thesis: x in b
then consider Z being set  such that
A3: x in Z and
A4: Z in D by A1, TARSKI:def_4;
reconsider Z = Z as Element of (InclPoset (Ids R)) by A4;
 b >= Z by A2, A4;
then  Z c= b by YELLOW_1:3;
hence  x in b by A3; ::_thesis: verum
end;
hence  UD <= b by YELLOW_1:3; ::_thesis: verum
end;
end;

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

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

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

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

registration
let R be 1 -element RelStr ;
cluster  ->  trivial for TopAugmentation of R;
coherence
 for b1 being TopAugmentation of R holds b1 is trivial
proofend;
end;

theorem :: WAYBEL30:5
for S being complete Scott TopLattice
for T being complete LATTICE
for A being Scott TopAugmentation of T st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) holds
TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #)
proofend;

theorem :: WAYBEL30:6
for N being complete Lawson TopLattice
for T being complete LATTICE
for A being correct Lawson TopAugmentation of T st RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of T, the InternalRel of T #) holds
TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #)
proofend;

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

registration
let A be complete LATTICE;
cluster lambda A ->  non empty ;
coherence
 not lambda A is empty
proofend;
end;

registration
let S be complete Scott TopLattice;
cluster InclPoset (sigma S) ->  non trivial complete ;
coherence
 ( InclPoset (sigma S) is complete &amp; not InclPoset (sigma S) is trivial ) ;
end;

registration
let N be complete Lawson TopLattice;
cluster InclPoset (sigma N) ->  non trivial complete ;
coherence
 ( InclPoset (sigma N) is complete &amp; not InclPoset (sigma N) is trivial ) ;
cluster InclPoset (lambda N) ->  non trivial complete ;
coherence
 ( InclPoset (lambda N) is complete &amp; not InclPoset (lambda N) is trivial )
proofend;
end;

theorem Th8: :: 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 &amp; F is finite )  }
proofend;

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

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

theorem :: WAYBEL30:11
for M, N being complete LATTICE st RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of N, the InternalRel of N #) holds
lambda M = lambda N
proofend;

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

registration
cluster1 -element TopSpace-like reflexive  -> 1 -element reflexive Scott for TopRelStr ;
coherence
 for b1 being 1 -element reflexive TopRelStr st b1 is TopSpace-like holds
b1 is Scott
proofend;
end;

registration
cluster trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete  ->  complete Lawson for TopRelStr ;
coherence
 for b1 being complete TopLattice st b1 is trivial holds
b1 is Lawson
proofend;
end;

registration
cluster non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete strict Scott continuous non void meet-continuous for TopRelStr ;
existence
 ex b1 being complete TopLattice st
( b1 is strict &amp; b1 is continuous &amp; b1 is lower-bounded &amp; b1 is meet-continuous &amp; b1 is Scott )
proofend;
end;

registration
cluster non empty TopSpace-like Hausdorff reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete strict Lawson continuous non void compact for TopRelStr ;
existence
 ex b1 being complete TopLattice st
( b1 is strict &amp; b1 is continuous &amp; b1 is compact &amp; b1 is Hausdorff &amp; b1 is Lawson )
proofend;
end;

scheme :: WAYBEL30:sch 1
EmptySch{ F1() ->  Scott TopLattice, F2() ->  set , F3( set ) ->  set } :
  {  F3(w) where w is Element of F1() : w in {}  }  = {}
proofend;

theorem Th13: :: WAYBEL30:13
for N being meet-continuous LATTICE
for A being Subset of N st A is property(S) holds
uparrow A is property(S)
proofend;

registration
let N be meet-continuous LATTICE;
let A be property(S) Subset of N;
cluster uparrow A ->  property(S) ;
coherence
 uparrow A is property(S) by Th13;
end;

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

theorem Th15: :: WAYBEL30:15
for N being complete Lawson meet-continuous TopLattice
for S being Scott TopAugmentation of N
for A being Subset of N
for J being Subset of S st A = J &amp; A is open holds
uparrow J is open
proofend;

theorem Th16: :: WAYBEL30:16
for N being complete Lawson meet-continuous TopLattice
for S being Scott TopAugmentation of N
for x being Point of S
for 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
proofend;

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

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

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

:: Proposition 2.2, p. 153
theorem Th20: :: WAYBEL30:20
for M, N being complete LATTICE
for P being correct Lawson TopAugmentation of [:M,N:]
for Q being correct Lawson TopAugmentation of M
for R being correct Lawson TopAugmentation of N st InclPoset (sigma N) is continuous holds
TopStruct(# the carrier of P, the topology of P #) = [:Q,R:]
proofend;

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

registration
let N be complete Lawson meet-continuous TopLattice;
let x be Element of N;
clusterx "/\"  ->  continuous ;
coherence
 x "/\" is continuous by Th21;
end;

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

Lm3: now__::_thesis:_for_S,_T,_x1,_x2_being_set_st_x1_in_S_&amp;_x2_in_T_holds_
<:(pr2_(S,T)),(pr1_(S,T)):>_._[x1,x2]_=_[x2,x1]
let S, T, x1, x2 be set ; ::_thesis: ( x1 in S &amp; x2 in T implies <:(pr2 (S,T)),(pr1 (S,T)):> . [x1,x2] = [x2,x1] )
assume that
A1: x1 in S and
A2: x2 in T ; ::_thesis: <:(pr2 (S,T)),(pr1 (S,T)):> . [x1,x2] = [x2,x1]
A3: dom <:(pr2 (S,T)),(pr1 (S,T)):> = (dom (pr2 (S,T))) /\ (dom (pr1 (S,T))) by FUNCT_3:def_7
.= (dom (pr2 (S,T))) /\ [:S,T:] by FUNCT_3:def_4
.= [:S,T:] /\ [:S,T:] by FUNCT_3:def_5
.= [:S,T:] ;
 [x1,x2] in [:S,T:] by A1, A2, ZFMISC_1:87;
hence <:(pr2 (S,T)),(pr1 (S,T)):> . [x1,x2] = [((pr2 (S,T)) . (x1,x2)),((pr1 (S,T)) . (x1,x2))] by A3, FUNCT_3:def_7
.= [x2,((pr1 (S,T)) . (x1,x2))] by A1, A2, FUNCT_3:def_5
.= [x2,x1] by A1, A2, FUNCT_3:def_4 ;
::_thesis: verum
end;

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

:: Definition 2.5, p. 154
definition
let N be non empty reflexive RelStr ;
let X be Subset of N;
funcX ^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  }  ;
coherence
  {  u where u is Element of N : for D being non empty directed Subset of N st u <= sup D holds
X meets D  }  is Subset of N
proofend;
end;

:: deftheorem  defines ^0 WAYBEL30:def_1_:_
 for N being non empty reflexive RelStr
for X being Subset of N holds X ^0 =  {  u where u is Element of N : for D being non empty directed Subset of N st u <= sup D holds
X meets D  }  ;

registration
let N be non empty reflexive antisymmetric RelStr ;
let X be empty Subset of N;
clusterX ^0  ->  empty ;
coherence
 X ^0 is empty
proofend;
end;

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

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

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

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

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

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

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

registration
cluster TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Lawson continuous  ->  Hausdorff complete for TopRelStr ;
coherence
 for b1 being complete TopLattice st b1 is continuous &amp; b1 is Lawson holds
b1 is Hausdorff ;
cluster TopSpace-like Hausdorff reflexive transitive antisymmetric with_suprema with_infima complete Lawson meet-continuous  ->  complete continuous for TopRelStr ;
coherence
 for b1 being complete TopLattice st b1 is meet-continuous &amp; b1 is Lawson &amp; b1 is Hausdorff holds
b1 is continuous by Th30;
end;

:: Definition 2.10, p. 155
definition
let N be non empty TopRelStr ;
attrN 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 ;
attrN 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 &amp; A is compact );
attrN is with_open_semilattices  means :Def4: :: 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;

:: deftheorem  defines with_small_semilattices WAYBEL30:def_2_:_
 for N being non empty TopRelStr holds
( N is with_small_semilattices iff 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 );

:: deftheorem  defines with_compact_semilattices WAYBEL30:def_3_:_
 for N being non empty TopRelStr holds
( N is with_compact_semilattices iff 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 &amp; A is compact ) );

:: deftheorem Def4 defines with_open_semilattices WAYBEL30:def_4_:_
 for N being non empty TopRelStr holds
( N is with_open_semilattices iff 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 );

registration
cluster non empty TopSpace-like with_open_semilattices  ->  non empty TopSpace-like with_small_semilattices for TopRelStr ;
coherence
 for b1 being non empty TopSpace-like TopRelStr st b1 is with_open_semilattices holds
b1 is with_small_semilattices
proofend;
cluster non empty TopSpace-like with_compact_semilattices  ->  non empty TopSpace-like with_small_semilattices for TopRelStr ;
coherence
 for b1 being non empty TopSpace-like TopRelStr st b1 is with_compact_semilattices holds
b1 is with_small_semilattices
proofend;
cluster non empty anti-discrete  ->  non empty with_small_semilattices with_open_semilattices for TopRelStr ;
coherence
 for b1 being non empty TopRelStr st b1 is anti-discrete holds
( b1 is with_small_semilattices &amp; b1 is with_open_semilattices )
proofend;
cluster1 -element TopSpace-like reflexive  -> 1 -element with_compact_semilattices for TopRelStr ;
coherence
 for b1 being 1 -element TopRelStr st b1 is reflexive &amp; b1 is TopSpace-like holds
b1 is with_compact_semilattices
proofend;
end;

registration
cluster non empty trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima strict lower non void for TopRelStr ;
existence
 ex b1 being TopLattice st
( b1 is strict &amp; b1 is trivial &amp; b1 is lower )
proofend;
end;

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

:: Theorem 2.11, p. 155
theorem Th32: :: WAYBEL30:32
for N being complete Lawson meet-continuous 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 )
proofend;

:: Theorem 2.12, p. 155, r => l
theorem Th33: :: WAYBEL30:33
for N being complete Lawson 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 &amp; A in sigma S )  }  c=  {  (inf J) where J is Subset of N : ( x in J &amp; J in lambda N )  }
proofend;

:: Theorem 2.12, p. 155
theorem Th34: :: WAYBEL30:34
for N being complete Lawson meet-continuous 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 &amp; A in sigma S )  }  =  {  (inf J) where J is Subset of N : ( x in J &amp; J in lambda N )  }
proofend;

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

registration
cluster TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Lawson continuous  ->  complete Lawson with_open_semilattices for TopRelStr ;
coherence
 for b1 being complete Lawson TopLattice st b1 is continuous holds
b1 is with_open_semilattices by Th35;
end;

registration
let N be complete Lawson continuous TopLattice;
cluster InclPoset (sigma N) ->  continuous ;
coherence
 InclPoset (sigma N) is continuous by Th35;
end;

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

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

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

:: Theorem 2.13, p. 155, 1 <=> 4
theorem :: WAYBEL30:39
for N being complete Lawson meet-continuous 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 &amp; V in lambda N )  }  ,N) )
proofend;

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

registration
let N be complete algebraic Lawson meet-continuous TopLattice;
cluster InclPoset (sigma N) ->  algebraic ;
coherence
 InclPoset (sigma N) is algebraic by Th40;
end;