Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users

### Completeness of the Lattices of Domains of a Topological Space

by
Zbigniew Karno, and
Toshihiko Watanabe

MML identifier: TDLAT_2
[ Mizar article, MML identifier index ]

```environ

vocabulary PRE_TOPC, TOPS_1, BOOLE, SETFAM_1, PCOMPS_1, TARSKI, FINSET_1,
FINSEQ_1, RELAT_1, FUNCT_1, TDLAT_1, LATTICES, SUBSET_1, LATTICE3,
BHSP_3, TDLAT_2;
notation TARSKI, XBOOLE_0, SUBSET_1, XREAL_0, SETFAM_1, STRUCT_0, FUNCT_1,
FINSET_1, FINSEQ_1, NAT_1, PRE_TOPC, TOPS_1, TOPS_2, PCOMPS_1, BINOP_1,
LATTICES, LATTICE3, TDLAT_1;
constructors FINSEQ_1, NAT_1, TOPS_1, TOPS_2, PCOMPS_1, LATTICE3, TDLAT_1,
MEMBERED, XBOOLE_0;
clusters SUBSET_1, PRE_TOPC, STRUCT_0, TDLAT_1, TOPS_1, ARYTM_3, MEMBERED,
ZFMISC_1, XBOOLE_0;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;

begin
:: 1. Preliminary Theorems about Subsets of a Toplogical Space.
reserve T for non empty TopSpace;

theorem :: TDLAT_2:1
for A being Subset of T holds
Int Cl Int A c= Int Cl A & Int Cl Int A c= Cl Int A;

theorem :: TDLAT_2:2
for A being Subset of T holds
Cl Int A c= Cl Int Cl A & Int Cl A c= Cl Int Cl A;

theorem :: TDLAT_2:3
for A being Subset of T, B being Subset of T st B is closed
holds Cl(Int(A /\ B)) = A implies A c= B;

theorem :: TDLAT_2:4
for A being Subset of T, B being Subset of T st A is open holds
Int(Cl(A \/ B)) = B implies A c= B;

theorem :: TDLAT_2:5
for A being Subset of T holds
A c= Cl Int A implies A \/ Int Cl A c= Cl Int(A \/ Int Cl A);

theorem :: TDLAT_2:6
for A being Subset of T holds
Int Cl A c= A implies Int Cl(A /\ Cl Int A) c= A /\ Cl Int A;

begin
:: 2. The Closure and the Interior Operations for Families of Subsets of
::                                                    a Topological Space.
reserve T for non empty TopSpace;

::(for the definition of clf see PCOMPS_1:def 3)
definition let T; let F be Subset-Family of T;
redefine func clf F;
synonym Cl F;
end;

theorem :: TDLAT_2:7
for F being Subset-Family of T holds Cl F =
{A where A is Subset of T :
ex B being Subset of T st A = Cl B & B in F};

theorem :: TDLAT_2:8
for F being Subset-Family of T holds Cl F = Cl Cl F;

theorem :: TDLAT_2:9
for F being Subset-Family of T holds F = {} iff Cl F = {};

theorem :: TDLAT_2:10
for F,G being Subset-Family of T holds Cl(F /\ G) c= (Cl F) /\ (Cl G);

theorem :: TDLAT_2:11
for F,G being Subset-Family of T holds (Cl F) \ (Cl G) c= Cl(F \ G);

theorem :: TDLAT_2:12
for F being Subset-Family of T, A being Subset of T holds
A in F implies meet(Cl F) c= Cl A & Cl A c= union(Cl F);

::for F being Subset-Family of T holds union F c= union(Cl F);
::(see PCOMPS_1:22)
theorem :: TDLAT_2:13
for F being Subset-Family of T holds meet F c= meet(Cl F);

theorem :: TDLAT_2:14
for F being Subset-Family of T holds Cl(meet F) c= meet(Cl F);

theorem :: TDLAT_2:15
for F being Subset-Family of T holds union(Cl F) c= Cl(union F);

definition let T; let F be Subset-Family of T;
func Int F -> Subset-Family of T means
:: TDLAT_2:def 1
for A being Subset of T holds
A in it iff ex B being Subset of T st A = Int B & B in F;
end;

::Properties of the Interior Operation Int.
theorem :: TDLAT_2:16
for F being Subset-Family of T holds Int F =
{A where A is Subset of T :
ex B being Subset of T st A = Int B & B in F};

theorem :: TDLAT_2:17
for F being Subset-Family of T holds Int F = Int Int F;

theorem :: TDLAT_2:18
for F being Subset-Family of T holds Int F is open;

theorem :: TDLAT_2:19
for F being Subset-Family of T holds F = {} iff Int F = {};

theorem :: TDLAT_2:20
for A being Subset of T, F being Subset-Family of T
st F = { A } holds
Int F = { Int A };

theorem :: TDLAT_2:21
for F,G being Subset-Family of T holds F c= G implies Int F c= Int G;

theorem :: TDLAT_2:22
for F,G being Subset-Family of T holds Int(F \/ G) = (Int F) \/ (Int G);

theorem :: TDLAT_2:23
for F,G being Subset-Family of T holds Int(F /\ G) c= (Int F) /\ (Int G);

theorem :: TDLAT_2:24
for F,G being Subset-Family of T holds (Int F) \ (Int G) c= Int(F \ G);

theorem :: TDLAT_2:25
for F being Subset-Family of T, A being Subset of T holds
A in F implies Int A c= union(Int F) & meet(Int F) c= Int A;

theorem :: TDLAT_2:26
for F being Subset-Family of T holds union(Int F) c= union F;

theorem :: TDLAT_2:27
for F being Subset-Family of T holds meet(Int F) c= meet F;

theorem :: TDLAT_2:28
for F being Subset-Family of T holds union(Int F) c= Int(union F);

theorem :: TDLAT_2:29
for F being Subset-Family of T holds Int(meet F) c= meet(Int F);

theorem :: TDLAT_2:30
for F being Subset-Family of T holds
F is finite implies Int(meet F) = meet(Int F);

::Connections between the Operations Int and Cl.
reserve F for Subset-Family of T;

theorem :: TDLAT_2:31
Cl Int F =
{A where A is Subset of T :
ex B being Subset of T st A = Cl Int B & B in F};

theorem :: TDLAT_2:32
Int Cl F =
{A where A is Subset of T :
ex B being Subset of T st A = Int Cl B & B in F};

theorem :: TDLAT_2:33
Cl Int Cl F = {A where A is Subset of T :
ex B being Subset of T st A = Cl Int Cl B & B in F};

theorem :: TDLAT_2:34
Int Cl Int F = {A where A is Subset of T :
ex B being Subset of T st A = Int Cl Int B & B in F};

theorem :: TDLAT_2:35
Cl Int Cl Int F = Cl Int F;

theorem :: TDLAT_2:36
Int Cl Int Cl F = Int Cl F;

theorem :: TDLAT_2:37
union(Int Cl F) c= union(Cl Int Cl F);

theorem :: TDLAT_2:38
meet(Int Cl F) c= meet(Cl Int Cl F);

theorem :: TDLAT_2:39
union(Cl Int F) c= union(Cl Int Cl F);

theorem :: TDLAT_2:40
meet(Cl Int F) c= meet(Cl Int Cl F);

theorem :: TDLAT_2:41
union(Int Cl Int F) c= union(Int Cl F);

theorem :: TDLAT_2:42
meet(Int Cl Int F) c= meet(Int Cl F);

theorem :: TDLAT_2:43
union(Int Cl Int F) c= union(Cl Int F);

theorem :: TDLAT_2:44
meet(Int Cl Int F) c= meet(Cl Int F);

theorem :: TDLAT_2:45
union(Cl Int Cl F) c= union(Cl F);

theorem :: TDLAT_2:46
meet(Cl Int Cl F) c= meet(Cl F);

theorem :: TDLAT_2:47
union(Int F) c= union(Int Cl Int F);

theorem :: TDLAT_2:48
meet(Int F) c= meet(Int Cl Int F);

theorem :: TDLAT_2:49
union(Cl Int F) c= Cl Int(union F);

theorem :: TDLAT_2:50
Cl Int(meet F) c= meet(Cl Int F);

theorem :: TDLAT_2:51
union(Int Cl F) c= Int Cl(union F);

theorem :: TDLAT_2:52
Int Cl(meet F) c= meet(Int Cl F);

theorem :: TDLAT_2:53
union(Cl Int Cl F) c= Cl Int Cl(union F);

theorem :: TDLAT_2:54
Cl Int Cl(meet F) c= meet(Cl Int Cl F);

theorem :: TDLAT_2:55
union(Int Cl Int F) c= Int Cl Int(union F);

theorem :: TDLAT_2:56
Int Cl Int(meet F) c= meet(Int Cl Int F);

theorem :: TDLAT_2:57
for F being Subset-Family of T holds
(for A being Subset of T st A in
F holds A c= Cl Int A) implies
union F c= Cl Int(union F) & Cl(union F) = Cl Int Cl(union F);

theorem :: TDLAT_2:58
for F being Subset-Family of T holds
(for A being Subset of T st A in
F holds Int Cl A c= A) implies
Int Cl(meet F) c= meet F & Int Cl Int(meet F) = Int(meet F);

begin
:: 3. Selected Properties of Domains of a Topological Space.
reserve T for non empty TopSpace;

theorem :: TDLAT_2:59
for A, B being Subset of T st B is condensed holds
Int(Cl(A \/ B)) \/ (A \/ B) = B iff A c= B;

theorem :: TDLAT_2:60
for A, B being Subset of T st A is condensed holds
Cl(Int(A /\ B)) /\ (A /\ B) = A iff A c= B;

theorem :: TDLAT_2:61
for A, B being Subset of T st A is closed_condensed & B is closed_condensed
holds Int A c= Int B iff A c= B;

theorem :: TDLAT_2:62
for A, B being Subset of T st A is open_condensed & B is open_condensed
holds
Cl A c= Cl B iff A c= B;

theorem :: TDLAT_2:63
for A, B being Subset of T st A is closed_condensed holds
A c= B implies Cl(Int(A /\ B)) = A;

theorem :: TDLAT_2:64
for A, B being Subset of T st B is open_condensed holds
A c= B implies Int(Cl(A \/ B)) = B;

definition let T;
let IT be Subset-Family of T;
attr IT is domains-family means
:: TDLAT_2:def 2
for A being Subset of T holds A in IT implies A is condensed;
end;

theorem :: TDLAT_2:65
for F being Subset-Family of T holds
F c= Domains_of T iff F is domains-family;

theorem :: TDLAT_2:66
for F being Subset-Family of T holds F is domains-family implies
union F c= Cl Int(union F) & Cl(union F) = Cl Int Cl(union F);

theorem :: TDLAT_2:67
for F being Subset-Family of T holds F is domains-family implies
Int Cl(meet F) c= meet F & Int Cl Int(meet F) = Int(meet F);

theorem :: TDLAT_2:68
for F being Subset-Family of T holds
F is domains-family implies (union F) \/ (Int Cl(union F)) is condensed;

theorem :: TDLAT_2:69
for F being Subset-Family of T holds
(for B being Subset of T st B in F
holds B c= (union F) \/ (Int Cl(union F)))
& (for A being Subset of T st A is condensed holds
(for B being Subset of T st B in F holds B c= A) implies
(union F) \/ (Int Cl(union F)) c= A);

theorem :: TDLAT_2:70
for F being Subset-Family of T holds
F is domains-family implies (meet F) /\ (Cl Int(meet F)) is condensed;

theorem :: TDLAT_2:71
for F being Subset-Family of T holds
(for B being Subset of T st B in F
holds (meet F) /\ (Cl Int(meet F)) c= B)
& (F = {} or for A being Subset of T st A is condensed holds
(for B being Subset of T st B in F holds A c= B) implies
A c= (meet F) /\ (Cl Int(meet F)));

definition let T;
let IT be Subset-Family of T;
attr IT is closed-domains-family means
:: TDLAT_2:def 3
for A being Subset of T holds A in IT implies A is closed_condensed;
end;

theorem :: TDLAT_2:72
for F being Subset-Family of T holds
F c= Closed_Domains_of T iff F is closed-domains-family;

theorem :: TDLAT_2:73
for F being Subset-Family of T holds
F is closed-domains-family implies F is domains-family;

theorem :: TDLAT_2:74
for F being Subset-Family of T holds
F is closed-domains-family implies F is closed;

theorem :: TDLAT_2:75
for F being Subset-Family of T holds
F is domains-family implies Cl F is closed-domains-family;

theorem :: TDLAT_2:76
for F being Subset-Family of T holds
F is closed-domains-family implies
Cl(union F) is closed_condensed & Cl Int(meet F) is closed_condensed;

theorem :: TDLAT_2:77
for F being Subset-Family of T holds
(for B being Subset of T st B in F holds B c= Cl(union F))
& (for A being Subset of T st A is closed_condensed holds
(for B being Subset of T st B in F holds B c= A)
implies Cl(union F) c= A);

theorem :: TDLAT_2:78
for F being Subset-Family of T holds
(F is closed implies
for B being Subset of T st B in F holds Cl Int(meet F) c= B)
& (F = {} or for A being Subset of T st A is closed_condensed
holds
(for B being Subset of T st B in F holds A c= B) implies
A c= Cl Int(meet F));

definition let T;
let IT be Subset-Family of T;
attr IT is open-domains-family means
:: TDLAT_2:def 4
for A being Subset of T holds A in IT implies A is open_condensed;
end;

theorem :: TDLAT_2:79
for F being Subset-Family of T holds
F c= Open_Domains_of T iff F is open-domains-family;

theorem :: TDLAT_2:80
for F being Subset-Family of T holds
F is open-domains-family implies F is domains-family;

theorem :: TDLAT_2:81
for F being Subset-Family of T holds
F is open-domains-family implies F is open;

theorem :: TDLAT_2:82
for F being Subset-Family of T holds
F is domains-family implies Int F is open-domains-family;

theorem :: TDLAT_2:83
for F being Subset-Family of T holds
F is open-domains-family implies
Int(meet F) is open_condensed & Int Cl(union F) is open_condensed;

theorem :: TDLAT_2:84
for F being Subset-Family of T holds
(F is open implies
for B being Subset of T st B in F holds B c= Int Cl(union F))
& (for A being Subset of T st A is open_condensed holds
(for B being Subset of T st B in F holds B c= A)
implies Int Cl(union F) c= A);

theorem :: TDLAT_2:85
for F being Subset-Family of T holds
(for B being Subset of T st B in F holds Int(meet F) c= B)
& (F = {} or for A being Subset of T st A is open_condensed
holds
(for B being Subset of T st B in F holds A c= B)
implies A c= Int(meet F));

begin
:: 4. Completeness of the Lattice of Domains.

reserve T for non empty TopSpace;

theorem :: TDLAT_2:86
the carrier of Domains_Lattice T = Domains_of T;

theorem :: TDLAT_2:87
for a, b being Element of Domains_Lattice T
for A, B being Element of Domains_of T st a = A & b = B holds
a "\/" b = Int(Cl(A \/ B)) \/ (A \/ B) & a "/\" b = Cl(Int(A /\ B)) /\ (A /\
B);

theorem :: TDLAT_2:88
Bottom (Domains_Lattice T) = {}T & Top (Domains_Lattice T) = [#]T;

theorem :: TDLAT_2:89
for a, b being Element of Domains_Lattice T
for A, B being Element of Domains_of T st a = A & b = B holds
a [= b iff A c= B;

theorem :: TDLAT_2:90
for X being Subset of Domains_Lattice T
ex a being Element of Domains_Lattice T
st X is_less_than a &
for b being Element of Domains_Lattice T
st X is_less_than b holds a [= b;

theorem :: TDLAT_2:91
Domains_Lattice T is complete;

theorem :: TDLAT_2:92
for F being Subset-Family of T st F is domains-family
for X being Subset of Domains_Lattice T st X = F holds
"\/"(X,Domains_Lattice T) = (union F) \/ (Int Cl(union F));

theorem :: TDLAT_2:93
for F being Subset-Family of T st F is domains-family
for X being Subset of Domains_Lattice T st X = F holds
(X <> {} implies "/\"(X,Domains_Lattice T) = (meet F) /\ (Cl Int(meet F))) &
(X = {} implies "/\"(X,Domains_Lattice T) = [#]T);

begin
:: 5. Completeness of the Lattices of Closed Domains and Open Domains.
reserve T for non empty TopSpace;

::The Lattice of Closed Domains.
theorem :: TDLAT_2:94
the carrier of Closed_Domains_Lattice T = Closed_Domains_of T;

theorem :: TDLAT_2:95
for a, b being Element of Closed_Domains_Lattice T
for A, B being Element of Closed_Domains_of T st a = A & b = B holds
a "\/" b = A \/ B & a "/\" b = Cl(Int(A /\ B));

theorem :: TDLAT_2:96
Bottom (Closed_Domains_Lattice T) = {}T & Top (Closed_Domains_Lattice T) =
[#]
T;

theorem :: TDLAT_2:97
for a, b being Element of Closed_Domains_Lattice T
for A, B being Element of Closed_Domains_of T st a = A & b = B holds
a [= b iff A c= B;

theorem :: TDLAT_2:98
for X being Subset of Closed_Domains_Lattice T
ex a being Element of Closed_Domains_Lattice T st
X is_less_than a &
for b being Element of Closed_Domains_Lattice T st
X is_less_than b holds a [= b;

theorem :: TDLAT_2:99
Closed_Domains_Lattice T is complete;

theorem :: TDLAT_2:100
for F being Subset-Family of T st F is closed-domains-family
for X being Subset of Closed_Domains_Lattice T st X = F holds
"\/"(X,Closed_Domains_Lattice T) = Cl(union F);

theorem :: TDLAT_2:101
for F being Subset-Family of T st F is closed-domains-family
for X being Subset of Closed_Domains_Lattice T st X = F holds
(X <> {} implies "/\"(X,Closed_Domains_Lattice T) = Cl(Int(meet F))) &
(X = {} implies "/\"(X,Closed_Domains_Lattice T) = [#]T);

theorem :: TDLAT_2:102
for F being Subset-Family of T st F is closed-domains-family
for X being Subset of Domains_Lattice T st X = F holds
(X <> {} implies "/\"(X,Domains_Lattice T) = Cl(Int(meet F))) &
(X = {} implies "/\"(X,Domains_Lattice T) = [#]T);

::The Lattice of Open Domains.
theorem :: TDLAT_2:103
the carrier of Open_Domains_Lattice T = Open_Domains_of T;

theorem :: TDLAT_2:104
for a, b being Element of Open_Domains_Lattice T
for A, B being Element of Open_Domains_of T st a = A & b = B holds
a "\/" b = Int(Cl(A \/ B)) & a "/\" b = A /\ B;

theorem :: TDLAT_2:105
Bottom (Open_Domains_Lattice T) = {}T & Top (Open_Domains_Lattice T) = [#]T;

theorem :: TDLAT_2:106
for a, b being Element of Open_Domains_Lattice T
for A, B being Element of Open_Domains_of T st a = A & b = B holds
a [= b iff A c= B;

theorem :: TDLAT_2:107
for X being Subset of Open_Domains_Lattice T
ex a being Element of Open_Domains_Lattice T st
X is_less_than a &
for b being Element of Open_Domains_Lattice T st
X is_less_than b holds a [= b;

theorem :: TDLAT_2:108
Open_Domains_Lattice T is complete;

theorem :: TDLAT_2:109
for F being Subset-Family of T st F is open-domains-family
for X being Subset of Open_Domains_Lattice T st X = F holds
"\/"(X,Open_Domains_Lattice T) = Int Cl(union F);

theorem :: TDLAT_2:110
for F being Subset-Family of T st F is open-domains-family
for X being Subset of Open_Domains_Lattice T st X = F holds
(X <> {} implies "/\"(X,Open_Domains_Lattice T) = Int(meet F)) &
(X = {} implies "/\"(X,Open_Domains_Lattice T) = [#]T);

theorem :: TDLAT_2:111
for F being Subset-Family of T st F is open-domains-family
for X being Subset of Domains_Lattice T st X = F holds
"\/"(X,Domains_Lattice T) = Int Cl(union F);

```