:: The Lattice of Domains of a Topological Space
:: by Toshihiko Watanabe
::
:: Received June 12, 1992
:: Copyright (c) 1992-2016 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 PRE_TOPC, SUBSET_1, XBOOLE_0, TARSKI, TOPS_1, RCOMP_1, SETFAM_1,
ZFMISC_1, STRUCT_0, BINOP_1, FUNCT_1, MCART_1, LATTICES, EQREL_1,
REALSET1, NAT_LAT, TDLAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, REALSET1, STRUCT_0, PRE_TOPC,
LATTICES, BINOP_1, TOPS_1, FUNCT_1, DOMAIN_1, FUNCT_2, NAT_LAT;
constructors PARTFUN1, BINOP_1, REALSET1, TOPS_1, NAT_LAT;
registrations SUBSET_1, REALSET1, LATTICES, TOPS_1, RELAT_1, PRE_TOPC;
requirements BOOLE, SUBSET;
begin
:: 1. Preliminary Theorems on Subsets of Topological Spaces.
reserve T for 1-sorted;
theorem :: TDLAT_1:1
for A,B being Subset of T holds A \/ B = [#] T iff A` c= B;
theorem :: TDLAT_1:2
for A,B being Subset of T holds A misses B iff B c= A`;
reserve T for TopSpace;
theorem :: TDLAT_1:3
for A being Subset of T holds Cl Int Cl A c= Cl A;
theorem :: TDLAT_1:4
for A being Subset of T holds Int A c= Int Cl Int A;
theorem :: TDLAT_1:5
for A being Subset of T holds Int Cl A = Int Cl Int Cl A;
theorem :: TDLAT_1:6
for A,B being Subset of T st A is closed or B is closed holds Cl
Int A \/ Cl Int B = Cl Int(A \/ B);
theorem :: TDLAT_1:7
for A,B being Subset of T st A is open or B is open holds Int Cl
A /\ Int Cl B = Int Cl(A /\ B);
theorem :: TDLAT_1:8
for A being Subset of T holds Int(A /\ Cl A`) = {} T;
theorem :: TDLAT_1:9
for A being Subset of T holds Cl(A \/ Int A`) = [#] T;
theorem :: TDLAT_1:10
for A,B being Subset of T holds Int(Cl(A \/ (Int(Cl B) \/ B)))
\/ (A \/ (Int(Cl B) \/ B)) = Int Cl(A \/ B) \/ (A \/ B);
theorem :: TDLAT_1:11
for A,C being Subset of T holds Int(Cl((Int(Cl A) \/ A) \/ C)) \/ ((
Int(Cl A) \/ A) \/ C) = Int Cl(A \/ C) \/ (A \/ C);
theorem :: TDLAT_1:12
for A,B being Subset of T holds Cl(Int(A /\ (Cl(Int B) /\ B)))
/\ (A /\ (Cl(Int B) /\ B)) = Cl Int(A /\ B) /\ (A /\ B);
theorem :: TDLAT_1:13
for A,C being Subset of T holds Cl(Int((Cl(Int A) /\ A) /\ C)) /\ ((Cl
(Int A) /\ A) /\ C) = Cl Int(A /\ C) /\ (A /\ C);
begin
:: 2. Properties of Domains_of of Topological Spaces.
theorem :: TDLAT_1:14
{}T is condensed;
theorem :: TDLAT_1:15
[#] T is condensed;
theorem :: TDLAT_1:16
for A being Subset of T st A is condensed holds A` is condensed;
theorem :: TDLAT_1:17
for A,B being Subset of T st A is condensed & B is condensed
holds Int(Cl(A \/ B)) \/ (A \/ B) is condensed & Cl(Int(A /\ B)) /\ (A /\ B) is
condensed;
theorem :: TDLAT_1:18
{} T is closed_condensed;
theorem :: TDLAT_1:19
[#] T is closed_condensed;
theorem :: TDLAT_1:20
{} T is open_condensed;
theorem :: TDLAT_1:21
[#] T is open_condensed;
theorem :: TDLAT_1:22
for A being Subset of T holds Cl(Int A) is closed_condensed;
theorem :: TDLAT_1:23
for A being Subset of T holds Int(Cl A) is open_condensed;
theorem :: TDLAT_1:24
for A being Subset of T st A is condensed holds Cl A is closed_condensed;
theorem :: TDLAT_1:25
for A being Subset of T st A is condensed holds Int A is open_condensed;
theorem :: TDLAT_1:26
for A being Subset of T st A is condensed holds Cl A` is
closed_condensed;
theorem :: TDLAT_1:27
for A being Subset of T st A is condensed holds Int A` is
open_condensed;
theorem :: TDLAT_1:28
for A,B,C being Subset of T st A is closed_condensed & B is
closed_condensed & C is closed_condensed holds Cl(Int(A /\ (Cl(Int(B /\ C)))))
= Cl(Int((Cl(Int(A /\ B)) /\ C)));
theorem :: TDLAT_1:29
for A,B,C being Subset of T st A is open_condensed & B is
open_condensed & C is open_condensed holds Int(Cl(A \/ (Int(Cl(B \/ C))))) =
Int(Cl((Int(Cl(A \/ B)) \/ C)));
begin
:: 3. The Lattice of Domains.
definition
let T be TopStruct;
func Domains_of T -> Subset-Family of T equals
:: TDLAT_1:def 1
{ A where A is Subset of T :
A is condensed };
end;
registration
let T be TopSpace;
cluster Domains_of T -> non empty;
end;
definition
let T be TopSpace;
func Domains_Union T -> BinOp of Domains_of T means
:: TDLAT_1:def 2
for A,B being
Element of Domains_of T holds it.(A,B) = Int(Cl(A \/ B)) \/ (A \/ B);
end;
notation
let T be TopSpace;
synonym D-Union T for Domains_Union T;
end;
definition
let T be TopSpace;
func Domains_Meet T -> BinOp of Domains_of T means
:: TDLAT_1:def 3
for A,B being
Element of Domains_of T holds it.(A,B) = Cl(Int(A /\ B)) /\ (A /\ B);
end;
notation
let T be TopSpace;
synonym D-Meet T for Domains_Meet T;
end;
theorem :: TDLAT_1:30
for T being TopSpace holds LattStr(#Domains_of T,D-Union T,
D-Meet T#) is C_Lattice;
definition
let T be TopSpace;
func Domains_Lattice T -> C_Lattice equals
:: TDLAT_1:def 4
LattStr(#Domains_of T,
Domains_Union T,Domains_Meet T#);
end;
begin
:: 4. The Lattice of Closed Domains.
definition
let T be TopStruct;
func Closed_Domains_of T -> Subset-Family of T equals
:: TDLAT_1:def 5
{ A where A is Subset
of T : A is closed_condensed };
end;
registration
let T be TopSpace;
cluster Closed_Domains_of T -> non empty;
end;
theorem :: TDLAT_1:31
for T being TopSpace holds Closed_Domains_of T c= Domains_of T;
definition
let T be TopSpace;
func Closed_Domains_Union T -> BinOp of Closed_Domains_of T means
:: TDLAT_1:def 6
for A,B being Element of Closed_Domains_of T holds it.(A,B) = A \/ B;
end;
notation
let T be TopSpace;
synonym CLD-Union T for Closed_Domains_Union T;
end;
theorem :: TDLAT_1:32
for A,B being Element of Closed_Domains_of T holds (CLD-Union T)
.(A,B) = (D-Union T).(A,B);
definition
let T be TopSpace;
func Closed_Domains_Meet T -> BinOp of Closed_Domains_of T means
:: TDLAT_1:def 7
for
A,B being Element of Closed_Domains_of T holds it.(A,B) = Cl(Int(A /\ B));
end;
notation
let T be TopSpace;
synonym CLD-Meet T for Closed_Domains_Meet T;
end;
theorem :: TDLAT_1:33
for A,B being Element of Closed_Domains_of T holds (CLD-Meet T).
(A,B) = (D-Meet T).(A,B);
theorem :: TDLAT_1:34
for T being TopSpace holds LattStr(#Closed_Domains_of T,
CLD-Union T,CLD-Meet T#) is B_Lattice;
definition
let T be TopSpace;
func Closed_Domains_Lattice T-> B_Lattice equals
:: TDLAT_1:def 8
LattStr(#Closed_Domains_of
T,Closed_Domains_Union T,Closed_Domains_Meet T #);
end;
begin
:: 5. The Lattice of Open Domains.
definition
let T be TopStruct;
func Open_Domains_of T -> Subset-Family of T equals
:: TDLAT_1:def 9
{ A where A is Subset of
T: A is open_condensed };
end;
registration
let T be TopSpace;
cluster Open_Domains_of T -> non empty;
end;
theorem :: TDLAT_1:35
for T being TopSpace holds Open_Domains_of T c= Domains_of T;
definition
let T be TopSpace;
func Open_Domains_Union T -> BinOp of Open_Domains_of T means
:: TDLAT_1:def 10
for A, B being Element of Open_Domains_of T holds it.(A,B) = Int(Cl(A \/ B));
end;
notation
let T be TopSpace;
synonym OPD-Union T for Open_Domains_Union T;
end;
theorem :: TDLAT_1:36
for A,B being Element of Open_Domains_of T holds (OPD-Union T).(
A,B) = (D-Union T).(A,B);
definition
let T be TopSpace;
func Open_Domains_Meet T -> BinOp of Open_Domains_of T means
:: TDLAT_1:def 11
for A,B being Element of Open_Domains_of T holds it.(A,B) = A /\ B;
end;
notation
let T be TopSpace;
synonym OPD-Meet T for Open_Domains_Meet T;
end;
theorem :: TDLAT_1:37
for A,B being Element of Open_Domains_of T holds (OPD-Meet T).(A
,B) = (D-Meet T).(A,B);
theorem :: TDLAT_1:38
for T being TopSpace holds LattStr(#Open_Domains_of T,OPD-Union
T,OPD-Meet T#) is B_Lattice;
definition
let T be TopSpace;
func Open_Domains_Lattice T-> B_Lattice equals
:: TDLAT_1:def 12
LattStr(#Open_Domains_of T,
Open_Domains_Union T,Open_Domains_Meet T#);
end;
begin
:: 6. Connections between Lattices of Domains.
theorem :: TDLAT_1:39
CLD-Union T = (D-Union T)||Closed_Domains_of T;
theorem :: TDLAT_1:40
CLD-Meet T = (D-Meet T)||Closed_Domains_of T;
theorem :: TDLAT_1:41
Closed_Domains_Lattice T is SubLattice of Domains_Lattice T;
theorem :: TDLAT_1:42
OPD-Union T = (D-Union T)||Open_Domains_of T;
theorem :: TDLAT_1:43
OPD-Meet T = (D-Meet T)||Open_Domains_of T;
theorem :: TDLAT_1:44
Open_Domains_Lattice T is SubLattice of Domains_Lattice T;