:: Introduction to Meet-Continuous Topological Lattices
:: by Artur Korni{\l}owicz
::
:: Received November 3, 1998
:: Copyright (c) 1998-2012 Association of Mizar Users


begin

theorem Th1: :: YELLOW13:1
for T being non empty T_1 TopSpace
for A being finite Subset of T holds A is closed
proofend;

registration
let T be non empty T_1 TopSpace;
cluster finite  ->  closed for Element of bool the carrier of T;
coherence
 for b1 being Subset of T st b1 is finite holds
b1 is closed by Th1;
end;

registration
let T be compact TopStruct ;
cluster [#] T ->  compact ;
coherence
 [#] T is compact by COMPTS_1:1;
end;

registration
cluster non empty finite TopSpace-like T_1  ->  non empty discrete for TopStruct ;
coherence
 for b1 being non empty TopSpace st b1 is finite & b1 is T_1 holds
b1 is discrete
proofend;
end;

registration
cluster finite TopSpace-like  ->  compact for TopStruct ;
coherence
 for b1 being TopSpace st b1 is finite holds
b1 is compact
proofend;
end;

theorem Th2: :: YELLOW13:2
for T being non empty discrete TopSpace holds T is normal
proofend;

theorem Th3: :: YELLOW13:3
for T being non empty discrete TopSpace holds T is regular
proofend;

theorem Th4: :: YELLOW13:4
for T being non empty discrete TopSpace holds T is T_2
proofend;

theorem Th5: :: YELLOW13:5
for T being non empty discrete TopSpace holds T is T_1
proofend;

registration
cluster non empty TopSpace-like discrete  ->  T_1 T_2 regular normal for TopStruct ;
coherence
 for b1 being TopSpace st b1 is discrete & not b1 is empty holds
( b1 is normal & b1 is regular & b1 is T_2 & b1 is T_1 ) by Th2, Th3, Th4, Th5;
end;

registration
cluster non empty TopSpace-like T_4  ->  non empty regular for TopStruct ;
coherence
 for b1 being non empty TopSpace st b1 is T_4 holds
b1 is regular
proofend;
end;

registration
cluster TopSpace-like T_3  ->  T_2 for TopStruct ;
coherence
 for b1 being TopSpace st b1 is T_3 holds
b1 is T_2
proofend;
end;

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

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

theorem Th8: :: YELLOW13:8
for N being non empty Poset holds IdsMap N is V13()
proofend;

registration
let N be non empty Poset;
cluster IdsMap N -> V13() ;
coherence
 IdsMap N is one-to-one by Th8;
end;

theorem Th9: :: YELLOW13:9
for N being finite LATTICE holds SupMap N is V13()
proofend;

registration
let N be finite LATTICE;
cluster SupMap N -> V13() ;
coherence
 SupMap N is one-to-one by Th9;
end;

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

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

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

registration
let N be non empty complete Poset;
let x be Element of N;
clusterx "/\"  ->  meet-preserving ;
coherence
 x "/\" is meet-preserving by Th12;
end;

begin

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

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

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

Lm1:  for T being non empty TopStruct
for A being Subset of T
for p being Point of T st p in Cl A holds
for K being Basis of
for Q being Subset of T st Q in K holds
A meets Q
proofend;

Lm2:  for T being non empty TopStruct
for A being Subset of T
for p being Point of T st ( for K being Basis of
for Q being Subset of T st Q in K holds
A meets Q ) holds
ex K being Basis of st
for Q being Subset of T st Q in K holds
A meets Q
proofend;

Lm3:  for T being non empty TopStruct
for A being Subset of T
for p being Point of T st ex K being Basis of st
for Q being Subset of T st Q in K holds
A meets Q holds
p in Cl A
proofend;

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

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

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

:: deftheorem Def1 defines basis YELLOW13:def_1_:_
 for T being TopStruct
for p being Point of T
for b3 being Subset-Family of T holds
( b3 is basis of p iff for A being Subset of T st p in Int A holds
ex P being Subset of T st
( P in b3 & p in Int P & P c= A ) );

definition
let T be non empty TopSpace;
let 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 );
compatibility
 for b1 being Subset-Family of T holds
( b1 is basis of p iff for A being a_neighborhood of p ex P being a_neighborhood of p st
( P in b1 & P c= A ) )
proofend;
end;

:: deftheorem  defines basis YELLOW13:def_2_:_
 for T being non empty TopSpace
for p being Point of T
for b3 being Subset-Family of T holds
( b3 is basis of p iff for A being a_neighborhood of p ex P being a_neighborhood of p st
( P in b3 & P c= A ) );

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

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

registration
let T be non empty TopSpace;
let p be Point of T;
cluster  ->  non empty for basis of p;
coherence
 for b1 being basis of p holds not b1 is empty by Th19;
end;

registration
let T be TopStruct ;
let p be Point of T;
cluster non empty for basis of p;
existence
 not for b1 being basis of p holds b1 is empty
proofend;
end;

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

:: deftheorem Def3 defines correct YELLOW13:def_3_:_
 for T being TopStruct
for p being Point of T
for P being basis of p holds
( P is correct iff for A being Subset of T holds
( A in P iff p in Int A ) );

Lm4: now__::_thesis:_for_T_being_TopStruct_
for_p_being_Point_of_T
for_K_being_set_st_K_=__{__A_where_A_is_Subset_of_T_:_p_in_Int_A__}__holds_
K_is_basis_of_p
let T be TopStruct ; ::_thesis: for p being Point of T
for K being set st K =  {  A where A is Subset of T : p in Int A  }  holds
K is basis of p
let p be Point of T; ::_thesis: for K being set st K =  {  A where A is Subset of T : p in Int A  }  holds
K is basis of p
let K be set ; ::_thesis: ( K =  {  A where A is Subset of T : p in Int A  }  implies K is basis of p )
assume A1: K =  {  A where A is Subset of T : p in Int A  }  ; ::_thesis: K is basis of p
 K c= bool the carrier of T
proof
let y be set ; :: according toTARSKI:def_3 ::_thesis: ( not y in K or y in bool the carrier of T )
assume  y in K ; ::_thesis: y in bool the carrier of T
then  ex A being Subset of T st
( y = A & p in Int A ) by A1;
hence  y in bool the carrier of T ; ::_thesis: verum
end;
then reconsider J = K as Subset-Family of T ;
reconsider J = J as Subset-Family of T ;
 for A being Subset of T st p in Int A holds
ex P being Subset of T st
( P in J & p in Int P & P c= A )
proof
let A be Subset of T; ::_thesis: ( p in Int A implies ex P being Subset of T st
( P in J & p in Int P & P c= A ) )
assume A2: p in Int A ; ::_thesis: ex P being Subset of T st
( P in J & p in Int P & P c= A )
take P = A; ::_thesis: ( P in J & p in Int P & P c= A )
thus  ( P in J & p in Int P & P c= A ) by A1, A2; ::_thesis: verum
end;
hence  K is basis of p by Def1; ::_thesis: verum
end;

Lm5: now__::_thesis:_for_T_being_TopStruct_
for_p_being_Point_of_T
for_K_being_basis_of_p_st_K_=__{__A_where_A_is_Subset_of_T_:_p_in_Int_A__}__holds_
K_is_correct
let T be TopStruct ; ::_thesis: for p being Point of T
for K being basis of p st K =  {  A where A is Subset of T : p in Int A  }  holds
K is correct
let p be Point of T; ::_thesis: for K being basis of p st K =  {  A where A is Subset of T : p in Int A  }  holds
K is correct
let K be basis of p; ::_thesis: ( K =  {  A where A is Subset of T : p in Int A  }  implies K is correct )
assume A1: K =  {  A where A is Subset of T : p in Int A  }  ; ::_thesis: K is correct
thus  K is correct ::_thesis: verum
proof
let A be Subset of T; :: according toYELLOW13:def_3 ::_thesis: ( A in K iff p in Int A )
hereby  ::_thesis: ( p in Int A implies A in K )
assume  A in K ; ::_thesis: p in Int A
then  ex M being Subset of T st
( A = M & p in Int M ) by A1;
hence  p in Int A ; ::_thesis: verum
end;
thus  ( p in Int A implies A in K ) by A1; ::_thesis: verum
end;
end;

registration
let T be TopStruct ;
let p be Point of T;
cluster correct for basis of p;
existence
 ex b1 being basis of p st b1 is correct
proofend;
end;

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

registration
let T be non empty TopSpace;
let p be Point of T;
cluster non empty correct for basis of p;
existence
 ex b1 being basis of p st
( not b1 is empty & b1 is correct )
proofend;
end;

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

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

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

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

:: deftheorem Def4 defines basis YELLOW13:def_4_:_
 for T being TopStruct
for b2 being Subset-Family of T holds
( b2 is basis of T iff for p being Point of T holds b2 is basis of p );

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

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

registration
let T be non empty TopSpace;
cluster  ->  non empty for basis of T;
coherence
 for b1 being basis of T holds not b1 is empty by Th25;
end;

registration
let T be TopStruct ;
cluster non empty for basis of T;
existence
 not for b1 being basis of T holds b1 is empty
proofend;
end;

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

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

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

:: deftheorem Def5 defines topological_semilattice YELLOW13:def_5_:_
 for T being non empty TopSpace-like TopRelStr holds
( T is topological_semilattice iff for f being Function of [:T,T:],T st f = inf_op T holds
f is continuous );

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

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

registration
let T be non empty TopSpace-like topological_semilattice TopRelStr ;
let x be Element of T;
clusterx "/\"  ->  continuous ;
coherence
 x "/\" is continuous by Th28;
end;