:: Introduction to Meet-Continuous Topological Lattices
:: by Artur Korni{\l}owicz
::
:: Received November 3, 1998
:: Copyright (c) 1998 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

proof end;

registration

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

end;

registration

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

end;

registration

cluster non empty trivial strict TopSpace-like TopStruct ;
existence
ex b₁ being TopSpace st
( b₁ is strict & not b₁ is empty & b₁ is trivial )

proof end;

end;

registration

cluster non empty finite TopSpace-like T_1 -> non empty discrete TopStruct ;
coherence
for b₁ being non empty TopSpace st b₁ is finite & b₁ is T_1 holds
b₁ is discrete

proof end;

end;

registration

cluster finite TopSpace-like -> compact TopStruct ;
coherence
for b₁ being TopSpace st b₁ is finite holds
b₁ is compact

proof end;

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 TopStruct ;
coherence
for b₁ being TopSpace st b₁ is discrete & not b₁ is empty holds
( b₁ is normal & b₁ is regular & b₁ is T_2 & b₁ is T_1 ) by Th2, Th3, Th4, Th5;

end;

registration

cluster non empty TopSpace-like T_4 -> non empty regular TopStruct ;
coherence
for b₁ being non empty TopSpace st b₁ is T_4 holds
b₁ is regular

proof end;

end;

registration

cluster TopSpace-like T_3 -> T_2 TopStruct ;
coherence
for b₁ being TopSpace st b₁ is T_3 holds
b₁ 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 one-to-one

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 one-to-one

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;

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

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 b₁ 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 b₁ & 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 b₃ being Subset-Family of T holds
( b₃ 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 b₃ & 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 b₁ being Subset-Family of T holds
( b₁ is basis of p iff for A being a_neighborhood of p ex P being a_neighborhood of p st
( P in b₁ & 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 b₃ being Subset-Family of T holds
( b₃ is basis of p iff for A being a_neighborhood of p ex P being a_neighborhood of p st
( P in b₃ & 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 basis of p;
coherence
for b₁ being basis of p holds not b₁ is empty by Th19;

end;

registration

let T be TopStruct ;
let p be Point of T;
cluster non empty basis of p;
existence
not for b₁ being basis of p holds b₁ 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

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

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 basis of p;
existence
ex b₁ being basis of p st b₁ 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 basis of p;
existence
ex b₁ being basis of p st
( not b₁ is empty & b₁ 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 b₁ being Subset-Family of T st
for p being Point of T holds b₁ is basis of p

proof end;

end;

:: deftheorem Def4 defines basis YELLOW13:def 4 :
for T being TopStruct
for b₂ being Subset-Family of T holds
( b₂ is basis of T iff for p being Point of T holds b₂ 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 basis of T;
coherence
for b₁ being basis of T holds not b₁ is empty by Th25;

end;

registration

let T be TopStruct ;
cluster non empty basis of T;
existence
not for b₁ being basis of T holds b₁ 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 non empty trivial TopSpace-like reflexive -> non empty TopSpace-like topological_semilattice TopRelStr ;
coherence
for b₁ being non empty TopSpace-like TopRelStr st b₁ is reflexive & b₁ is trivial holds
b₁ is topological_semilattice

proof end;

end;

registration

cluster non empty trivial TopSpace-like reflexive TopRelStr ;
existence
ex b₁ being TopRelStr st
( b₁ is reflexive & b₁ is trivial & not b₁ is empty & b₁ is TopSpace-like )

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;