:: 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;
definitions TARSKI, LATTICES, NAT_LAT;
equalities LATTICES, XBOOLE_0, BINOP_1, REALSET1, SUBSET_1, STRUCT_0;
expansions TARSKI, XBOOLE_0;
theorems TOPS_1, PRE_TOPC, LATTICE2, BINOP_1, FUNCT_2, SUBSET_1, MCART_1,
FUNCT_1, XBOOLE_1, XTUPLE_0, ZFMISC_1;
schemes FUNCT_2, BINOP_2;
begin
:: 1. Preliminary Theorems on Subsets of Topological Spaces.
reserve T for 1-sorted;
theorem Th1:
for A,B being Subset of T holds A \/ B = [#] T iff A` c= B
proof
let A,B be Subset of T;
hereby
assume A \/ B = [#] T;
then [#] T \ A = B \ A by XBOOLE_1:40;
hence A` c= B by XBOOLE_1:36;
end;
assume A` c= B;
then A \/ A` c= A \/ B by XBOOLE_1:9;
then [#] T c= A \/ B by PRE_TOPC:2;
hence A \/ B = [#] T;
end;
theorem Th2:
for A,B being Subset of T holds A misses B iff B c= A` by SUBSET_1:23;
reserve T for TopSpace;
theorem Th3:
for A being Subset of T holds Cl Int Cl A c= Cl A
proof
let A be Subset of T;
Cl Int Cl A c= Cl Cl A by PRE_TOPC:19,TOPS_1:16;
hence thesis;
end;
theorem Th4:
for A being Subset of T holds Int A c= Int Cl Int A
proof
let A be Subset of T;
Int Int A c= Int Cl Int A by PRE_TOPC:18,TOPS_1:19;
hence thesis;
end;
theorem Th5:
for A being Subset of T holds Int Cl A = Int Cl Int Cl A
proof
let A be Subset of T;
A1: Int Int Cl A c= Int Cl Int Cl A by PRE_TOPC:18,TOPS_1:19;
Int Cl Int Cl A c= Int Cl A by Th3,TOPS_1:19;
hence thesis by A1;
end;
theorem Th6:
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)
proof
let A,B be Subset of T;
A1: (A \/ B) \/ (A \/ B)` c= (A \/ B) \/ Cl (A \/ B)` by PRE_TOPC:18,XBOOLE_1:9
;
(A \/ B) \/ (A \/ B)` = [#] T by PRE_TOPC:2;
then
A2: (A \/ B) \/ Cl(A \/ B)` = [#] T by A1;
then A \/ (B \/ Cl(A \/ B)`) = [#] T by XBOOLE_1:4;
then A` c= B \/ Cl(A \/ B)` by Th1;
then
A3: Cl A` c= Cl(B \/ Cl(A \/ B)`) by PRE_TOPC:19;
B \/ (A \/ Cl(A \/ B)`) = [#] T by A2,XBOOLE_1:4;
then B` c= A \/ Cl(A \/ B)` by Th1;
then
A4: Cl B` c= Cl(A \/ Cl(A \/ B)`) by PRE_TOPC:19;
assume
A5: A is closed or B is closed;
A6: now
per cases by A5;
suppose
A is closed;
then (Cl B`)`` c= A \/ Cl(B \/ A)` by A4,PRE_TOPC:22;
then (Cl B`)` \/ (A \/ Cl(B \/ A)`) = [#] T by Th1;
then Int B \/ (A \/ Cl(B \/ A)`) = [#] T by TOPS_1:def 1;
then A \/ (Int B \/ Cl(B \/ A)`) = [#] T by XBOOLE_1:4;
then A` c= Int B \/ Cl(B \/ A)` by Th1;
then Cl A` c= Cl(Int B \/ Cl(B \/ A)`) by PRE_TOPC:19;
then Cl A` c= Cl Int B \/ Cl Cl(B \/ A)` by PRE_TOPC:20;
then Cl A` \/ (Cl A`)` c= (Cl Int B \/ Cl(B \/ A)`) \/ (Cl A`)` by
XBOOLE_1:9;
then [#] T c= (Cl Int B \/ Cl(B \/ A)`) \/ ((Cl A`)`) by PRE_TOPC:2;
then [#] T c= (Cl(B \/ A)` \/ Cl Int B) \/ Int A by TOPS_1:def 1;
then [#] T c= Cl(B \/ A)` \/ (Cl Int B \/ Int A) by XBOOLE_1:4;
then [#] T = Cl(B \/ A)` \/ (Cl Int B \/ Int A);
then (Cl(B \/ A)`)` c= Cl Int B \/ Int A by Th1;
then Int(B \/ A) c= Cl Int B \/ Int A by TOPS_1:def 1;
then Cl Int(B \/ A) c= Cl(Cl Int B \/ Int A) by PRE_TOPC:19;
then Cl Int(B \/ A) c= Cl Cl Int B \/ Cl Int A by PRE_TOPC:20;
hence Cl Int(A \/ B) c= Cl Int A \/ Cl Int B;
end;
suppose
B is closed;
then (Cl A`)`` c= B \/ Cl(A \/ B)` by A3,PRE_TOPC:22;
then ((Cl A`)`) \/ (B \/ Cl(A \/ B)`) = [#] T by Th1;
then Int A \/ (B \/ Cl(A \/ B)`) = [#] T by TOPS_1:def 1;
then B \/ (Int A \/ Cl(A \/ B)`) = [#] T by XBOOLE_1:4;
then B` c= Int A \/ Cl(A \/ B)` by Th1;
then Cl B` c= Cl(Int A \/ Cl(A \/ B)`) by PRE_TOPC:19;
then Cl B` c= Cl Int A \/ Cl Cl(A \/ B)` by PRE_TOPC:20;
then Cl B` \/ (Cl B`)` c= (Cl Int A \/ Cl(A \/ B)`) \/ (Cl B`)` by
XBOOLE_1:9;
then [#] T c= (Cl Int A \/ Cl(A \/ B)`) \/ (Cl B`)` by PRE_TOPC:2;
then [#] T c= (Cl(A \/ B)` \/ Cl Int A) \/ Int B by TOPS_1:def 1;
then [#] T c= Cl(A \/ B)` \/ (Cl Int A \/ Int B) by XBOOLE_1:4;
then [#] T = Cl(A \/ B)` \/ (Cl Int A \/ Int B);
then (Cl(A \/ B)`)` c= Cl Int A \/ Int B by Th1;
then Int(A \/ B) c= Cl Int A \/ Int B by TOPS_1:def 1;
then Cl Int(A \/ B) c= Cl(Cl Int A \/ Int B) by PRE_TOPC:19;
then Cl Int(A \/ B) c= Cl Cl Int A \/ Cl Int B by PRE_TOPC:20;
hence Cl Int(A \/ B) c= Cl Int A \/ Cl Int B;
end;
end;
Int B c= Int(A \/ B) by TOPS_1:19,XBOOLE_1:7;
then
A7: Cl Int B c= Cl Int(A \/ B) by PRE_TOPC:19;
Int A c= Int(A \/ B) by TOPS_1:19,XBOOLE_1:7;
then Cl Int A c= Cl Int(A \/ B) by PRE_TOPC:19;
then Cl Int A \/ Cl Int B c= Cl Int(A \/ B) by A7,XBOOLE_1:8;
hence thesis by A6;
end;
theorem Th7:
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)
proof
let A,B be Subset of T;
A1: (Int A`) misses (Int A`)` by XBOOLE_1:79;
A2: (Int B`) misses (Int B`)` by XBOOLE_1:79;
(A /\ B) misses (A /\ B)` by XBOOLE_1:79;
then
A3: {} T = (A /\ B) /\ (A /\ B)`;
A4: (A /\ B) /\ Int (A /\ B)` c= (A /\ B) /\ (A /\ B)` by TOPS_1:16,XBOOLE_1:26
;
then A /\ (B /\ Int(A /\ B)`) = {} T by A3,XBOOLE_1:16;
then A misses (B /\ Int(A /\ B)`);
then B /\ Int(A /\ B)` c= A` by Th2;
then
A5: Int(B /\ Int(A /\ B)`) c= Int A` by TOPS_1:19;
B /\ (A /\ Int(A /\ B)`) = {} T by A3,A4,XBOOLE_1:16;
then B misses (A /\ Int(A /\ B)`);
then A /\ Int(A /\ B)` c= B` by Th2;
then
A6: Int(A /\ Int(A /\ B)`) c= Int B` by TOPS_1:19;
assume
A7: A is open or B is open;
A8: now
per cases by A7;
suppose
A is open;
then A /\ Int(A /\ B)` c= (Int B`)`` by A6,TOPS_1:23;
then (Int B`)` misses (A /\ Int(A /\ B)`) by Th2;
then (Int B`)` /\ (A /\ Int(A /\ B)`) = {};
then (Cl B``)`` /\ (A /\ Int(A /\ B)`) = {} by TOPS_1:def 1;
then A /\ (Cl B /\ Int(A /\ B)`) = {} by XBOOLE_1:16;
then A misses (Cl B /\ Int(A /\ B)`);
then Cl B /\ Int(A /\ B)` c= A` by Th2;
then Int(Cl B /\ Int(A /\ B)`) c= Int A` by TOPS_1:19;
then Int Cl B /\ Int Int(A /\ B)` c= Int A` by TOPS_1:17;
then
(Int Cl B /\ Int(A /\ B)`) /\ (Int A`)` c= (Int A`) /\ (Int A`)` by
XBOOLE_1:26;
then (Int Cl B /\ Int(A /\ B)`) /\ (Int A`)` c= {} T by A1;
then (Int Cl B /\ Int(A /\ B)`) /\ (Cl A``)`` c= {} T by TOPS_1:def 1;
then {} T = (Int(A /\ B)`) /\ (Int Cl B /\ Cl A) by XBOOLE_1:16;
then (Int(A /\ B)`) misses (Int Cl B /\ Cl A);
then Int Cl B /\ Cl A c= (Int(A /\ B)`)` by Th2;
then Int Cl B /\ Cl A c= (Cl (A /\ B)``)`` by TOPS_1:def 1;
then Int(Int Cl B /\ Cl A) c= Int Cl(B /\ A) by TOPS_1:19;
then Int Int Cl B /\ Int Cl A c= Int Cl(B /\ A) by TOPS_1:17;
hence Int Cl A /\ Int Cl B c= Int Cl(A /\ B);
end;
suppose
B is open;
then B /\ Int(A /\ B)` c= (Int A`)`` by A5,TOPS_1:23;
then (Int A`)` misses (B /\ Int(A /\ B)`) by Th2;
then (Int A`)` /\ (B /\ Int(A /\ B)`) = {} T;
then (Cl A``)`` /\ (B /\ Int(A /\ B)`) = {} T by TOPS_1:def 1;
then B /\ (Cl A /\ Int(A /\ B)`) = {} T by XBOOLE_1:16;
then B misses (Cl A /\ Int(A /\ B)`);
then Cl A /\ Int(A /\ B)` c= B` by Th2;
then Int(Cl A /\ Int(A /\ B)`) c= Int B` by TOPS_1:19;
then Int Cl A /\ Int Int(A /\ B)` c= Int B` by TOPS_1:17;
then
(Int Cl A /\ Int(A /\ B)`) /\ (Int B`)` c= (Int B`) /\ (Int B`)` by
XBOOLE_1:26;
then (Int Cl A /\ Int(A /\ B)`) /\ (Int B`)` c= {} T by A2;
then (Int Cl A /\ Int(A /\ B)`) /\ ((Cl B``)``) c= {} T by TOPS_1:def 1;
then {} T = (Int(A /\ B)`) /\ (Int Cl A /\ Cl B) by XBOOLE_1:16;
then (Int(A /\ B)`) misses (Int Cl A /\ Cl B);
then Int Cl A /\ Cl B c= (Int(A /\ B)`)` by Th2;
then Int Cl A /\ Cl B c= (Cl (A /\ B)``)`` by TOPS_1:def 1;
then Int(Int Cl A /\ Cl B) c= Int Cl(A /\ B) by TOPS_1:19;
then Int Int Cl A /\ Int Cl B c= Int Cl(A /\ B) by TOPS_1:17;
hence Int Cl A /\ Int Cl B c= Int Cl(A /\ B);
end;
end;
Cl(A /\ B) c= Cl B by PRE_TOPC:19,XBOOLE_1:17;
then
A9: Int Cl(A /\ B) c= Int Cl B by TOPS_1:19;
Cl(A /\ B) c= Cl A by PRE_TOPC:19,XBOOLE_1:17;
then Int Cl(A /\ B) c= Int Cl A by TOPS_1:19;
then Int Cl(A /\ B) c= Int Cl A /\ Int Cl B by A9,XBOOLE_1:19;
hence thesis by A8;
end;
theorem Th8:
for A being Subset of T holds Int(A /\ Cl A`) = {} T
proof
let A be Subset of T;
A1: Int A misses (Int A)` by XBOOLE_1:79;
thus Int(A /\ Cl A`) = Int(A /\ ((Cl A`)`)`)
.= Int(A /\ (Int A)`) by TOPS_1:def 1
.= Int Int A /\ Int((Int A)`) by TOPS_1:17
.= Int(Int A /\ (Int A)`) by TOPS_1:17
.= Int({} T) by A1
.= {} T;
end;
theorem Th9:
for A being Subset of T holds Cl(A \/ Int A`) = [#] T
proof
let A be Subset of T;
thus Cl(A \/ Int A`) = Cl(A \/ (Cl(A``))`) by TOPS_1:def 1
.= Cl Cl A \/ Cl (Cl A)` by PRE_TOPC:20
.= Cl(Cl A \/ (Cl A)`) by PRE_TOPC:20
.= Cl([#] T) by PRE_TOPC:2
.= [#] T by TOPS_1:2;
end;
theorem Th10:
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)
proof
let A,B be Subset of T;
Cl B c= Cl (A \/ B) by PRE_TOPC:19,XBOOLE_1:7;
then
A1: Int Cl B c= Int Cl(A \/ B) by TOPS_1:19;
A \/ B c= A \/ (Int(Cl B) \/ B) by XBOOLE_1:7,9;
then Cl(A \/ B) c= Cl(A \/ (Int(Cl B) \/ B)) by PRE_TOPC:19;
then
A2: Int Cl(A \/ B) c= Int(Cl(A \/ (Int(Cl B) \/ B))) by TOPS_1:19;
Int(Cl(A \/ (Int(Cl B) \/ B))) c= Int(Cl(A \/ (Int(Cl B) \/ B))) \/ Int(
Cl B) by XBOOLE_1:7;
then
A3: Int Cl(A \/ B) c= Int(Cl(A \/ (Int(Cl B) \/ B))) \/ Int(Cl B) by A2;
Int(Cl(A \/ (Int(Cl B) \/ B))) = Int(Cl((A \/ Int(Cl B)) \/ B)) by XBOOLE_1:4
.= Int(Cl(A \/ Int(Cl B)) \/ Cl B) by PRE_TOPC:20
.= Int(Cl A \/ Cl Int Cl B \/ Cl B) by PRE_TOPC:20
.= Int(Cl A \/ (Cl Int Cl B \/ Cl B)) by XBOOLE_1:4
.= Int(Cl A \/ Cl B) by Th3,XBOOLE_1:12
.= Int Cl(A \/ B) by PRE_TOPC:20;
then Int(Cl(A \/ (Int(Cl B) \/ B))) \/ Int(Cl B) c= Int Cl(A \/ B) by A1,
XBOOLE_1:8;
then
A4: Int(Cl(A \/ (Int(Cl B) \/ B))) \/ Int(Cl B) = Int Cl(A \/ B) by A3;
A \/ (Int(Cl B) \/ B) = Int(Cl B) \/ (A \/ B) by XBOOLE_1:4;
hence thesis by A4,XBOOLE_1:4;
end;
theorem
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) by Th10;
theorem Th12:
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)
proof
let A,B be Subset of T;
Int (A /\ B) c= Int B by TOPS_1:19,XBOOLE_1:17;
then
A1: Cl Int(A /\ B) c= Cl(Int B) by PRE_TOPC:19;
Cl(Int(A /\ (Cl(Int B) /\ B))) = Cl(Int((A /\ Cl(Int B)) /\ B)) by
XBOOLE_1:16
.= Cl(Int(A /\ Cl(Int B)) /\ Int B) by TOPS_1:17
.= Cl(Int A /\ Int Cl Int B /\ Int B) by TOPS_1:17
.= Cl(Int A /\ (Int Cl Int B /\ Int B)) by XBOOLE_1:16
.= Cl(Int A /\ Int B) by Th4,XBOOLE_1:28
.= Cl Int(A /\ B) by TOPS_1:17;
then
A2: Cl Int(A /\ B) c= Cl(Int(A /\ (Cl(Int B) /\ B))) /\ Cl(Int B) by A1,
XBOOLE_1:19;
A /\ (Cl(Int B) /\ B) c= A /\ B by XBOOLE_1:17,26;
then Int(A /\ (Cl(Int B) /\ B)) c= Int(A /\ B) by TOPS_1:19;
then
A3: Cl(Int(A /\ (Cl(Int B) /\ B))) c= Cl Int(A /\ B) by PRE_TOPC:19;
Cl(Int(A /\ (Cl(Int B) /\ B))) /\ Cl(Int B) c= Cl(Int(A /\ (Cl(Int B) /\
B))) by XBOOLE_1:17;
then Cl(Int(A /\ (Cl(Int B) /\ B))) /\ Cl(Int B) c= Cl Int(A /\ B) by A3;
then
A4: Cl(Int(A /\ (Cl(Int B) /\ B))) /\ Cl(Int B) = Cl Int(A /\ B) by A2;
A /\ (Cl(Int B) /\ B) = Cl(Int B) /\ (A /\ B) by XBOOLE_1:16;
hence thesis by A4,XBOOLE_1:16;
end;
theorem
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) by Th12;
begin
:: 2. Properties of Domains_of of Topological Spaces.
theorem Th14:
{}T is condensed
proof
Int {} T c= {} T;
then
A1: Int Cl {} T c= {} T by PRE_TOPC:22;
{} T c= Cl Int {} T;
hence thesis by A1,TOPS_1:def 6;
end;
theorem Th15:
[#] T is condensed
proof
[#] T c= Cl [#] T by PRE_TOPC:18;
then
A1: [#] T c= Cl Int [#] T by TOPS_1:15;
Int Cl [#] T c= [#] T;
hence thesis by A1,TOPS_1:def 6;
end;
theorem Th16:
for A being Subset of T st A is condensed holds A` is condensed
proof
let X be Subset of T;
assume
A1: X is condensed;
then X c= Cl Int X by TOPS_1:def 6;
then (Cl(Int X)``)` c= X` by SUBSET_1:12;
then Int(Int X)` c= X` by TOPS_1:def 1;
then
A2: Int(Cl X`)`` c= X` by TOPS_1:def 1;
Int Cl X c= X by A1,TOPS_1:def 6;
then (Cl((Cl X)`))` c= X by TOPS_1:def 1;
then X` c= Cl(Cl(X``))` by SUBSET_1:12;
then X` c= Cl(Int X`) by TOPS_1:def 1;
hence thesis by A2,TOPS_1:def 6;
end;
theorem Th17:
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
proof
let A,B be Subset of T;
assume
A1: A is condensed;
assume
A2: B is condensed;
then
A3: B c= Cl(Int(B)) by TOPS_1:def 6;
A4: A c= Cl(Int(A)) by A1,TOPS_1:def 6;
thus Int(Cl(A \/ B)) \/ (A \/ B) is condensed
proof
set X = Int(Cl(A \/ B)) \/ (A \/ B);
Cl(Int(A) \/ Int(B)) c= Cl(Int(A \/ B)) by PRE_TOPC:19,TOPS_1:20;
then
A5: Cl(Int(A)) \/ Cl(Int(B)) c= Cl(Int(A \/ B)) by PRE_TOPC:20;
A \/ B c= Cl(Int(A)) \/ Cl(Int(B)) by A4,A3,XBOOLE_1:13;
then A \/ B c= Cl(Int(A \/ B)) by A5;
then
A6: Int(Cl(A \/ B)) \/ (A \/ B) c= Int(Cl(A \/ B)) \/ Cl(Int(A \/ B)) by
XBOOLE_1:9;
Cl(Int(Int(Cl(A \/ B))) \/ Int(A \/ B)) c= Cl(Int(X)) by PRE_TOPC:19
,TOPS_1:20;
then
A7: Cl(Int(Cl(A \/ B))) \/ Cl(Int(A \/ B)) c= Cl(Int(X)) by PRE_TOPC:20;
Cl(Int(Cl(A \/ B))) c= Cl(Cl(A \/ B)) by PRE_TOPC:19,TOPS_1:16;
then Cl(Int(Cl(A \/ B))) \/ Cl(A \/ B) = Cl(A \/ B) by XBOOLE_1:12;
then Int(Cl(X)) = Int(Cl(A \/ B)) by PRE_TOPC:20;
then
A8: Int(Cl(X)) c= X by XBOOLE_1:7;
Int(Cl(A \/ B)) \/ Cl(Int(A \/ B)) c= Cl(Int(Cl(A \/ B))) \/ Cl(Int(A
\/ B)) by PRE_TOPC:18,XBOOLE_1:9;
then Int(Cl(A \/ B)) \/ Cl(Int(A \/ B)) c= Cl(Int(X)) by A7;
then X c= Cl(Int(X)) by A6;
hence thesis by A8,TOPS_1:def 6;
end;
A9: Int(Cl(B)) c= B by A2,TOPS_1:def 6;
A10: Int(Cl(A)) c= A by A1,TOPS_1:def 6;
thus Cl(Int(A /\ B)) /\ (A /\ B) is condensed
proof
set X = Cl(Int(A /\ B)) /\ (A /\ B);
Int(Cl(A /\ B)) c= Int(Cl(A) /\ Cl(B)) by PRE_TOPC:21,TOPS_1:19;
then
A11: Int(Cl(A /\ B)) c= Int(Cl(A)) /\ Int(Cl(B)) by TOPS_1:17;
Int(Cl(A)) /\ Int(Cl(B)) c= A /\ B by A10,A9,XBOOLE_1:27;
then Int(Cl(A /\ B)) c= A /\ B by A11;
then
A12: Cl(Int(A /\ B)) /\ Int(Cl(A /\ B)) c= Cl(Int(A /\ B)) /\ (A /\ B) by
XBOOLE_1:26;
Int(Cl(X)) c= Int(Cl(Cl(Int(A /\ B))) /\ Cl(A /\ B)) by PRE_TOPC:21
,TOPS_1:19;
then
A13: Int(Cl(X)) c= Int(Cl(Int(A /\ B))) /\ Int(Cl(A /\ B)) by TOPS_1:17;
Int(Int(A /\ B)) c= Int(Cl(Int(A /\ B))) by PRE_TOPC:18,TOPS_1:19;
then Int(A /\ B) = Int(Cl(Int(A /\ B))) /\ Int(A /\ B) by XBOOLE_1:28;
then Cl(Int(A /\ B)) = Cl(Int(X)) by TOPS_1:17;
then
A14: X c= Cl(Int(X)) by XBOOLE_1:17;
Int(Cl(Int(A /\ B))) /\ Int(Cl(A /\ B)) c= Cl(Int(A /\ B)) /\ Int(Cl(
A /\ B)) by TOPS_1:16,XBOOLE_1:26;
then Int(Cl(X)) c= Cl(Int(A /\ B)) /\ Int(Cl(A /\ B)) by A13;
then Int(Cl(X)) c= X by A12;
hence thesis by A14,TOPS_1:def 6;
end;
end;
theorem Th18:
{} T is closed_condensed
proof
Cl Int {} T = {} T by PRE_TOPC:22;
hence thesis by TOPS_1:def 7;
end;
theorem Th19:
[#] T is closed_condensed
proof
Int [#] T = [#] T by TOPS_1:15;
then Cl Int [#] T = [#] T by TOPS_1:2;
hence thesis by TOPS_1:def 7;
end;
theorem Th20:
{} T is open_condensed
proof
Cl {} T = {} T by PRE_TOPC:22;
then Int Cl {} T = {} T;
hence thesis by TOPS_1:def 8;
end;
theorem Th21:
[#] T is open_condensed
proof
Cl [#] T = [#] T by TOPS_1:2;
then Int Cl [#] T = [#] T by TOPS_1:15;
hence thesis by TOPS_1:def 8;
end;
theorem Th22:
for A being Subset of T holds Cl(Int A) is closed_condensed
proof
let A be Subset of T;
Cl(Int A) = Cl Int Cl(Int A) by TOPS_1:26;
hence thesis by TOPS_1:def 7;
end;
theorem Th23:
for A being Subset of T holds Int(Cl A) is open_condensed
proof
let A be Subset of T;
Int(Cl A) = Int Cl Int(Cl A) by Th5;
hence thesis by TOPS_1:def 8;
end;
theorem Th24:
for A being Subset of T st A is condensed holds Cl A is closed_condensed
proof
let A be Subset of T;
assume
A1: A is condensed;
then Int Cl A c= A by TOPS_1:def 6;
then
A2: Cl Int Cl A c= Cl A by PRE_TOPC:19;
Cl A is condensed by A1,TOPS_1:71;
then Cl A c= Cl Int Cl A by TOPS_1:def 6;
then Cl A = Cl Int Cl A by A2;
hence thesis by TOPS_1:def 7;
end;
theorem Th25:
for A being Subset of T st A is condensed holds Int A is open_condensed
proof
let A be Subset of T;
assume
A1: A is condensed;
then A c= Cl Int A by TOPS_1:def 6;
then
A2: Int A c= Int Cl Int A by TOPS_1:19;
Int A is condensed by A1,TOPS_1:71;
then Int Cl Int A c= Int A by TOPS_1:def 6;
then Int Cl Int A = Int A by A2;
hence thesis by TOPS_1:def 8;
end;
theorem
for A being Subset of T st A is condensed holds Cl A` is
closed_condensed by Th16,Th24;
theorem
for A being Subset of T st A is condensed holds Int A` is
open_condensed by Th16,Th25;
theorem Th28:
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)))
proof
let A,B,C be Subset of T;
assume that
A1: A is closed_condensed and
A2: B is closed_condensed and
A3: C is closed_condensed;
A4: B = Cl Int B by A2,TOPS_1:def 7;
A5: (A /\ B) /\ C c= C by XBOOLE_1:17;
A6: Int(A /\ Cl Int(B /\ C)) c= A /\ Cl Int(B /\ C) by TOPS_1:16;
A7: Cl Int(B /\ C) = Cl(Int B /\ Int C) by TOPS_1:17;
C = Cl Int C by A3,TOPS_1:def 7;
then A /\ Cl Int(B /\ C) c= A /\ (B /\ C) by A7,A4,PRE_TOPC:21,XBOOLE_1:26;
then
A8: Int(A /\ Cl Int(B /\ C)) c= A /\ (B /\ C) by A6;
then Int(A /\ Cl Int(B /\ C)) c= (A /\ B) /\ C by XBOOLE_1:16;
then
A9: Int(A /\ Cl Int(B /\ C)) c= C by A5;
A10: (A /\ B) /\ C c= A /\ B by XBOOLE_1:17;
Int(A /\ Cl Int(B /\ C)) c= (A /\ B) /\ C by A8,XBOOLE_1:16;
then Int(A /\ Cl Int(B /\ C)) c= A /\ B by A10;
then
A11: Int Int(A /\ Cl Int(B /\ C)) c= Int(A /\ B) by TOPS_1:19;
Int(A /\ B) c= Cl Int(A /\ B) by PRE_TOPC:18;
then Int(A /\ Cl Int(B /\ C)) c= Cl Int(A /\ B) by A11;
then Int(A /\ Cl Int(B /\ C)) c= Cl Int(A /\ B) /\ C by A9,XBOOLE_1:19;
then Int Int(A /\ Cl Int(B /\ C)) c= Int(Cl Int(A /\ B) /\ C) by TOPS_1:19;
then
A12: Cl Int(A /\ Cl Int(B /\ C)) c= Cl Int(Cl Int(A /\ B) /\ C) by PRE_TOPC:19;
A13: A /\ (B /\ C) c= B /\ C by XBOOLE_1:17;
A14: A /\ (B /\ C) c= A by XBOOLE_1:17;
A15: Int(Cl Int(A /\ B) /\ C) c= Cl Int(A /\ B) /\ C by TOPS_1:16;
A16: Cl Int(A /\ B) = Cl(Int A /\ Int B) by TOPS_1:17;
A = Cl Int A by A1,TOPS_1:def 7;
then Cl Int(A /\ B) /\ C c= (A /\ B) /\ C by A16,A4,PRE_TOPC:21,XBOOLE_1:26;
then
A17: Int(Cl Int(A /\ B) /\ C) c= (A /\ B) /\ C by A15;
then Int(Cl Int(A /\ B) /\ C) c= A /\ (B /\ C) by XBOOLE_1:16;
then
A18: Int(Cl Int(A /\ B) /\ C) c= A by A14;
Int(Cl Int(A /\ B) /\ C) c= A /\ (B /\ C) by A17,XBOOLE_1:16;
then Int(Cl Int(A /\ B) /\ C) c= B /\ C by A13;
then
A19: Int Int(Cl Int(A /\ B) /\ C) c= Int(B /\ C) by TOPS_1:19;
Int(B /\ C) c= Cl Int(B /\ C) by PRE_TOPC:18;
then Int(Cl Int(A /\ B) /\ C) c= Cl Int(B /\ C) by A19;
then Int(Cl Int(A /\ B) /\ C) c= A /\ Cl Int(B /\ C) by A18,XBOOLE_1:19;
then Int Int(Cl Int(A /\ B) /\ C) c= Int(A /\ Cl Int(B /\ C)) by TOPS_1:19;
then Cl Int(Cl Int(A /\ B) /\ C) c= Cl Int(A /\ Cl Int(B /\ C)) by
PRE_TOPC:19;
hence thesis by A12;
end;
theorem Th29:
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)))
proof
let A,B,C be Subset of T;
assume that
A1: A is open_condensed and
A2: B is open_condensed and
A3: C is open_condensed;
A4: B = Int Cl B by A2,TOPS_1:def 8;
A5: C c= (A \/ B) \/ C by XBOOLE_1:7;
A6: A \/ Int Cl(B \/ C) c= Cl(A \/ Int Cl(B \/ C)) by PRE_TOPC:18;
A7: Int Cl(B \/ C) = Int(Cl B \/ Cl C) by PRE_TOPC:20;
C = Int Cl C by A3,TOPS_1:def 8;
then A \/ (B \/ C) c= A \/ Int Cl(B \/ C) by A7,A4,TOPS_1:20,XBOOLE_1:9;
then
A8: A \/ (B \/ C) c= Cl(A \/ Int Cl(B \/ C)) by A6;
then (A \/ B) \/ C c= Cl(A \/ Int Cl(B \/ C)) by XBOOLE_1:4;
then
A9: C c= Cl(A \/ Int Cl(B \/ C)) by A5;
A10: A \/ B c= (A \/ B) \/ C by XBOOLE_1:7;
(A \/ B) \/ C c= Cl(A \/ Int Cl(B \/ C)) by A8,XBOOLE_1:4;
then A \/ B c= Cl(A \/ Int Cl(B \/ C)) by A10;
then
A11: Cl(A \/ B) c= Cl Cl(A \/ Int Cl(B \/ C)) by PRE_TOPC:19;
Int Cl(A \/ B) c= Cl(A \/ B) by TOPS_1:16;
then Int Cl(A \/ B) c= Cl(A \/ Int Cl(B \/ C)) by A11;
then Int Cl(A \/ B) \/ C c= Cl(A \/ Int Cl(B \/ C)) by A9,XBOOLE_1:8;
then Cl(Int Cl(A \/ B) \/ C) c= Cl Cl(A \/ Int Cl(B \/ C)) by PRE_TOPC:19;
then
A12: Int Cl(Int Cl(A \/ B) \/ C) c= Int Cl(A \/ Int Cl(B \/ C)) by TOPS_1:19;
A13: B \/ C c= A \/ (B \/ C) by XBOOLE_1:7;
A14: A c= A \/ (B \/ C) by XBOOLE_1:7;
A15: Int Cl(A \/ B) \/ C c= Cl(Int Cl(A \/ B) \/ C) by PRE_TOPC:18;
A16: Int Cl(A \/ B) = Int(Cl A \/ Cl B) by PRE_TOPC:20;
A = Int Cl A by A1,TOPS_1:def 8;
then (A \/ B) \/ C c= Int Cl(A \/ B) \/ C by A16,A4,TOPS_1:20,XBOOLE_1:9;
then
A17: (A \/ B) \/ C c= Cl(Int Cl(A \/ B) \/ C) by A15;
then A \/ (B \/ C) c= Cl(Int Cl(A \/ B) \/ C) by XBOOLE_1:4;
then
A18: A c= Cl(Int Cl(A \/ B) \/ C) by A14;
A \/ (B \/ C) c= Cl(Int Cl(A \/ B) \/ C) by A17,XBOOLE_1:4;
then B \/ C c= Cl(Int Cl(A \/ B) \/ C) by A13;
then
A19: Cl(B \/ C) c= Cl Cl(Int Cl(A \/ B) \/ C) by PRE_TOPC:19;
Int Cl(B \/ C) c= Cl(B \/ C) by TOPS_1:16;
then Int Cl(B \/ C) c= Cl(Int Cl(A \/ B) \/ C) by A19;
then A \/ Int Cl(B \/ C) c= Cl(Int Cl(A \/ B) \/ C) by A18,XBOOLE_1:8;
then Cl(A \/ Int Cl(B \/ C)) c= Cl Cl(Int Cl(A \/ B) \/ C) by PRE_TOPC:19;
then Int Cl(A \/ Int Cl(B \/ C)) c= Int Cl(Int Cl(A \/ B) \/ C) by TOPS_1:19;
hence thesis by A12;
end;
begin
:: 3. The Lattice of Domains.
definition
let T be TopStruct;
func Domains_of T -> Subset-Family of T equals
{ A where A is Subset of T :
A is condensed };
coherence
proof
set B = { A where A is Subset of T : A is condensed };
B c= bool the carrier of T
proof
let x be object;
assume x in B;
then ex A being Subset of T st x = A & A is condensed;
hence thesis;
end;
hence thesis;
end;
end;
registration
let T be TopSpace;
cluster Domains_of T -> non empty;
coherence
proof
{} T is condensed by Th14;
then {} T in { A where A is Subset of T : A is condensed };
hence thesis;
end;
end;
definition
let T be TopSpace;
func Domains_Union T -> BinOp of Domains_of T means
:Def2:
for A,B being
Element of Domains_of T holds it.(A,B) = Int(Cl(A \/ B)) \/ (A \/ B);
existence
proof
defpred X[set,set] means for A,B being Element of Domains_of T st $1 = [A,
B] holds $2 = Int(Cl(A \/ B)) \/ (A \/ B);
set D = [:Domains_of T,(Domains_of T) qua non empty set:];
A1: for a being Element of D ex b being Element of Domains_of T st X[a,b]
proof
let a be Element of D;
reconsider G = a`1, F = a`2 as Element of Domains_of T;
F in { H where H is Subset of T : H is condensed };
then
A2: ex H being Subset of T st H = F & H is condensed;
G in { E where E is Subset of T : E is condensed };
then ex E being Subset of T st E = G & E is condensed;
then Int(Cl(G \/ F)) \/ (G \/ F) is condensed by A2,Th17;
then Int(Cl(G \/ F)) \/ (G \/ F) in { E where E is Subset of T : E is
condensed };
then reconsider
b = Int(Cl(G \/ F)) \/ (G \/ F) as Element of Domains_of T;
take b;
let A,B be Element of Domains_of T;
assume a = [A,B];
then
A3: [A,B] = [G,F] by MCART_1:21;
then
A4: B = F by XTUPLE_0:1;
A = G by A3,XTUPLE_0:1;
hence thesis by A4;
end;
consider h being Function of D, Domains_of T such that
A5: for a being Element of D holds X[a,h.a] from FUNCT_2:sch 3(A1);
take h;
let A,B be Element of Domains_of T;
thus h.(A,B) = h . [A,B] .= Int(Cl(A \/ B)) \/ (A \/ B) by A5;
end;
uniqueness
proof
deffunc U(Element of Domains_of T,Element of Domains_of T) = Int(Cl($1 \/
$2)) \/ ($1 \/ $2);
thus for o1,o2 being BinOp of Domains_of T st (for a,b being Element of
Domains_of T holds o1.(a,b) = U(a,b)) & (for a,b being Element of Domains_of T
holds o2.(a,b) = U(a,b)) holds o1 = o2 from BINOP_2:sch 2;
end;
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
:Def3:
for A,B being
Element of Domains_of T holds it.(A,B) = Cl(Int(A /\ B)) /\ (A /\ B);
existence
proof
defpred X[set,set] means for A,B being Element of Domains_of T st $1 = [A,
B] holds $2 = Cl(Int(A /\ B)) /\ (A /\ B);
set D = [:Domains_of T,(Domains_of T) qua non empty set:];
A1: for a being Element of D ex b being Element of Domains_of T st X[a,b]
proof
let a be Element of D;
reconsider G = a`1, F = a`2 as Element of Domains_of T;
F in { H where H is Subset of T : H is condensed };
then
A2: ex H being Subset of T st H = F & H is condensed;
G in { E where E is Subset of T : E is condensed };
then ex E being Subset of T st E = G & E is condensed;
then Cl(Int(G /\ F)) /\ (G /\ F) is condensed by A2,Th17;
then Cl(Int(G /\ F)) /\ (G /\ F) in { E where E is Subset of T : E is
condensed };
then reconsider
b = Cl(Int(G /\ F)) /\ (G /\ F) as Element of Domains_of T;
take b;
let A,B be Element of Domains_of T;
assume a = [A,B];
then
A3: [A,B] = [G,F] by MCART_1:21;
then
A4: B = F by XTUPLE_0:1;
A = G by A3,XTUPLE_0:1;
hence thesis by A4;
end;
consider h being Function of D, Domains_of T such that
A5: for a being Element of D holds X[a,h.a] from FUNCT_2:sch 3(A1);
take h;
let A,B be Element of Domains_of T;
thus h.(A,B) = h . [A,B] .= Cl(Int(A /\ B)) /\ (A /\ B) by A5;
end;
uniqueness
proof
deffunc U(Element of Domains_of T,Element of Domains_of T) = Cl(Int($1 /\
$2)) /\ ($1 /\ $2);
thus for o1,o2 being BinOp of Domains_of T st (for a,b being Element of
Domains_of T holds o1.(a,b) = U(a,b)) & (for a,b being Element of Domains_of T
holds o2.(a,b) = U(a,b)) holds o1 = o2 from BINOP_2:sch 2;
end;
end;
notation
let T be TopSpace;
synonym D-Meet T for Domains_Meet T;
end;
theorem Th30:
for T being TopSpace holds LattStr(#Domains_of T,D-Union T,
D-Meet T#) is C_Lattice
proof
let T be TopSpace;
set L = LattStr(#Domains_of T,D-Union T,D-Meet T#);
A1: L is join-commutative
proof
let a,b be Element of L;
reconsider A = a, B = b as Element of Domains_of T;
thus a"\/"b = Int(Cl(B \/ A)) \/ (B \/ A) by Def2
.= b"\/"a by Def2;
end;
A2: L is meet-absorbing
proof
let a,b be Element of L;
reconsider A = a, B = b as Element of Domains_of T;
A3: Cl(Int(A /\ B)) /\ (A /\ B) c= A /\ B by XBOOLE_1:17;
B in { D where D is Subset of T : D is condensed };
then ex D being Subset of T st D = B & D is condensed;
then
A4: Int(Cl(B)) c= B by TOPS_1:def 6;
A5: A /\ B c= B by XBOOLE_1:17;
a"/\"b = Cl(Int(A /\ B)) /\ (A /\ B) by Def3;
hence (a"/\"b)"\/"b = Int(Cl((Cl(Int(A /\ B)) /\ (A /\ B)) \/ B)) \/ ((Cl(
Int(A /\ B)) /\ (A /\ B)) \/ B) by Def2
.= Int(Cl((Cl(Int(A /\ B)) /\ (A /\ B)) \/ B)) \/ B by A3,A5,XBOOLE_1:1
,12
.= Int(Cl(B)) \/ B by A3,A5,XBOOLE_1:1,12
.= b by A4,XBOOLE_1:12;
end;
A6: L is join-associative
proof
let a,b,c be Element of L;
reconsider A = a, B = b, C = c as Element of Domains_of T;
A7: a"\/"b = Int(Cl(A \/ B)) \/ (A \/ B) by Def2;
b"\/"c = Int(Cl(B \/ C)) \/ (B \/ C) by Def2;
hence a"\/"(b"\/"c) = Int(Cl(A \/ (Int(Cl(B \/ C)) \/ (B \/ C)))) \/ (A \/
(Int(Cl(B \/ C)) \/ (B \/ C))) by Def2
.= Int Cl(A \/ (B \/ C)) \/ (A \/ (B \/ C)) by Th10
.= Int Cl(A \/ (B \/ C)) \/ (A \/ B \/ C) by XBOOLE_1:4
.= Int Cl(A \/ B \/ C) \/ (A \/ B \/ C) by XBOOLE_1:4
.= Int(Cl((Int(Cl(A \/ B)) \/ (A \/ B)) \/ C)) \/ ((Int(Cl(A \/ B)) \/
(A \/ B)) \/ C) by Th10
.= (a"\/"b)"\/"c by A7,Def2;
end;
A8: L is meet-commutative
proof
let a,b be Element of L;
reconsider A = a, B = b as Element of Domains_of T;
thus a"/\"b = Cl(Int(B /\ A)) /\ (B /\ A) by Def3
.= b"/\"a by Def3;
end;
A9: L is join-absorbing
proof
let a,b be Element of L;
reconsider A = a, B = b as Element of Domains_of T;
A10: A c= (A \/ B) by XBOOLE_1:7;
A in { D where D is Subset of T : D is condensed };
then ex D being Subset of T st D = A & D is condensed;
then
A11: A c= Cl(Int(A)) by TOPS_1:def 6;
A12: (A \/ B) c= Int(Cl(A \/ B)) \/ (A \/ B) by XBOOLE_1:7;
a"\/"b = Int(Cl(A \/ B)) \/ (A \/ B) by Def2;
hence a"/\"(a"\/"b) = Cl(Int(A /\ (Int(Cl(A \/ B)) \/ (A \/ B)))) /\ (A /\
(Int(Cl(A \/ B)) \/ (A \/ B))) by Def3
.= Cl(Int(A /\ (Int(Cl(A \/ B)) \/ (A \/ B)))) /\ A by A10,A12,XBOOLE_1:1
,28
.= Cl(Int(A)) /\ A by A10,A12,XBOOLE_1:1,28
.= a by A11,XBOOLE_1:28;
end;
L is meet-associative
proof
let a,b,c be Element of L;
reconsider A = a, B = b, C = c as Element of Domains_of T;
A13: a"/\"b = Cl(Int(A /\ B)) /\ (A /\ B) by Def3;
b"/\"c = Cl(Int(B /\ C)) /\ (B /\ C) by Def3;
hence a"/\"(b"/\"c) = Cl(Int(A /\ (Cl(Int(B /\ C)) /\ (B /\ C)))) /\ (A /\
(Cl(Int(B /\ C)) /\ (B /\ C))) by Def3
.= Cl Int(A /\ (B /\ C)) /\ (A /\ (B /\ C)) by Th12
.= Cl Int(A /\ (B /\ C)) /\ (A /\ B /\ C) by XBOOLE_1:16
.= Cl Int(A /\ B /\ C) /\ (A /\ B /\ C) by XBOOLE_1:16
.= Cl(Int((Cl(Int(A /\ B)) /\ (A /\ B)) /\ C)) /\ ((Cl(Int(A /\ B)) /\
(A /\ B)) /\ C) by Th12
.= (a"/\"b)"/\"c by A13,Def3;
end;
then reconsider L as Lattice by A1,A6,A2,A8,A9;
A14: L is lower-bounded
proof
{} T is condensed by Th14;
then {} T in { D where D is Subset of T : D is condensed };
then reconsider c = {} T as Element of L;
take c;
let a be Element of L;
reconsider C = c, A = a as Element of Domains_of T;
C /\ A = C;
hence c"/\"a = Cl(Int(C)) /\ C by Def3
.= c;
hence a"/\"c = c;
end;
L is upper-bounded
proof
[#] T is condensed by Th15;
then [#] T in { D where D is Subset of T : D is condensed };
then reconsider c = [#] T as Element of L;
take c;
let a be Element of L;
reconsider C = c, A = a as Element of Domains_of T;
C \/ A = C by XBOOLE_1:12;
hence c"\/"a = Int(Cl(C)) \/ C by Def2
.= c by XBOOLE_1:12;
hence a"\/"c = c;
end;
then reconsider L as 01_Lattice by A14;
L is complemented
proof
[#] T is condensed by Th15;
then [#] T in { D where D is Subset of T : D is condensed};
then reconsider c = [#] T as Element of L;
let b be Element of L;
reconsider B = b as Element of Domains_of T;
A15: (B`) misses B by XBOOLE_1:79;
B in { D where D is Subset of T : D is condensed};
then ex D being Subset of T st D = B & D is condensed;
then B` is condensed by Th16;
then B` in { D where D is Subset of T : D is condensed};
then reconsider a = B` as Element of L;
take a;
A16: for v being Element of L holds (the L_meet of L).(c,v) = v
proof
let v be Element of L;
reconsider V = v as Element of Domains_of T;
V in { D where D is Subset of T : D is condensed};
then ex D being Subset of T st D = V & D is condensed;
then
A17: V c= Cl(Int V) by TOPS_1:def 6;
thus (the L_meet of L).(c,v) = Cl(Int([#] T /\ V)) /\ ([#] T /\ V) by
Def3
.= Cl(Int([#] T /\ V)) /\ V by XBOOLE_1:28
.= Cl(Int V) /\ V by XBOOLE_1:28
.= v by A17,XBOOLE_1:28;
end;
thus a"\/"b = Int(Cl(B` \/ B)) \/ (B` \/ B) by Def2
.= Int(Cl(B` \/ B)) \/ ([#] T) by PRE_TOPC:2
.= c by XBOOLE_1:12
.= Top L by A16,LATTICE2:17;
hence b"\/"a = Top L;
{} T is condensed by Th14;
then {} T in { D where D is Subset of T : D is condensed};
then reconsider c = {} T as Element of L;
A18: for v being Element of L holds (the L_join of L).(c,v) = v
proof
let v be Element of L;
reconsider V = v as Element of Domains_of T;
V in { D where D is Subset of T : D is condensed};
then ex D being Subset of T st D = V & D is condensed;
then
A19: Int(Cl V) c= V by TOPS_1:def 6;
thus (the L_join of L).(c,v) = Int(Cl({} T \/ V)) \/ ({} T \/ V) by Def2
.= Int(Cl((([#]T)`) \/ V)) \/ ({} T \/ V) by XBOOLE_1:37
.= Int(Cl((([#]T)`) \/ (V``))) \/ ((([#]T)`) \/ V) by XBOOLE_1:37
.= Int(Cl((([#] T) /\ V`)`)) \/ (([#] T)` \/ (V``)) by XBOOLE_1:54
.= Int(Cl((([#] T) /\ V`)`)) \/ ((([#] T) /\ V`)`) by XBOOLE_1:54
.= Int(Cl((V`)`)) \/ ((([#] T) /\ V`))` by XBOOLE_1:28
.= Int(Cl V) \/ ((V``)) by XBOOLE_1:28
.= v by A19,XBOOLE_1:12;
end;
thus a"/\"b = Cl(Int((B`) /\ B)) /\ ((B`) /\ B) by Def3
.= Cl(Int((B`) /\ B)) /\ ({} T) by A15
.= Bottom L by A18,LATTICE2:15;
hence b"/\"a = Bottom L;
end;
hence thesis;
end;
definition
let T be TopSpace;
func Domains_Lattice T -> C_Lattice equals
LattStr(#Domains_of T,
Domains_Union T,Domains_Meet T#);
coherence by Th30;
end;
begin
:: 4. The Lattice of Closed Domains.
definition
let T be TopStruct;
func Closed_Domains_of T -> Subset-Family of T equals
{ A where A is Subset
of T : A is closed_condensed };
coherence
proof
set B = { A where A is Subset of T : A is closed_condensed };
B c= bool the carrier of T
proof
let x be object;
assume x in B;
then ex A being Subset of T st x = A & A is closed_condensed;
hence thesis;
end;
hence thesis;
end;
end;
registration
let T be TopSpace;
cluster Closed_Domains_of T -> non empty;
coherence
proof
{} T is closed_condensed by Th18;
then {} T in { A where A is Subset of T : A is closed_condensed };
hence thesis;
end;
end;
theorem Th31:
for T being TopSpace holds Closed_Domains_of T c= Domains_of T
proof
let T be TopSpace;
let x be object;
assume x in Closed_Domains_of T; then
x in { A where A is Subset of T : A is closed_condensed }; then
consider A1 being Subset of T such that
A1: x = A1 & A1 is closed_condensed;
A1 is condensed by A1,TOPS_1:66; then
x in { A where A is Subset of T : A is condensed } by A1;
hence thesis;
end;
definition
let T be TopSpace;
func Closed_Domains_Union T -> BinOp of Closed_Domains_of T means
:Def6:
for A,B being Element of Closed_Domains_of T holds it.(A,B) = A \/ B;
existence
proof
defpred X[set,set] means for A,B being Element of Closed_Domains_of T st
$1 = [A,B] holds $2 = A \/ B;
set D = [:Closed_Domains_of T,(Closed_Domains_of T) qua non empty set:];
A1: for a being Element of D ex b being Element of Closed_Domains_of T st
X[a,b]
proof
let a be Element of D;
reconsider G = a`1, F = a`2 as Element of Closed_Domains_of T;
G in { E where E is Subset of T : E is closed_condensed };
then consider E being Subset of T such that
A2: E = G and
A3: E is closed_condensed;
F in { H where H is Subset of T : H is closed_condensed };
then consider H being Subset of T such that
A4: H = F and
A5: H is closed_condensed;
E \/ H is closed_condensed by A3,A5,TOPS_1:68;
then
G \/ F in { K where K is Subset of T : K is closed_condensed } by A2,A4;
then reconsider b = G \/ F as Element of Closed_Domains_of T;
take b;
let A,B be Element of Closed_Domains_of T;
assume a = [A,B];
then
A6: [A,B] = [G,F] by MCART_1:21;
then A = G by XTUPLE_0:1;
hence thesis by A6,XTUPLE_0:1;
end;
consider h being Function of D, Closed_Domains_of T such that
A7: for a being Element of D holds X[a,h.a] from FUNCT_2:sch 3(A1);
take h;
let A,B be Element of Closed_Domains_of T;
thus h.(A,B) = h . [A,B] .= A \/ B by A7;
end;
uniqueness
proof
deffunc U(Element of Closed_Domains_of T,Element of Closed_Domains_of T) =
$1 \/ $2;
thus for o1,o2 being BinOp of Closed_Domains_of T st (for a,b being
Element of Closed_Domains_of T holds o1.(a,b) = U(a,b)) & (for a,b being
Element of Closed_Domains_of T holds o2.(a,b) = U(a,b)) holds o1 = o2 from
BINOP_2:sch 2;
end;
end;
notation
let T be TopSpace;
synonym CLD-Union T for Closed_Domains_Union T;
end;
theorem Th32:
for A,B being Element of Closed_Domains_of T holds (CLD-Union T)
.(A,B) = (D-Union T).(A,B)
proof
let A,B be Element of Closed_Domains_of T;
A1: A in { D where D is Subset of T : D is closed_condensed };
Closed_Domains_of T c= Domains_of T by Th31; then
reconsider A0 = A, B0 = B as Element of Domains_of T;
B in { E where E is Subset of T : E is closed_condensed };
then consider E being Subset of T such that
A2: E = B and
A3: E is closed_condensed;
consider D being Subset of T such that
A4: D = A and
A5: D is closed_condensed by A1;
D \/ E is closed_condensed by A5,A3,TOPS_1:68;
then D \/ E is condensed by TOPS_1:66;
then
A6: Int Cl(A \/ B) c= A \/ B by A4,A2,TOPS_1:def 6;
thus (CLD-Union T).(A,B) = A \/ B by Def6
.= Int(Cl(A0 \/ B0)) \/ (A0 \/ B0) by A6,XBOOLE_1:12
.= (D-Union T).(A,B) by Def2;
end;
definition
let T be TopSpace;
func Closed_Domains_Meet T -> BinOp of Closed_Domains_of T means
:Def7:
for
A,B being Element of Closed_Domains_of T holds it.(A,B) = Cl(Int(A /\ B));
existence
proof
defpred X[set,set] means for A,B being Element of Closed_Domains_of T st
$1 = [A,B] holds $2 = Cl Int(A /\ B);
set D = [:Closed_Domains_of T, Closed_Domains_of T:];
A1: for a being Element of D ex b being Element of Closed_Domains_of T st
X[a,b]
proof
let a be Element of D;
reconsider G = a`1, F = a`2 as Element of Closed_Domains_of T;
Cl(Int(G /\ F)) is closed_condensed by Th22;
then Cl(Int(G /\ F)) in { E where E is Subset of T : E is
closed_condensed };
then reconsider b = Cl(Int(G /\ F)) as Element of Closed_Domains_of T;
take b;
let A,B be Element of Closed_Domains_of T;
assume a = [A,B];
then
A2: [A,B] = [G,F] by MCART_1:21;
then A = G by XTUPLE_0:1;
hence thesis by A2,XTUPLE_0:1;
end;
consider h being Function of D, Closed_Domains_of T such that
A3: for a being Element of D holds X[a,h.a] from FUNCT_2:sch 3(A1);
take h;
let A,B be Element of Closed_Domains_of T;
thus h.(A,B) = h . [A,B] .= Cl(Int(A /\ B)) by A3;
end;
uniqueness
proof
deffunc U(Element of Closed_Domains_of T,Element of Closed_Domains_of T) =
Cl Int($1 /\ $2);
thus for o1,o2 being BinOp of Closed_Domains_of T st (for a,b being
Element of Closed_Domains_of T holds o1.(a,b) = U(a,b)) & (for a,b being
Element of Closed_Domains_of T holds o2.(a,b) = U(a,b)) holds o1 = o2 from
BINOP_2:sch 2;
end;
end;
notation
let T be TopSpace;
synonym CLD-Meet T for Closed_Domains_Meet T;
end;
theorem Th33:
for A,B being Element of Closed_Domains_of T holds (CLD-Meet T).
(A,B) = (D-Meet T).(A,B)
proof
let A,B be Element of Closed_Domains_of T;
A in { D where D is Subset of T : D is closed_condensed };
then consider D being Subset of T such that
A1: D = A and
A2: D is closed_condensed;
A3: Int(A /\ B) c= A /\ B by TOPS_1:16;
Closed_Domains_of T c= Domains_of T by Th31; then
reconsider A0 = A, B0 = B as Element of Domains_of T;
B in { E where E is Subset of T : E is closed_condensed };
then consider E being Subset of T such that
A4: E = B and
A5: E is closed_condensed;
A6: E is closed by A5,TOPS_1:66;
D is closed by A2,TOPS_1:66;
then
A7: Cl(D /\ E) = D /\ E by A6,PRE_TOPC:22;
thus (CLD-Meet T).(A,B) = Cl(Int(A /\ B)) by Def7
.= Cl(Int(A0 /\ B0)) /\ (A0 /\ B0) by A1,A4,A7,A3,PRE_TOPC:19,XBOOLE_1:28
.= (D-Meet T).(A,B) by Def3;
end;
theorem Th34:
for T being TopSpace holds LattStr(#Closed_Domains_of T,
CLD-Union T,CLD-Meet T#) is B_Lattice
proof
let T be TopSpace;
set L = LattStr(#Closed_Domains_of T,CLD-Union T,CLD-Meet T#);
A1: L is join-commutative
proof
let a,b be Element of L;
reconsider A = a, B = b as Element of Closed_Domains_of T;
thus a"\/"b = B \/ A by Def6
.= b"\/"a by Def6;
end;
A2: L is meet-absorbing
proof
let a,b be Element of L;
reconsider A = a, B = b as Element of Closed_Domains_of T;
A3: Cl Int A /\ B c= B by XBOOLE_1:17;
B in { D where D is Subset of T : D is closed_condensed };
then ex D being Subset of T st D = B & D is closed_condensed;
then
A4: B = Cl Int B by TOPS_1:def 7;
Cl(Int(A /\ B)) = Cl(Int A /\ Int B) by TOPS_1:17;
then
A5: Cl(Int(A /\ B)) c= Cl Int A /\ B by A4,PRE_TOPC:21;
a"/\"b = Cl(Int(A /\ B)) by Def7;
hence (a"/\"b)"\/"b = Cl(Int(A /\ B)) \/ B by Def6
.= b by A5,A3,XBOOLE_1:1,12;
end;
A6: L is join-absorbing
proof
let a,b be Element of L;
reconsider A = a, B = b as Element of Closed_Domains_of T;
A in { D where D is Subset of T : D is closed_condensed };
then
A7: ex D being Subset of T st D = A & D is closed_condensed;
a"\/"b = A \/ B by Def6;
hence a"/\"(a"\/"b) = Cl(Int(A /\ (A \/ B))) by Def7
.= Cl(Int(A)) by XBOOLE_1:21
.= a by A7,TOPS_1:def 7;
end;
A8: L is join-associative
proof
let a,b,c be Element of L;
reconsider A = a, B = b, C = c as Element of Closed_Domains_of T;
A9: a"\/"b = A \/ B by Def6;
b"\/"c = B \/ C by Def6;
hence a"\/"(b"\/"c) = A \/ (B \/ C) by Def6
.= (A \/ B) \/ C by XBOOLE_1:4
.= (a"\/"b)"\/"c by A9,Def6;
end;
A10: L is meet-associative
proof
let a,b,c be Element of L;
reconsider A = a, B = b, C = c as Element of Closed_Domains_of T;
A in { D where D is Subset of T : D is closed_condensed };
then
A11: ex D being Subset of T st D = A & D is closed_condensed;
B in { E where E is Subset of T : E is closed_condensed };
then
A12: ex E being Subset of T st E = B & E is closed_condensed;
C in { F where F is Subset of T : F is closed_condensed };
then
A13: ex F being Subset of T st F = C & F is closed_condensed;
A14: a"/\"b = Cl(Int(A /\ B)) by Def7;
b"/\"c = Cl(Int(B /\ C)) by Def7;
hence a"/\"(b"/\"c) = Cl(Int(A /\ (Cl(Int(B /\ C))))) by Def7
.= Cl(Int((Cl(Int(A /\ B)) /\ C))) by A11,A12,A13,Th28
.= (a"/\"b)"/\"c by A14,Def7;
end;
L is meet-commutative
proof
let a,b be Element of L;
reconsider A = a, B = b as Element of Closed_Domains_of T;
thus a"/\"b = Cl(Int(B /\ A)) by Def7
.= b"/\"a by Def7;
end;
then reconsider L as Lattice by A1,A8,A2,A10,A6;
A15: L is upper-bounded
proof
[#] T is closed_condensed by Th19;
then [#] T in { D where D is Subset of T : D is closed_condensed };
then reconsider c = [#] T as Element of L;
take c;
let a be Element of L;
reconsider C = c, A = a as Element of Closed_Domains_of T;
thus c"\/"a = C \/ A by Def6
.= c by XBOOLE_1:12;
hence a"\/"c = c;
end;
A16: L is distributive
proof
let a,b,c be Element of L;
reconsider A = a, B = b, C = c as Element of Closed_Domains_of T;
A in { D where D is Subset of T : D is closed_condensed };
then consider D being Subset of T such that
A17: D = A and
A18: D is closed_condensed;
A19: D is closed by A18,TOPS_1:66;
B in { E where E is Subset of T : E is closed_condensed };
then consider E being Subset of T such that
A20: E = B and
A21: E is closed_condensed;
A22: E is closed by A21,TOPS_1:66;
A23: a"/\"c = Cl(Int(A /\ C)) by Def7;
A24: a"/\"b = Cl(Int(A /\ B)) by Def7;
b"\/"c = B \/ C by Def6;
hence a"/\"(b"\/"c) = Cl(Int(A /\ (B \/ C))) by Def7
.= Cl(Int((A /\ B) \/ (A /\ C))) by XBOOLE_1:23
.= Cl(Int(A /\ B)) \/ Cl(Int(A /\ C)) by A17,A20,A19,A22,Th6
.= (a"/\"b)"\/"(a"/\"c) by A24,A23,Def6;
end;
A25: L is complemented
proof
[#] T is closed_condensed by Th19;
then [#] T in { K where K is Subset of T : K is closed_condensed};
then reconsider c = [#] T as Element of L;
let b be Element of L;
reconsider B = b as Element of Closed_Domains_of T;
B in { D where D is Subset of T : D is closed_condensed};
then consider D being Subset of T such that
A26: D = B and
A27: D is closed_condensed;
D is condensed by A27,TOPS_1:66;
then Cl B` is closed_condensed by A26,Th16,Th24;
then Cl B` in { K where K is Subset of T : K is closed_condensed};
then reconsider a = Cl B` as Element of L;
take a;
A28: D is closed by A27,TOPS_1:66;
A29: for v being Element of L holds (the L_meet of L).(c,v) = v
proof
let v be Element of L;
reconsider V = v as Element of Closed_Domains_of T;
V in { K where K is Subset of T : K is closed_condensed};
then
A30: ex D being Subset of T st D = V & D is closed_condensed;
thus (the L_meet of L).(c,v) = Cl(Int([#] T /\ V)) by Def7
.= Cl(Int V) by XBOOLE_1:28
.= v by A30,TOPS_1:def 7;
end;
thus a"\/"b = Cl B` \/ B by Def6
.= Cl D` \/ Cl D by A26,A28,PRE_TOPC:22
.= Cl(B` \/ B) by A26,PRE_TOPC:20
.= Cl [#] T by PRE_TOPC:2
.= c by TOPS_1:2
.= Top L by A29,LATTICE2:17;
hence b"\/"a = Top L;
{} T is closed_condensed by Th18;
then {} T in { K where K is Subset of T : K is closed_condensed};
then reconsider c = {} T as Element of L;
A31: for v being Element of L holds (the L_join of L).(c,v) = v
proof
let v be Element of L;
reconsider V = v as Element of Closed_Domains_of T;
thus (the L_join of L).(c,v) = {} T \/ V by Def6
.= (([#]T)`) \/ (V``) by XBOOLE_1:37
.= ([#] T /\ V`)` by XBOOLE_1:54
.= (V``) by XBOOLE_1:28
.= v;
end;
thus a"/\"b = Cl(Int(B /\ Cl B`)) by Def7
.= Cl({} T) by Th8
.= c by PRE_TOPC:22
.= Bottom L by A31,LATTICE2:15;
hence b"/\"a = Bottom L;
end;
L is lower-bounded
proof
A32: {} T is closed_condensed by Th18;
then {}T in { D where D is Subset of T : D is closed_condensed };
then reconsider c = {} T as Element of L;
take c;
let a be Element of L;
reconsider C = c, A = a as Element of Closed_Domains_of T;
thus c"/\"a = Cl(Int(C /\ A)) by Def7
.= c by A32,TOPS_1:def 7;
hence a"/\"c = c;
end;
hence thesis by A15,A25,A16;
end;
definition
let T be TopSpace;
func Closed_Domains_Lattice T-> B_Lattice equals
LattStr(#Closed_Domains_of
T,Closed_Domains_Union T,Closed_Domains_Meet T #);
coherence by Th34;
end;
begin
:: 5. The Lattice of Open Domains.
definition
let T be TopStruct;
func Open_Domains_of T -> Subset-Family of T equals
{ A where A is Subset of
T: A is open_condensed };
coherence
proof
set B = { A where A is Subset of T : A is open_condensed };
B c= bool the carrier of T
proof
let x be object;
assume x in B;
then ex A being Subset of T st x = A & A is open_condensed;
hence thesis;
end;
hence thesis;
end;
end;
registration
let T be TopSpace;
cluster Open_Domains_of T -> non empty;
coherence
proof
{} T is open_condensed by Th20;
then {} T in { A where A is Subset of T : A is open_condensed };
hence thesis;
end;
end;
theorem Th35:
for T being TopSpace holds Open_Domains_of T c= Domains_of T
proof
let T be TopSpace;
let x be object;
assume x in Open_Domains_of T; then
x in { A where A is Subset of T : A is open_condensed }; then
consider A1 being Subset of T such that
A1: x = A1 & A1 is open_condensed;
A1 is condensed by A1,TOPS_1:67; then
x in { A where A is Subset of T : A is condensed } by A1;
hence thesis;
end;
definition
let T be TopSpace;
func Open_Domains_Union T -> BinOp of Open_Domains_of T means
:Def10:
for A, B being Element of Open_Domains_of T holds it.(A,B) = Int(Cl(A \/ B));
existence
proof
defpred X[set,set] means for A,B being Element of Open_Domains_of T st $1
= [A,B] holds $2 = Int(Cl(A \/ B));
set D = [:Open_Domains_of T,(Open_Domains_of T) qua non empty set:];
A1: for a being Element of D ex b being Element of Open_Domains_of T st X[ a,b]
proof
let a be Element of D;
reconsider G = a`1, F = a`2 as Element of Open_Domains_of T;
Int(Cl(G \/ F)) is open_condensed by Th23;
then
Int(Cl(G \/ F)) in { E where E is Subset of T : E is open_condensed };
then reconsider b = Int(Cl(G \/ F)) as Element of Open_Domains_of T;
take b;
let A,B be Element of Open_Domains_of T;
assume a = [A,B];
then
A2: [A,B] = [G,F] by MCART_1:21;
then A = G by XTUPLE_0:1;
hence thesis by A2,XTUPLE_0:1;
end;
consider h being Function of D, Open_Domains_of T such that
A3: for a being Element of D holds X[a,h.a] from FUNCT_2:sch 3(A1);
take h;
let A,B be Element of Open_Domains_of T;
thus h.(A,B) = h . [A,B] .= Int(Cl(A \/ B)) by A3;
end;
uniqueness
proof
deffunc U(Element of Open_Domains_of T,Element of Open_Domains_of T) = Int
Cl($1 \/ $2);
thus for o1,o2 being BinOp of Open_Domains_of T st (for a,b being Element
of Open_Domains_of T holds o1.(a,b) = U(a,b)) & (for a,b being Element of
Open_Domains_of T holds o2.(a,b) = U(a,b)) holds o1 = o2 from BINOP_2:sch 2;
end;
end;
notation
let T be TopSpace;
synonym OPD-Union T for Open_Domains_Union T;
end;
theorem Th36:
for A,B being Element of Open_Domains_of T holds (OPD-Union T).(
A,B) = (D-Union T).(A,B)
proof
let A,B be Element of Open_Domains_of T;
A in { D where D is Subset of T : D is open_condensed };
then consider D being Subset of T such that
A1: D = A and
A2: D is open_condensed;
A3: A \/ B c= Cl(A \/ B) by PRE_TOPC:18;
Open_Domains_of T c= Domains_of T by Th35; then
reconsider A0 = A, B0 = B as Element of Domains_of T;
B in { E where E is Subset of T : E is open_condensed };
then consider E being Subset of T such that
A4: E = B and
A5: E is open_condensed;
A6: E is open by A5,TOPS_1:67;
D is open by A2,TOPS_1:67;
then
A7: Int(D \/ E) = D \/ E by A6,TOPS_1:23;
thus (OPD-Union T).(A,B) = Int(Cl(A \/ B)) by Def10
.= Int(Cl(A0 \/ B0)) \/ (A0 \/ B0) by A1,A4,A7,A3,TOPS_1:19,XBOOLE_1:12
.= (D-Union T).(A,B) by Def2;
end;
definition
let T be TopSpace;
func Open_Domains_Meet T -> BinOp of Open_Domains_of T means
:Def11:
for A,B being Element of Open_Domains_of T holds it.(A,B) = A /\ B;
existence
proof
defpred X[set,set] means for A,B being Element of Open_Domains_of T st $1
= [A,B] holds $2 = A /\ B;
set D = [:Open_Domains_of T,(Open_Domains_of T) qua non empty set:];
A1: for a being Element of D ex b being Element of Open_Domains_of T st X[ a,b]
proof
let a be Element of D;
reconsider G = a`1, F = a`2 as Element of Open_Domains_of T;
G in { E where E is Subset of T : E is open_condensed };
then consider E being Subset of T such that
A2: E = G and
A3: E is open_condensed;
F in { H where H is Subset of T : H is open_condensed };
then consider H being Subset of T such that
A4: H = F and
A5: H is open_condensed;
E /\ H is open_condensed by A3,A5,TOPS_1:69;
then G /\ F in { K where K is Subset of T : K is open_condensed } by A2
,A4;
then reconsider b = G /\ F as Element of Open_Domains_of T;
take b;
let A,B be Element of Open_Domains_of T;
assume a = [A,B];
then
A6: [A,B] = [G,F] by MCART_1:21;
then A = G by XTUPLE_0:1;
hence thesis by A6,XTUPLE_0:1;
end;
consider h being Function of D, Open_Domains_of T such that
A7: for a being Element of D holds X[a,h.a] from FUNCT_2:sch 3(A1);
take h;
let A,B be Element of Open_Domains_of T;
thus h.(A,B) = h . [A,B] .= A /\ B by A7;
end;
uniqueness
proof
deffunc U(Element of Open_Domains_of T,Element of Open_Domains_of T) = $1
/\ $2;
thus for o1,o2 being BinOp of Open_Domains_of T st (for a,b being Element
of Open_Domains_of T holds o1.(a,b) = U(a,b)) & (for a,b being Element of
Open_Domains_of T holds o2.(a,b) = U(a,b)) holds o1 = o2 from BINOP_2:sch 2;
end;
end;
notation
let T be TopSpace;
synonym OPD-Meet T for Open_Domains_Meet T;
end;
theorem Th37:
for A,B being Element of Open_Domains_of T holds (OPD-Meet T).(A
,B) = (D-Meet T).(A,B)
proof
let A,B be Element of Open_Domains_of T;
A1: A in { D where D is Subset of T : D is open_condensed };
Open_Domains_of T c= Domains_of T by Th35; then
reconsider A0 = A, B0 = B as Element of Domains_of T;
B in { E where E is Subset of T : E is open_condensed };
then consider E being Subset of T such that
A2: E = B and
A3: E is open_condensed;
consider D being Subset of T such that
A4: D = A and
A5: D is open_condensed by A1;
D /\ E is open_condensed by A5,A3,TOPS_1:69;
then A /\ B is condensed by A4,A2,TOPS_1:67;
then
A6: A /\ B c= Cl Int(A /\ B) by TOPS_1:def 6;
thus (OPD-Meet T).(A,B) = A /\ B by Def11
.= Cl(Int(A0 /\ B0)) /\ (A0 /\ B0) by A6,XBOOLE_1:28
.= (D-Meet T).(A,B) by Def3;
end;
theorem Th38:
for T being TopSpace holds LattStr(#Open_Domains_of T,OPD-Union
T,OPD-Meet T#) is B_Lattice
proof
let T be TopSpace;
set L = LattStr(#Open_Domains_of T,OPD-Union T,OPD-Meet T#);
A1: L is join-commutative
proof
let a,b be Element of L;
reconsider A = a, B = b as Element of Open_Domains_of T;
thus a"\/"b = Int(Cl(B \/ A)) by Def10
.= b"\/"a by Def10;
end;
A2: L is meet-absorbing
proof
let a,b be Element of L;
reconsider A = a, B = b as Element of Open_Domains_of T;
B in { D where D is Subset of T : D is open_condensed };
then
A3: ex D being Subset of T st D = B & D is open_condensed;
a"/\"b = A /\ B by Def11;
hence (a"/\"b)"\/"b = Int(Cl((A /\ B) \/ B)) by Def10
.= Int(Cl(B))by XBOOLE_1:22
.= b by A3,TOPS_1:def 8;
end;
A4: L is join-absorbing
proof
let a,b be Element of L;
reconsider A = a, B = b as Element of Open_Domains_of T;
A5: A c= A \/ Int Cl B by XBOOLE_1:7;
A in { D where D is Subset of T : D is open_condensed };
then ex D being Subset of T st D = A & D is open_condensed;
then
A6: A = Int Cl A by TOPS_1:def 8;
Int(Cl A \/ Cl B) = Int(Cl(A \/ B)) by PRE_TOPC:20;
then
A7: A \/ Int Cl B c= Int(Cl(A \/ B)) by A6,TOPS_1:20;
a"\/"b = Int(Cl(A \/ B)) by Def10;
hence a"/\"(a"\/"b) = A /\ Int(Cl(A \/ B)) by Def11
.= a by A5,A7,XBOOLE_1:1,28;
end;
A8: L is meet-associative
proof
let a,b,c be Element of L;
reconsider A = a, B = b, C = c as Element of Open_Domains_of T;
A9: a"/\"b = A /\ B by Def11;
b"/\"c = B /\ C by Def11;
hence a"/\"(b"/\"c) = A /\ (B /\ C) by Def11
.= (A /\ B) /\ C by XBOOLE_1:16
.= (a"/\"b)"/\"c by A9,Def11;
end;
A10: L is join-associative
proof
let a,b,c be Element of L;
reconsider A = a, B = b, C = c as Element of Open_Domains_of T;
A in { D where D is Subset of T : D is open_condensed };
then
A11: ex D being Subset of T st D = A & D is open_condensed;
B in { E where E is Subset of T : E is open_condensed };
then
A12: ex E being Subset of T st E = B & E is open_condensed;
C in { F where F is Subset of T : F is open_condensed };
then
A13: ex F being Subset of T st F = C & F is open_condensed;
A14: a"\/"b = Int(Cl(A \/ B)) by Def10;
b"\/"c = Int(Cl(B \/ C)) by Def10;
hence a"\/"(b"\/"c) = Int(Cl(A \/ (Int(Cl(B \/ C))))) by Def10
.= Int(Cl((Int(Cl(A \/ B)) \/ C))) by A11,A12,A13,Th29
.= (a"\/"b)"\/"c by A14,Def10;
end;
L is meet-commutative
proof
let a,b be Element of L;
reconsider A = a, B = b as Element of Open_Domains_of T;
thus a"/\"b = B /\ A by Def11
.= b"/\"a by Def11;
end;
then reconsider L as Lattice by A1,A10,A2,A8,A4;
A15: L is upper-bounded
proof
A16: [#] T is open_condensed by Th21;
then [#] T in { D where D is Subset of T : D is open_condensed };
then reconsider c = [#] T as Element of L;
take c;
let a be Element of L;
reconsider C = c, A = a as Element of Open_Domains_of T;
thus c"\/"a = Int(Cl(C \/ A)) by Def10
.= Int(Cl(C)) by XBOOLE_1:12
.= c by A16,TOPS_1:def 8;
hence a"\/"c = c;
end;
A17: L is distributive
proof
let a,b,c be Element of L;
reconsider A = a, B = b, C = c as Element of Open_Domains_of T;
A in { D where D is Subset of T : D is open_condensed };
then consider D being Subset of T such that
A18: D = A and
A19: D is open_condensed;
A20: D is open by A19,TOPS_1:67;
A21: a"/\"c = A /\ C by Def11;
C in { F where F is Subset of T : F is open_condensed };
then consider F being Subset of T such that
A22: F = C and
F is open_condensed;
B in { E where E is Subset of T : E is open_condensed };
then consider E being Subset of T such that
A23: E = B and
E is open_condensed;
A24: a"/\"b = A /\ B by Def11;
b"\/"c = Int(Cl(B \/ C)) by Def10;
hence a"/\"(b"\/"c) = A /\ Int(Cl(B \/ C)) by Def11
.= Int Cl A /\ Int(Cl(B \/ C)) by A18,A19,TOPS_1:def 8
.= Int(Cl(D /\ (E \/ F))) by A18,A23,A22,A20,Th7
.= Int(Cl((A /\ B) \/ (A /\ C))) by A18,A23,A22,XBOOLE_1:23
.= (a"/\"b)"\/"(a"/\"c) by A24,A21,Def10;
end;
A25: L is complemented
proof
[#] T is open_condensed by Th21;
then [#] T in { K where K is Subset of T : K is open_condensed};
then reconsider c = [#] T as Element of L;
let b be Element of L;
reconsider B = b as Element of Open_Domains_of T;
B in { D where D is Subset of T : D is open_condensed};
then consider D being Subset of T such that
A26: D = B and
A27: D is open_condensed;
A28: D is open by A27,TOPS_1:67;
D is condensed by A27,TOPS_1:67;
then Int B` is open_condensed by A26,Th16,Th25;
then Int B` in { K where K is Subset of T : K is open_condensed};
then reconsider a = Int B` as Element of L;
take a;
A29: (B`) misses B by XBOOLE_1:79;
A30: for v being Element of L holds (the L_meet of L).(c,v) = v
proof
let v be Element of L;
reconsider V = v as Element of Open_Domains_of T;
thus (the L_meet of L).(c,v) = [#] T /\ V by Def11
.= v by XBOOLE_1:28;
end;
thus a"\/"b = Int(Cl(B \/ Int B`)) by Def10
.= Int([#] T) by Th9
.= c by TOPS_1:15
.= Top L by A30,LATTICE2:17;
hence b"\/"a = Top L;
{} T is open_condensed by Th20;
then {} T in { K where K is Subset of T : K is open_condensed};
then reconsider c = {} T as Element of L;
A31: for v being Element of L holds (the L_join of L).(c,v) = v
proof
let v be Element of L;
reconsider V = v as Element of Open_Domains_of T;
V in { K where K is Subset of T : K is open_condensed};
then
A32: ex D being Subset of T st D = V & D is open_condensed;
thus (the L_join of L).(c,v) = Int(Cl({} T \/ V)) by Def10
.= Int Cl((([#]T)`) \/ (V``)) by XBOOLE_1:37
.= Int Cl([#] T /\ V`)` by XBOOLE_1:54
.= Int Cl(V``) by XBOOLE_1:28
.= v by A32,TOPS_1:def 8;
end;
thus a"/\"b = (Int B`) /\ B by Def11
.= (Int D`) /\ Int D by A26,A28,TOPS_1:23
.= Int((B`) /\ B) by A26,TOPS_1:17
.= Int {} T by A29
.= Bottom L by A31,LATTICE2:15;
hence b"/\"a = Bottom L;
end;
L is lower-bounded
proof
{} T is open_condensed by Th20;
then {} T in { D where D is Subset of T : D is open_condensed };
then reconsider c = {} T as Element of L;
take c;
let a be Element of L;
reconsider C = c, A = a as Element of Open_Domains_of T;
thus c"/\"a = C /\ A by Def11
.= c;
hence a"/\"c = c;
end;
hence thesis by A15,A25,A17;
end;
definition
let T be TopSpace;
func Open_Domains_Lattice T-> B_Lattice equals
LattStr(#Open_Domains_of T,
Open_Domains_Union T,Open_Domains_Meet T#);
coherence by Th38;
end;
begin
:: 6. Connections between Lattices of Domains.
theorem Th39:
CLD-Union T = (D-Union T)||Closed_Domains_of T
proof
A1: Closed_Domains_of T c= Domains_of T by Th31; then
reconsider F = CLD-Union T as Function of [:Closed_Domains_of T,
Closed_Domains_of T:],Domains_of T by FUNCT_2:7;
[:Closed_Domains_of T,Closed_Domains_of T:] c=
[:Domains_of T,Domains_of T:] by A1,ZFMISC_1:96; then
reconsider G = (D-Union T)||Closed_Domains_of T as Function of [:
Closed_Domains_of T,Closed_Domains_of T:],Domains_of T by FUNCT_2:32;
for A being Element of Closed_Domains_of T, B being Element of
Closed_Domains_of T holds F.(A,B) = G.(A,B)
proof
let A be Element of Closed_Domains_of T, B be Element of Closed_Domains_of
T;
thus F.(A,B) = (D-Union T).(A,B) by Th32
.= ((D-Union T)||Closed_Domains_of T). [A,B] by FUNCT_1:49
.= G.(A,B);
end;
hence thesis by BINOP_1:2;
end;
theorem Th40:
CLD-Meet T = (D-Meet T)||Closed_Domains_of T
proof
A1: Closed_Domains_of T c= Domains_of T by Th31; then
reconsider F = CLD-Meet T as Function of [:Closed_Domains_of T,
Closed_Domains_of T:],Domains_of T by FUNCT_2:7;
[:Closed_Domains_of T,Closed_Domains_of T:] c=
[:Domains_of T,Domains_of T:] by A1,ZFMISC_1:96; then
reconsider G = (D-Meet T)||Closed_Domains_of T as Function of [:
Closed_Domains_of T,Closed_Domains_of T:],Domains_of T by FUNCT_2:32;
for A being Element of Closed_Domains_of T, B being Element of
Closed_Domains_of T holds F.(A,B) = G.(A,B)
proof
let A be Element of Closed_Domains_of T, B be Element of Closed_Domains_of
T;
thus F.(A,B) = (D-Meet T).(A,B) by Th33
.= ((D-Meet T)||Closed_Domains_of T) . [A,B] by FUNCT_1:49
.= G.(A,B);
end;
hence thesis by BINOP_1:2;
end;
theorem
Closed_Domains_Lattice T is SubLattice of Domains_Lattice T
proof
set L = Domains_Lattice T, CL = Closed_Domains_Lattice T;
thus the carrier of CL c= the carrier of L by Th31;
thus the L_join of CL = (the L_join of L)||the carrier of CL by Th39;
thus thesis by Th40;
end;
theorem Th42:
OPD-Union T = (D-Union T)||Open_Domains_of T
proof
A1: Open_Domains_of T c= Domains_of T by Th35; then
reconsider F = OPD-Union T as Function of [:Open_Domains_of T,
Open_Domains_of T:],Domains_of T by FUNCT_2:7;
[:Open_Domains_of T,Open_Domains_of T:] c=
[:Domains_of T,Domains_of T:] by A1,ZFMISC_1:96; then
reconsider G = (D-Union T)||Open_Domains_of T as Function of [:
Open_Domains_of T,Open_Domains_of T:],Domains_of T by FUNCT_2:32;
for A being Element of Open_Domains_of T, B being Element of
Open_Domains_of T holds F.(A,B) = G.(A,B)
proof
let A be Element of Open_Domains_of T, B be Element of Open_Domains_of T;
thus F.(A,B) = (D-Union T).(A,B) by Th36
.= ((D-Union T)||Open_Domains_of T) . [A,B] by FUNCT_1:49
.= G.(A,B);
end;
hence thesis by BINOP_1:2;
end;
theorem Th43:
OPD-Meet T = (D-Meet T)||Open_Domains_of T
proof
A1: Open_Domains_of T c= Domains_of T by Th35; then
reconsider F = OPD-Meet T as Function of [:Open_Domains_of T,Open_Domains_of
T:],Domains_of T by FUNCT_2:7;
[:Open_Domains_of T,Open_Domains_of T:] c=
[:Domains_of T,Domains_of T:] by A1,ZFMISC_1:96; then
reconsider G = (D-Meet T)||Open_Domains_of T as Function of [:
Open_Domains_of T,Open_Domains_of T:],Domains_of T by FUNCT_2:32;
for A being Element of Open_Domains_of T, B being Element of
Open_Domains_of T holds F.(A,B) = G.(A,B)
proof
let A be Element of Open_Domains_of T, B be Element of Open_Domains_of T;
thus F.(A,B) = (D-Meet T).(A,B) by Th37
.= ((D-Meet T)||Open_Domains_of T) . [A,B] by FUNCT_1:49
.= G.(A,B);
end;
hence thesis by BINOP_1:2;
end;
theorem
Open_Domains_Lattice T is SubLattice of Domains_Lattice T
proof
set L = Domains_Lattice T, OL = Open_Domains_Lattice T;
thus the carrier of OL c= the carrier of L by Th35;
thus the L_join of OL = (the L_join of L)||the carrier of OL by Th42;
thus thesis by Th43;
end;