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


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

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
proof end;
end;

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

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

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

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

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

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
proof end;
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
proof end;
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))
proof end;

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))
proof end;

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

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()
proof end;

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
proof end;

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
proof end;

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

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

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
proof end;

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}
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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 )
proof end;

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 )
proof end;

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 )
proof end;
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 ) )
proof end;
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
proof end;

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
proof end;

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
proof end;
end;

definition
let T be TopStruct ;
let p be Point of T;
let P be basis of p;
attr P 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 object ; :: according to TARSKI: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 to YELLOW13: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
proof end;
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 )
proof end;
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
proof end;

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}
proof end;

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
proof end;

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
proof end;
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
proof end;

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

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
proof end;
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)
proof end;

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

definition
let T be non empty TopSpace-like TopRelStr ;
attr T 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
cluster 1 -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
proof end;
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
proof end;

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