:: Completeness of the Lattices of Domains of a Topological Space
:: by Zbigniew Karno and Toshihiko Watanabe
::
:: Received July 16, 1992
:: Copyright (c) 1992-2026 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, TOPS_1, TARSKI, RCOMP_1, XBOOLE_0, SETFAM_1,
PCOMPS_1, ZFMISC_1, STRUCT_0, FINSET_1, FINSEQ_1, RELAT_1, NAT_1,
XXREAL_0, ARYTM_3, CARD_1, FUNCT_1, TDLAT_1, LATTICES, EQREL_1, PBOOLE,
LATTICE3, REWRITE1, TDLAT_2;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, SETFAM_1, STRUCT_0, FUNCT_1,
ORDINAL1, NUMBERS, FINSET_1, FINSEQ_1, XCMPLX_0, NAT_1, PRE_TOPC, TOPS_1,
TOPS_2, PCOMPS_1, BINOP_1, LATTICES, LATTICE3, TDLAT_1, XXREAL_0;
constructors SETFAM_1, XXREAL_0, NAT_1, MEMBERED, FINSEQ_1, TOPS_1, TOPS_2,
PCOMPS_1, LATTICE3, TDLAT_1, BINOP_1;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, TOPS_1, TDLAT_1,
XREAL_0, FINSEQ_1, RELAT_1, ORDINAL1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, LATTICE3;
equalities RELAT_1, STRUCT_0;
expansions TARSKI, LATTICE3;
theorems TARSKI, ZFMISC_1, SETFAM_1, FINSEQ_1, FUNCT_1, NAT_1, PRE_TOPC,
TOPS_1, TOPS_2, PCOMPS_1, LATTICES, LATTICE2, LATTICE3, TDLAT_1, RELAT_1,
XBOOLE_0, XBOOLE_1, XREAL_1;
schemes SUBSET_1, NAT_1;
begin
:: 1. Preliminary Theorems about Subsets of a Toplogical Space.
reserve T for TopSpace;
theorem Th1:
for A being Subset of T holds Int Cl Int A c= Int Cl A & Int Cl
Int A c= Cl Int A
proof
let A be Subset of T;
Cl Int A c= Cl A by PRE_TOPC:19,TOPS_1:16;
hence Int Cl Int A c= Int Cl A by TOPS_1:19;
thus thesis by TOPS_1:16;
end;
theorem Th2:
for A being Subset of T holds Cl Int A c= Cl Int Cl A & Int Cl A
c= Cl Int Cl A
proof
let A be Subset of T;
Int A c= Int Cl A by PRE_TOPC:18,TOPS_1:19;
hence Cl Int A c= Cl Int Cl A by PRE_TOPC:19;
thus thesis by PRE_TOPC:18;
end;
theorem
for A, B being Subset of T st B is closed holds Cl(Int(A /\ B)) = A
implies A c= B
proof
let A, B be Subset of T;
assume
A1: B is closed;
A2: A /\ B c= B by XBOOLE_1:17;
Int(A /\ B) c= A /\ B by TOPS_1:16;
then Int(A /\ B) c= B by A2;
then
A3: Cl Int(A /\ B) c= Cl B by PRE_TOPC:19;
assume Cl(Int(A /\ B)) = A;
hence thesis by A1,A3,PRE_TOPC:22;
end;
theorem Th4:
for A, B being Subset of T st A is open holds Int(Cl(A \/ B)) = B
implies A c= B
proof
let A, B be Subset of T;
assume
A1: A is open;
A2: A c= A \/ B by XBOOLE_1:7;
A \/ B c= Cl(A \/ B) by PRE_TOPC:18;
then A c= Cl(A \/ B) by A2;
then
A3: Int A c= Int Cl(A \/ B) by TOPS_1:19;
assume Int(Cl(A \/ B)) = B;
hence thesis by A1,A3,TOPS_1:23;
end;
theorem Th5:
for A being Subset of T st A c= Cl Int A holds A \/ Int Cl A c=
Cl Int(A \/ Int Cl A)
proof
let A be Subset of T;
assume
A1: A c= Cl Int A;
A2: Int Cl A c= Cl Int Cl A by PRE_TOPC:18;
A3: Int A c= Int Cl A by PRE_TOPC:18,TOPS_1:19;
then Cl(Int A) c= Cl(Int Cl A) by PRE_TOPC:19;
then A c= Cl(Int Cl A) by A1;
then A \/ Int Cl A c= (Cl Int Cl A) \/ (Cl Int Cl A) by A2,XBOOLE_1:13;
then
A4: A \/ Int Cl A c= Cl((Int A) \/ (Int Cl A)) by A3,XBOOLE_1:12;
(Int A) \/ (Int Int Cl A) c= Int (A \/ Int Cl A) by TOPS_1:20;
then Cl((Int A) \/ (Int Cl A)) c= Cl(Int (A \/ Int Cl A)) by PRE_TOPC:19;
hence thesis by A4;
end;
theorem Th6:
for A being Subset of T st Int Cl A c= A holds Int Cl(A /\ Cl Int
A) c= A /\ Cl Int A
proof
let A be Subset of T;
assume
A1: Int Cl A c= A;
A2: Int Cl Int A c= Cl Int A by TOPS_1:16;
A3: Cl Int A c= Cl A by PRE_TOPC:19,TOPS_1:16;
then Int(Cl Int A) c= Int(Cl A) by TOPS_1:19;
then Int Cl Int A c= A by A1;
then (Int Cl Int A) /\ (Int Cl Int A) c= A /\ Cl Int A by A2,XBOOLE_1:27;
then
A4: Int((Cl A) /\ (Cl Int A)) c= A /\ Cl Int A by A3,XBOOLE_1:28;
Cl (A /\ Cl Int A) c= (Cl A) /\ (Cl Cl Int A) by PRE_TOPC:21;
then Int(Cl (A /\ Cl Int A)) c= Int((Cl A) /\ (Cl Int A)) by TOPS_1:19;
hence thesis by A4;
end;
begin
:: 2. The Closure and the Interior Operations for Families of Subsets of
:: a Topological Space.
::(for the definition of clf see PCOMPS_1:def 3)
notation
let T;
let F be Subset-Family of T;
synonym Cl F for clf F;
end;
::Properties of the Closure Operation Cl (see also PCOMPS_1).
theorem Th7:
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}
proof
let F be Subset-Family of T;
set P = {A where A is Subset of T : ex B being Subset of T st A = Cl B & B
in F};
now
let C be object;
assume C in P;
then
ex A being Subset of T st C = A & ex B being Subset of T st A = Cl B &
B in F;
hence C in bool the carrier of T;
end;
then reconsider P as Subset-Family of T by TARSKI:def 3;
reconsider P as Subset-Family of T;
for X being object holds X in Cl F iff X in P
proof
let X be object;
A1: now
assume
A2: X in P;
then reconsider C = X as Subset of T;
ex D being Subset of T st D = C & ex B being Subset of T st D = Cl
B & B in F by A2;
hence X in Cl F by PCOMPS_1:def 2;
end;
now
assume
A3: X in Cl F;
then reconsider C = X as Subset of T;
ex B being Subset of T st C = Cl B & B in F by A3,PCOMPS_1:def 2;
hence X in P;
end;
hence thesis by A1;
end;
hence thesis by TARSKI:2;
end;
theorem
for F being Subset-Family of T holds Cl F = Cl Cl F
proof
let F be Subset-Family of T;
A1: Cl Cl F = {D where D is Subset of T : ex B being Subset of T st D = Cl B
& B in Cl F} by Th7;
A2: Cl F = {A where A is Subset of T : ex B being Subset of T st A = Cl B &
B in F} by Th7;
for X being object holds X in Cl F iff X in Cl Cl F
proof
let X be object;
A3: now
assume
A4: X in Cl F;
then reconsider C = X as Subset of T;
consider B being Subset of T such that
A5: C = Cl B and
A6: B in F by A4,PCOMPS_1:def 2;
A7: Cl B in Cl F by A6,PCOMPS_1:def 2;
C = Cl Cl B by A5;
hence X in Cl Cl F by A1,A7;
end;
now
assume
A8: X in Cl Cl F;
then reconsider C = X as Subset of T;
ex Q being Subset of T st Q = C & ex B being Subset of T st Q = Cl
B & B in Cl F by A1,A8;
then consider B being Subset of T such that
A9: C = Cl B and
A10: B in Cl F;
ex Q being Subset of T st Q = B & ex R being Subset of T st Q = Cl
R & R in F by A2,A10;
hence X in Cl F by A9,PCOMPS_1:def 2;
end;
hence thesis by A3;
end;
hence thesis by TARSKI:2;
end;
theorem Th9:
for F being Subset-Family of T holds F = {} iff Cl F = {}
proof
let F be Subset-Family of T;
thus F = {} implies Cl F = {} by PCOMPS_1:12;
assume
A1: Cl F = {};
set B = the Element of F;
assume
A2: F <> {};
then reconsider B as Subset of T by TARSKI:def 3;
Cl B in Cl F by A2,PCOMPS_1:def 2;
hence contradiction by A1;
end;
theorem
for F,G being Subset-Family of T holds Cl(F /\ G) c= (Cl F) /\ (Cl G)
proof
let F,G be Subset-Family of T;
for X being object holds X in Cl(F /\ G) implies X in (Cl F) /\ (Cl G)
proof
let X be object;
assume
A1: X in Cl(F /\ G);
then reconsider X0 = X as Subset of T;
consider W being Subset of T such that
A2: X0 = Cl W and
A3: W in F /\ G by A1,PCOMPS_1:def 2;
W in G by A3,XBOOLE_0:def 4;
then
A4: X0 in Cl G by A2,PCOMPS_1:def 2;
W in F by A3,XBOOLE_0:def 4;
then X0 in Cl F by A2,PCOMPS_1:def 2;
hence thesis by A4,XBOOLE_0:def 4;
end;
hence thesis;
end;
theorem
for F,G being Subset-Family of T holds (Cl F) \ (Cl G) c= Cl(F \ G)
proof
let F,G be Subset-Family of T;
for X being object holds X in (Cl F) \ (Cl G) implies X in Cl(F \ G)
proof
let X be object;
assume
A1: X in (Cl F) \ (Cl G);
then reconsider X0 = X as Subset of T;
X in Cl F by A1,XBOOLE_0:def 5;
then consider W being Subset of T such that
A2: X0 = Cl W and
A3: W in F by PCOMPS_1:def 2;
not X in Cl G by A1,XBOOLE_0:def 5;
then not W in G by A2,PCOMPS_1:def 2;
then W in F \ G by A3,XBOOLE_0:def 5;
hence thesis by A2,PCOMPS_1:def 2;
end;
hence thesis;
end;
theorem
for F being Subset-Family of T, A being Subset of T st A in F holds
meet(Cl F) c= Cl A & Cl A c= union(Cl F)
proof
let F be Subset-Family of T, A be Subset of T;
assume A in F;
then
Cl A in {P where P is Subset of T : ex B being Subset of T st P = Cl B &
B in F};
then
A1: Cl A in Cl F by Th7;
hence meet(Cl F) c= Cl A by SETFAM_1:3;
thus thesis by A1,ZFMISC_1:74;
end;
::for F being Subset-Family of T holds union F c= union(Cl F);
::(see PCOMPS_1:22)
theorem Th13:
for F being Subset-Family of T holds meet F c= meet(Cl F)
proof
let F be Subset-Family of T;
A1: for A being set st A in Cl F holds meet F c= A
proof
let A be set;
assume
A2: A in Cl F;
then reconsider A0 = A as Subset of T;
consider B being Subset of T such that
A3: A0 = Cl B and
A4: B in F by A2,PCOMPS_1:def 2;
A5: B c= A0 by A3,PRE_TOPC:18;
meet F c= B by A4,SETFAM_1:3;
hence thesis by A5;
end;
now
per cases;
suppose
Cl F = {};
hence thesis by Th9;
end;
suppose
Cl F <> {};
hence thesis by A1,SETFAM_1:5;
end;
end;
hence thesis;
end;
theorem Th14:
for F being Subset-Family of T holds Cl(meet F) c= meet(Cl F)
proof
let F be Subset-Family of T;
A1: meet(Cl F) is closed by PCOMPS_1:11,TOPS_2:22;
Cl meet F c= Cl meet(Cl F) by Th13,PRE_TOPC:19;
hence thesis by A1,PRE_TOPC:22;
end;
theorem Th15:
for F being Subset-Family of T holds union(Cl F) c= Cl(union F)
proof
let F be Subset-Family of T;
for A being set st A in Cl F holds A c= Cl(union F)
proof
let A be set;
assume
A1: A in Cl F;
then reconsider A0 = A as Subset of T;
ex B being Subset of T st A0 = Cl B & B in F by A1,PCOMPS_1:def 2;
hence thesis by PRE_TOPC:19,ZFMISC_1:74;
end;
hence thesis by ZFMISC_1:76;
end;
definition
let T;
let F be Subset-Family of T;
func Int F -> Subset-Family of T means
:Def1:
for A being Subset of T holds
A in it iff ex B being Subset of T st A = Int B & B in F;
existence
proof
defpred X[Subset of T] means ex B being Subset of T st $1 = Int B & B in F;
thus ex F being Subset-Family of T st for A being Subset of T holds A in F
iff X[A] from SUBSET_1:sch 3;
end;
uniqueness
proof
let H,G be Subset-Family of T;
assume
A1: for A being Subset of T holds A in H iff ex B being Subset of T st
A = Int B & B in F;
assume
A2: for A being Subset of T holds A in G iff ex B being Subset of T st
A = Int B & B in F;
now
let A be object;
assume
A3: A in G;
then reconsider A0 = A as Subset of T;
ex B being Subset of T st A0 = Int B & B in F by A2,A3;
hence A in H by A1;
end;
then
A4: G c= H;
now
let A be object;
assume
A5: A in H;
then reconsider A0 = A as Subset of T;
ex B being Subset of T st A0 = Int B & B in F by A1,A5;
hence A in G by A2;
end;
then H c= G;
hence thesis by A4,XBOOLE_0:def 10;
end;
projectivity
proof let G,F be Subset-Family of T such that
A6: for A being Subset of T holds
A in G iff ex B being Subset of T st A = Int B & B in F;
let A being Subset of T;
thus A in G implies ex B being Subset of T st A = Int B & B in G
proof
assume A in G;
then consider B being Subset of T such that
A7: A = Int B and
A8: B in F by A6;
take C = Int B;
thus A = Int C by A7;
thus C in G by A8,A6;
end;
given B being Subset of T such that
A9: A = Int B and
A10: B in G;
consider C being Subset of T such that
A11: B = Int C and
C in F by A10,A6;
A = B by A9,A11;
hence A in G by A10;
end;
end;
::Properties of the Interior Operation Int.
theorem Th16:
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}
proof
let F be Subset-Family of T;
set P = {A where A is Subset of T : ex B being Subset of T st A = Int B & B
in F};
now
let C be object;
assume C in P;
then
ex A being Subset of T st C = A & ex B being Subset of T st A = Int B
& B in F;
hence C in bool the carrier of T;
end;
then reconsider P as Subset-Family of T by TARSKI:def 3;
reconsider P as Subset-Family of T;
for X being object holds X in Int F iff X in P
proof
let X be object;
A1: now
assume
A2: X in P;
then reconsider C = X as Subset of T;
ex D being Subset of T st D = C & ex B being Subset of T st D = Int
B & B in F by A2;
hence X in Int F by Def1;
end;
now
assume
A3: X in Int F;
then reconsider C = X as Subset of T;
ex B being Subset of T st C = Int B & B in F by A3,Def1;
hence X in P;
end;
hence thesis by A1;
end;
hence thesis by TARSKI:2;
end;
::$CT
theorem Th17:
for F being Subset-Family of T holds Int F is open
proof
let F be Subset-Family of T;
now
let A be Subset of T;
assume A in Int F;
then ex B being Subset of T st A = Int B & B in F by Def1;
hence A is open;
end;
hence thesis by TOPS_2:def 1;
end;
theorem Th18:
for F being Subset-Family of T holds F = {} iff Int F = {}
proof
let F be Subset-Family of T;
thus F = {} implies Int F = {}
proof
set A = the Element of Int F;
assume
A1: F = {};
assume
A2: not thesis;
then reconsider A as Subset of T by TARSKI:def 3;
ex V being Subset of T st A = Int V & V in F by A2,Def1;
hence contradiction by A1;
end;
thus Int F = {} implies F = {}
proof
set B = the Element of F;
assume
A3: Int F = {};
assume
A4: not thesis;
then reconsider B as Subset of T by TARSKI:def 3;
reconsider A = Int B as set;
ex A be set st A in Int F
proof
take A;
thus thesis by A4,Def1;
end;
hence contradiction by A3;
end;
end;
theorem Th19:
for A being Subset of T, F being Subset-Family of T st F = { A }
holds Int F = { Int A }
proof
let A be Subset of T, F be Subset-Family of T;
reconsider C = Int F as set;
assume
A1: F = { A };
for B being object holds B in C iff B = Int A
proof
let B be object;
A2: now
assume
A3: B = Int A;
ex M being Subset of T st B = Int M & M in F
proof
take A;
thus thesis by A1,A3,TARSKI:def 1;
end;
hence B in C by Def1;
end;
now
assume
A4: B in C;
then reconsider B0 = B as Subset of T;
ex M being Subset of T st B0 = Int M & M in F by A4,Def1;
hence B = Int A by A1,TARSKI:def 1;
end;
hence thesis by A2;
end;
hence thesis by TARSKI:def 1;
end;
theorem
for F,G being Subset-Family of T holds F c= G implies Int F c= Int G
proof
let F,G be Subset-Family of T;
reconsider F0 = Int F, G0 = Int G as set;
assume
A1: F c= G;
now
let X be object;
assume
A2: X in F0;
then reconsider X0 = X as Subset of T;
ex V being Subset of T st X0 = Int V & V in F by A2,Def1;
hence X in G0 by A1,Def1;
end;
hence thesis;
end;
theorem Th21:
for F,G being Subset-Family of T holds Int(F \/ G) = (Int F) \/ (Int G)
proof
let F,G be Subset-Family of T;
for X being object holds X in Int(F \/ G) iff X in (Int F) \/ (Int G)
proof
let X be object;
A1: now
assume
A2: X in (Int F) \/ (Int G);
now
per cases by A2,XBOOLE_0:def 3;
suppose
A3: X in Int F;
then reconsider X0 = X as Subset of T;
ex W being Subset of T st X0 = Int W & W in (F \/ G)
proof
consider Z being Subset of T such that
A4: X0 = Int Z and
A5: Z in F by A3,Def1;
take Z;
thus thesis by A4,A5,XBOOLE_0:def 3;
end;
hence X in Int(F \/ G) by Def1;
end;
suppose
A6: X in Int G;
then reconsider X0 = X as Subset of T;
ex W being Subset of T st X0 = Int W & W in (F \/ G)
proof
consider Z being Subset of T such that
A7: X0 = Int Z and
A8: Z in G by A6,Def1;
take Z;
thus thesis by A7,A8,XBOOLE_0:def 3;
end;
hence X in Int(F \/ G) by Def1;
end;
end;
hence X in Int(F \/ G);
end;
now
assume
A9: X in Int(F \/ G);
then reconsider X0 = X as Subset of T;
consider W being Subset of T such that
A10: X0 = Int W and
A11: W in (F \/ G) by A9,Def1;
now
per cases by A11,XBOOLE_0:def 3;
suppose
W in F;
then X0 in Int F by A10,Def1;
hence X0 in (Int F) \/ (Int G) by XBOOLE_0:def 3;
end;
suppose
W in G;
then X0 in Int G by A10,Def1;
hence X0 in (Int F) \/ (Int G) by XBOOLE_0:def 3;
end;
end;
hence X in (Int F) \/ (Int G);
end;
hence thesis by A1;
end;
hence thesis by TARSKI:2;
end;
theorem
for F,G being Subset-Family of T holds Int(F /\ G) c= (Int F) /\ (Int G)
proof
let F,G be Subset-Family of T;
for X being object holds X in Int(F /\ G) implies X in (Int F) /\ (Int G)
proof
let X be object;
assume
A1: X in Int(F /\ G);
then reconsider X0 = X as Subset of T;
consider W being Subset of T such that
A2: X0 = Int W and
A3: W in (F /\ G) by A1,Def1;
W in G by A3,XBOOLE_0:def 4;
then
A4: X0 in Int G by A2,Def1;
W in F by A3,XBOOLE_0:def 4;
then X0 in Int F by A2,Def1;
hence thesis by A4,XBOOLE_0:def 4;
end;
hence thesis;
end;
theorem
for F,G being Subset-Family of T holds (Int F) \ (Int G) c= Int(F \ G)
proof
let F,G be Subset-Family of T;
for X being object holds X in (Int F) \ (Int G) implies X in Int(F \ G)
proof
let X be object;
assume
A1: X in (Int F) \ (Int G);
then reconsider X0 = X as Subset of T;
X in Int F by A1,XBOOLE_0:def 5;
then consider W being Subset of T such that
A2: X0 = Int W and
A3: W in F by Def1;
not X in Int G by A1,XBOOLE_0:def 5;
then not W in G by A2,Def1;
then W in F \ G by A3,XBOOLE_0:def 5;
hence thesis by A2,Def1;
end;
hence thesis;
end;
theorem
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
proof
let F be Subset-Family of T, A be Subset of T;
assume A in F;
then
Int A in {P where P is Subset of T : ex B being Subset of T st P = Int B
& B in F};
then
A1: Int A in Int F by Th16;
hence Int A c= union(Int F) by ZFMISC_1:74;
thus thesis by A1,SETFAM_1:3;
end;
theorem Th25:
for F being Subset-Family of T holds union(Int F) c= union F
proof
let F be Subset-Family of T;
now
let x be object;
assume x in union(Int F);
then consider A being set such that
A1: x in A and
A2: A in Int F by TARSKI:def 4;
reconsider A as Subset of T by A2;
consider B being Subset of T such that
A3: A = Int B and
A4: B in F by A2,Def1;
ex B being set st x in B & B in F
proof
take B;
Int B c= B by TOPS_1:16;
hence thesis by A1,A3,A4;
end;
hence x in union F by TARSKI:def 4;
end;
hence thesis;
end;
theorem
for F being Subset-Family of T holds meet(Int F) c= meet F
proof
let F be Subset-Family of T;
A1: for A being set st A in F holds meet(Int F) c= A
proof
let A be set;
assume
A2: A in F;
then reconsider A0 = A as Subset of T;
set C = Int A0;
C in {P where P is Subset of T : ex Q being Subset of T st P = Int Q &
Q in F} by A2;
then C in Int F by Th16;
then
A3: meet(Int F) c= C by SETFAM_1:3;
C c= A0 by TOPS_1:16;
hence thesis by A3;
end;
now
per cases;
suppose
F = {};
hence thesis by Th18;
end;
suppose
F <> {};
hence thesis by A1,SETFAM_1:5;
end;
end;
hence thesis;
end;
theorem Th27:
for F being Subset-Family of T holds union(Int F) c= Int(union F )
proof
let F be Subset-Family of T;
A1: Int union(Int F) c= Int(union F) by Th25,TOPS_1:19;
union(Int F) is open by Th17,TOPS_2:19;
hence thesis by A1,TOPS_1:23;
end;
theorem Th28:
for F being Subset-Family of T holds Int(meet F) c= meet(Int F)
proof
let F be Subset-Family of T;
A1: for A being set st A in Int F holds Int(meet F) c= A
proof
let A be set;
assume
A2: A in Int F;
then reconsider A0 = A as Subset of T;
A0 in {B where B is Subset of T : ex C being Subset of T st B = Int C
& C in F} by A2,Th16;
then
ex P being Subset of T st P = A0 & ex C being Subset of T st P = Int
C & C in F;
hence thesis by SETFAM_1:3,TOPS_1:19;
end;
now
per cases;
suppose
Int F = {};
then meet F = {}T by Th18,SETFAM_1:1;
hence thesis;
end;
suppose
Int F <> {};
hence thesis by A1,SETFAM_1:5;
end;
end;
hence thesis;
end;
theorem
for F being Subset-Family of T holds F is finite implies Int(meet F) =
meet(Int F)
proof
let F be Subset-Family of T;
assume
A1: F is finite;
A2: meet(Int F) c= Int(meet F)
proof
consider p being FinSequence such that
A3: rng p = F by A1,FINSEQ_1:52;
consider n being Nat such that
A4: dom p = Seg n by FINSEQ_1:def 2;
defpred X[Nat] means for G being Subset-Family of T st G = p.:(Seg $1) &
$1 <= n & 1 <= n holds meet(Int G) c= Int(meet G);
A5: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat;
assume
A6: for G being Subset-Family of T st G = p.:(Seg k) & k <= n & 1 <=
n holds meet(Int G) c= Int(meet G);
let G be Subset-Family of T;
assume
A7: G = p.:(Seg(k + 1));
assume that
A8: k + 1 <= n and
A9: 1 <= n;
A10: now
reconsider G2 = Im(p,k + 1) as Subset-Family of T by A3,RELAT_1:111
,TOPS_2:2;
reconsider G1 = p.:(Seg k) as Subset-Family of T by A3,RELAT_1:111
,TOPS_2:2;
A11: 0 + 1 = 1;
0 <= k by NAT_1:2;
then 1 <= k + 1 by A11,XREAL_1:7;
then
A12: k + 1 in dom p by A4,A8,FINSEQ_1:1;
then
A13: G2 = {p.(k + 1)} by FUNCT_1:59;
then meet G2 = p.(k + 1) by SETFAM_1:10;
then reconsider G3 = p.(k + 1) as Subset of T;
A14: meet(Int G2) = meet {Int G3} by A13,Th19
.= Int G3 by SETFAM_1:10
.= Int(meet G2) by A13,SETFAM_1:10;
k + 1 <= n + 1 by A8,NAT_1:12;
then k <= n by XREAL_1:6;
then
A15: meet(Int G1) c= Int(meet G1) by A6,A9;
assume 0 < k;
then
A16: 0 + 1 <= k by NAT_1:13;
then
A17: k in Seg k by FINSEQ_1:1;
k <= n by A8,NAT_1:13;
then k in dom p by A4,A16,FINSEQ_1:1;
then
A18: p.k in G1 by A17,FUNCT_1:def 6;
k + 1 in {k + 1} by TARSKI:def 1;
then
A19: p.(k + 1) in G2 by A12,FUNCT_1:def 6;
then
A20: Int G2 <> {} by Th18;
A21: p.:(Seg(k + 1)) = p.:(Seg k \/ {k + 1}) by FINSEQ_1:9
.= p.:(Seg k) \/ p.:{k + 1} by RELAT_1:120;
then Int(meet G) = Int((meet G1) /\ (meet G2)) by A7,A18,A19,SETFAM_1:9
.= Int(meet G1) /\ Int(meet G2) by TOPS_1:17;
then
A22: meet(Int G1) /\ meet(Int G2) c= Int(meet G) by A14,A15,XBOOLE_1:27;
Int G1 <> {} by A18,Th18;
then meet((Int G1) \/ (Int G2)) c= Int(meet G) by A20,A22,SETFAM_1:9;
hence thesis by A7,A21,Th21;
end;
now
assume
A23: k = 0;
then 1 in dom p by A4,A8,FINSEQ_1:1;
then
A24: Im(p,1) = {p.1} by FUNCT_1:59;
then union G = p.1 by A7,A23,FINSEQ_1:2,ZFMISC_1:25;
then reconsider G1 = p.1 as Subset of T;
Int(meet G) = Int G1 by A7,A23,A24,FINSEQ_1:2,SETFAM_1:10
.= meet {Int G1} by SETFAM_1:10
.= meet(Int G) by A7,A23,A24,Th19,FINSEQ_1:2;
hence thesis;
end;
hence thesis by A10,NAT_1:3;
end;
A25: X[ 0 ] by Th18,SETFAM_1:1;
A26: for k being Nat holds X[k] from NAT_1:sch 2(A25,A5);
A27: now
assume
A28: 1 <= n;
F = p.:(Seg n) by A3,A4,RELAT_1:113;
hence thesis by A26,A28;
end;
A29: now
assume n <> 0;
then
A30: 0 < n by NAT_1:3;
1 = 0 + 1;
hence 1 <= n by A30,NAT_1:13;
end;
now
assume n = 0;
then Seg n = {};
then F = p.:{} by A3,A4,RELAT_1:113;
then F = {};
hence thesis by Th18,SETFAM_1:1;
end;
hence thesis by A27,A29;
end;
Int(meet F) c= meet(Int F) by Th28;
hence thesis by A2,XBOOLE_0:def 10;
end;
::Connections between the Operations Int and Cl.
reserve T for non empty TopSpace;
reserve F for Subset-Family of T;
theorem Th30:
Cl Int F = {A where A is Subset of T : ex B being Subset of T st
A = Cl Int B & B in F}
proof
set P = {A where A is Subset of T : ex B being Subset of T st A = Cl Int B &
B in F};
now
let C be object;
assume C in P;
then
ex A being Subset of T st C = A & ex B being Subset of T st A = Cl Int
B & B in F;
hence C in bool the carrier of T;
end;
then reconsider P as Subset-Family of T by TARSKI:def 3;
reconsider P as Subset-Family of T;
for X being object holds X in Cl Int F iff X in P
proof
let X be object;
A1: now
assume
A2: X in P;
then reconsider C = X as Subset of T;
ex D being Subset of T st D = C & ex B being Subset of T st D = Cl
Int B & B in F by A2;
then consider B being Subset of T such that
A3: C = Cl Int B and
A4: B in F;
Int B in Int F by A4,Def1;
hence X in Cl Int F by A3,PCOMPS_1:def 2;
end;
now
assume
A5: X in Cl Int F;
then reconsider C = X as Subset of T;
consider B being Subset of T such that
A6: C = Cl B and
A7: B in Int F by A5,PCOMPS_1:def 2;
ex D being Subset of T st B = Int D & D in F by A7,Def1;
hence X in P by A6;
end;
hence thesis by A1;
end;
hence thesis by TARSKI:2;
end;
theorem Th31:
Int Cl F = {A where A is Subset of T : ex B being Subset of T st
A = Int Cl B & B in F}
proof
set P = {A where A is Subset of T : ex B being Subset of T st A = Int Cl B &
B in F};
now
let C be object;
assume C in P;
then
ex A being Subset of T st C = A & ex B being Subset of T st A = Int Cl
B & B in F;
hence C in bool the carrier of T;
end;
then reconsider P as Subset-Family of T by TARSKI:def 3;
reconsider P as Subset-Family of T;
for X being object holds X in Int Cl F iff X in P
proof
let X be object;
A1: now
assume
A2: X in P;
then reconsider C = X as Subset of T;
ex D being Subset of T st D = C & ex B being Subset of T st D = Int
Cl B & B in F by A2;
then consider B being Subset of T such that
A3: C = Int Cl B and
A4: B in F;
Cl B in Cl F by A4,PCOMPS_1:def 2;
hence X in Int Cl F by A3,Def1;
end;
now
assume
A5: X in Int Cl F;
then reconsider C = X as Subset of T;
consider B being Subset of T such that
A6: C = Int B and
A7: B in Cl F by A5,Def1;
ex D being Subset of T st B = Cl D & D in F by A7,PCOMPS_1:def 2;
hence X in P by A6;
end;
hence thesis by A1;
end;
hence thesis by TARSKI:2;
end;
theorem Th32:
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}
proof
set P = {A where A is Subset of T : ex B being Subset of T st A = Cl Int Cl
B & B in F};
now
let C be object;
assume C in P;
then
ex A being Subset of T st C = A & ex B being Subset of T st A = Cl Int
Cl B & B in F;
hence C in bool the carrier of T;
end;
then reconsider P as Subset-Family of T by TARSKI:def 3;
reconsider P as Subset-Family of T;
for X being object holds X in Cl Int Cl F iff X in P
proof
let X be object;
A1: now
assume
A2: X in P;
then reconsider C = X as Subset of T;
ex D being Subset of T st D = C & ex B being Subset of T st D = Cl
Int Cl B & B in F by A2;
then consider B being Subset of T such that
A3: C = Cl Int Cl B and
A4: B in F;
Cl B in Cl F by A4,PCOMPS_1:def 2;
then Int Cl B in Int Cl F by Def1;
hence X in Cl Int Cl F by A3,PCOMPS_1:def 2;
end;
now
assume
A5: X in Cl Int Cl F;
then reconsider C = X as Subset of T;
consider B being Subset of T such that
A6: C = Cl B and
A7: B in Int Cl F by A5,PCOMPS_1:def 2;
consider D being Subset of T such that
A8: B = Int D and
A9: D in Cl F by A7,Def1;
ex E being Subset of T st D = Cl E & E in F by A9,PCOMPS_1:def 2;
hence X in P by A6,A8;
end;
hence thesis by A1;
end;
hence thesis by TARSKI:2;
end;
theorem Th33:
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}
proof
set P = {A where A is Subset of T : ex B being Subset of T st A = Int Cl Int
B & B in F};
now
let C be object;
assume C in P;
then
ex A being Subset of T st C = A & ex B being Subset of T st A = Int Cl
Int B & B in F;
hence C in bool the carrier of T;
end;
then reconsider P as Subset-Family of T by TARSKI:def 3;
reconsider P as Subset-Family of T;
for X being object holds X in Int Cl Int F iff X in P
proof
let X be object;
A1: now
assume
A2: X in P;
then reconsider C = X as Subset of T;
ex D being Subset of T st D = C & ex B being Subset of T st D = Int
Cl Int B & B in F by A2;
then consider B being Subset of T such that
A3: C = Int Cl Int B and
A4: B in F;
Int B in Int F by A4,Def1;
then Cl Int B in Cl Int F by PCOMPS_1:def 2;
hence X in Int Cl Int F by A3,Def1;
end;
now
assume
A5: X in Int Cl Int F;
then reconsider C = X as Subset of T;
consider B being Subset of T such that
A6: C = Int B and
A7: B in Cl Int F by A5,Def1;
consider D being Subset of T such that
A8: B = Cl D and
A9: D in Int F by A7,PCOMPS_1:def 2;
ex E being Subset of T st D = Int E & E in F by A9,Def1;
hence X in P by A6,A8;
end;
hence thesis by A1;
end;
hence thesis by TARSKI:2;
end;
theorem
Cl Int Cl Int F = Cl Int F
proof
set H = {A where A is Subset of T : ex B being Subset of T st A = Int Cl Int
B & B in F};
Int Cl Int F = H by Th33;
then reconsider H as Subset-Family of T;
A1: Cl Int Cl Int F = Cl H by Th33;
A2: Cl Int F = {A where A is Subset of T : ex B being Subset of T st A = Cl
Int B & B in F} by Th30;
for X being object holds X in Cl Int Cl Int F iff X in Cl Int F
proof
let X be object;
A3: now
assume
A4: X in Cl Int F;
then reconsider C = X as Subset of T;
ex D being Subset of T st D = C & ex B being Subset of T st D = Cl
Int B & B in F by A2,A4;
then consider B being Subset of T such that
A5: C = Cl Int B and
A6: B in F;
Int B in Int F by A6,Def1;
then Cl Int B in Cl Int F by PCOMPS_1:def 2;
then
A7: Int Cl Int B in Int Cl Int F by Def1;
C = Cl Int Cl Int B by A5,TOPS_1:26;
hence X in Cl Int Cl Int F by A7,PCOMPS_1:def 2;
end;
now
assume
A8: X in Cl Int Cl Int F;
then reconsider C = X as Subset of T;
consider B being Subset of T such that
A9: C = Cl B and
A10: B in {A where A is Subset of T : ex B being Subset of T st A =
Int Cl Int B & B in F} by A1,A8,PCOMPS_1:def 2;
ex S being Subset of T st S = B & ex R being Subset of T st S = Int
Cl Int R & R in F by A10;
then consider D being Subset of T such that
A11: B = Int Cl Int D and
A12: D in F;
A13: Int D in Int F by A12,Def1;
C = Cl Int D by A9,A11,TOPS_1:26;
hence X in Cl Int F by A13,PCOMPS_1:def 2;
end;
hence thesis by A3;
end;
hence thesis by TARSKI:2;
end;
theorem
Int Cl Int Cl F = Int Cl F
proof
set H = {A where A is Subset of T : ex B being Subset of T st A = Cl Int Cl
B & B in F};
Cl Int Cl F = H by Th32;
then reconsider H as Subset-Family of T;
A1: Int Cl Int Cl F = Int H by Th32;
A2: Int Cl F = {A where A is Subset of T : ex B being Subset of T st A = Int
Cl B & B in F} by Th31;
for X being object holds X in Int Cl Int Cl F iff X in Int Cl F
proof
let X be object;
A3: now
assume
A4: X in Int Cl F;
then reconsider C = X as Subset of T;
ex D being Subset of T st D = C & ex B being Subset of T st D = Int
Cl B & B in F by A2,A4;
then consider B being Subset of T such that
A5: C = Int Cl B and
A6: B in F;
Cl B in Cl F by A6,PCOMPS_1:def 2;
then Int Cl B in Int Cl F by Def1;
then
A7: Cl Int Cl B in Cl Int Cl F by PCOMPS_1:def 2;
C = Int Cl Int Cl B by A5,TDLAT_1:5;
hence X in Int Cl Int Cl F by A7,Def1;
end;
now
assume
A8: X in Int Cl Int Cl F;
then reconsider C = X as Subset of T;
consider B being Subset of T such that
A9: C = Int B and
A10: B in {A where A is Subset of T : ex B being Subset of T st A =
Cl Int Cl B & B in F} by A1,A8,Def1;
ex S being Subset of T st S = B & ex R being Subset of T st S = Cl
Int Cl R & R in F by A10;
then consider D being Subset of T such that
A11: B = Cl Int Cl D and
A12: D in F;
A13: Cl D in Cl F by A12,PCOMPS_1:def 2;
C = Int Cl D by A9,A11,TDLAT_1:5;
hence X in Int Cl F by A13,Def1;
end;
hence thesis by A3;
end;
hence thesis by TARSKI:2;
end;
theorem
union(Int Cl F) c= union(Cl Int Cl F)
proof
now
let x be object;
assume x in union(Int Cl F);
then consider A being set such that
A1: x in A and
A2: A in Int Cl F by TARSKI:def 4;
reconsider A as Subset of T by A2;
consider B being Subset of T such that
A3: A = Int B and
A4: B in Cl F by A2,Def1;
consider D being Subset of T such that
A5: B = Cl D and
A6: D in F by A4,PCOMPS_1:def 2;
ex P being set st x in P & P in Cl Int Cl F
proof
take Cl Int Cl D;
Cl D in Cl F by A6,PCOMPS_1:def 2;
then
A7: Int Cl D in Int Cl F by Def1;
A c= Cl Int Cl D by A3,A5,Th2;
hence thesis by A1,A7,PCOMPS_1:def 2;
end;
hence x in union(Cl Int Cl F) by TARSKI:def 4;
end;
hence thesis;
end;
theorem
meet(Int Cl F) c= meet(Cl Int Cl F)
proof
now
per cases;
suppose
F = {};
then Cl F = {} by Th9;
then Int Cl F = {} by Th18;
hence thesis by Th9;
end;
suppose
F <> {};
then Cl F <> {} by Th9;
then Int Cl F <> {} by Th18;
then
A1: Cl Int Cl F <> {} by Th9;
now
let x be object;
assume
A2: x in meet(Int Cl F);
for A being set st A in Cl Int Cl F holds x in A
proof
let A be set;
assume
A3: A in Cl Int Cl F;
then reconsider A as Subset of T;
consider B being Subset of T such that
A4: A = Cl B and
A5: B in Int Cl F by A3,PCOMPS_1:def 2;
A6: B c= Cl B by PRE_TOPC:18;
x in B by A2,A5,SETFAM_1:def 1;
hence thesis by A4,A6;
end;
hence x in meet(Cl Int Cl F) by A1,SETFAM_1:def 1;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem
union(Cl Int F) c= union(Cl Int Cl F)
proof
let x be object;
assume x in union(Cl Int F);
then consider A being set such that
A1: x in A and
A2: A in Cl Int F by TARSKI:def 4;
reconsider A as Subset of T by A2;
consider B being Subset of T such that
A3: A = Cl B and
A4: B in Int F by A2,PCOMPS_1:def 2;
consider D being Subset of T such that
A5: B = Int D and
A6: D in F by A4,Def1;
ex P being set st x in P & P in Cl Int Cl F
proof
take Cl Int Cl D;
Cl D in Cl F by A6,PCOMPS_1:def 2;
then
A7: Int Cl D in Int Cl F by Def1;
A c= Cl Int Cl D by A3,A5,Th2;
hence thesis by A1,A7,PCOMPS_1:def 2;
end;
hence x in union(Cl Int Cl F) by TARSKI:def 4;
end;
theorem
meet(Cl Int F) c= meet(Cl Int Cl F)
proof
now
per cases;
suppose
F = {};
hence thesis by Th9;
end;
suppose
F <> {};
then Cl F <> {} by Th9;
then Int Cl F <> {} by Th18;
then
A1: Cl Int Cl F <> {} by Th9;
now
let x be object;
assume
A2: x in meet(Cl Int F);
for A being set st A in Cl Int Cl F holds x in A
proof
let A be set;
assume
A3: A in Cl Int Cl F;
then reconsider A as Subset of T;
consider B being Subset of T such that
A4: A = Cl B and
A5: B in Int Cl F by A3,PCOMPS_1:def 2;
consider D being Subset of T such that
A6: B = Int D and
A7: D in Cl F by A5,Def1;
consider E being Subset of T such that
A8: D = Cl E and
A9: E in F by A7,PCOMPS_1:def 2;
Int E in Int F by A9,Def1;
then Cl Int E in Cl Int F by PCOMPS_1:def 2;
then
A10: x in Cl Int E by A2,SETFAM_1:def 1;
Cl Int E c= Cl Int Cl E by Th2;
hence thesis by A4,A6,A8,A10;
end;
hence x in meet(Cl Int Cl F) by A1,SETFAM_1:def 1;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem
union(Int Cl Int F) c= union(Int Cl F)
proof
let x be object;
assume x in union(Int Cl Int F);
then consider A being set such that
A1: x in A and
A2: A in Int Cl Int F by TARSKI:def 4;
reconsider A as Subset of T by A2;
consider B being Subset of T such that
A3: A = Int B and
A4: B in Cl Int F by A2,Def1;
consider D being Subset of T such that
A5: B = Cl D and
A6: D in Int F by A4,PCOMPS_1:def 2;
consider E being Subset of T such that
A7: D = Int E and
A8: E in F by A6,Def1;
ex P being set st x in P & P in Int Cl F
proof
take Int Cl E;
A9: Cl E in Cl F by A8,PCOMPS_1:def 2;
A c= Int Cl E by A3,A5,A7,Th1;
hence thesis by A1,A9,Def1;
end;
hence x in union(Int Cl F) by TARSKI:def 4;
end;
theorem
meet(Int Cl Int F) c= meet(Int Cl F)
proof
now
per cases;
suppose
F = {};
hence thesis by Th18;
end;
suppose
F <> {};
then Cl F <> {} by Th9;
then
A1: Int Cl F <> {} by Th18;
now
let x be object;
assume
A2: x in meet(Int Cl Int F);
for A being set st A in Int Cl F holds x in A
proof
let A be set;
assume
A3: A in Int Cl F;
then reconsider A as Subset of T;
consider E being Subset of T such that
A4: A = Int E and
A5: E in Cl F by A3,Def1;
consider B being Subset of T such that
A6: E = Cl B and
A7: B in F by A5,PCOMPS_1:def 2;
Int B in Int F by A7,Def1;
then Cl Int B in Cl Int F by PCOMPS_1:def 2;
then Int Cl Int B in Int Cl Int F by Def1;
then
A8: x in Int Cl Int B by A2,SETFAM_1:def 1;
Int Cl Int B c= Int Cl B by Th1;
hence thesis by A4,A6,A8;
end;
hence x in meet(Int Cl F) by A1,SETFAM_1:def 1;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem
union(Int Cl Int F) c= union(Cl Int F)
proof
let x be object;
assume x in union(Int Cl Int F);
then consider A being set such that
A1: x in A and
A2: A in Int Cl Int F by TARSKI:def 4;
reconsider A as Subset of T by A2;
consider B being Subset of T such that
A3: A = Int B and
A4: B in Cl Int F by A2,Def1;
consider D being Subset of T such that
A5: B = Cl D and
A6: D in Int F by A4,PCOMPS_1:def 2;
consider E being Subset of T such that
A7: D = Int E and
A8: E in F by A6,Def1;
ex P being set st x in P & P in Cl Int F
proof
take Cl Int E;
A9: Int E in Int F by A8,Def1;
A c= Cl Int E by A3,A5,A7,Th1;
hence thesis by A1,A9,PCOMPS_1:def 2;
end;
hence x in union(Cl Int F) by TARSKI:def 4;
end;
theorem
meet(Int Cl Int F) c= meet(Cl Int F)
proof
per cases;
suppose
F = {};
then Int F = {} by Th18;
then Cl Int F = {} by Th9;
hence thesis by Th18;
end;
suppose
F <> {};
then Int F <> {} by Th18;
then
A1: Cl Int F <> {} by Th9;
now
let x be object;
assume
A2: x in meet(Int Cl Int F);
for A being set st A in Cl Int F holds x in A
proof
let A be set;
assume
A3: A in Cl Int F;
then reconsider A as Subset of T;
consider E being Subset of T such that
A4: A = Cl E and
A5: E in Int F by A3,PCOMPS_1:def 2;
consider B being Subset of T such that
A6: E = Int B and
A7: B in F by A5,Def1;
Int B in Int F by A7,Def1;
then Cl Int B in Cl Int F by PCOMPS_1:def 2;
then Int Cl Int B in Int Cl Int F by Def1;
then
A8: x in Int Cl Int B by A2,SETFAM_1:def 1;
Int Cl Int B c= Cl Int B by Th1;
hence thesis by A4,A6,A8;
end;
hence x in meet(Cl Int F) by A1,SETFAM_1:def 1;
end;
hence thesis;
end;
end;
theorem
union(Cl Int Cl F) c= union(Cl F)
proof
let x be object;
assume x in union(Cl Int Cl F);
then consider A being set such that
A1: x in A and
A2: A in Cl Int Cl F by TARSKI:def 4;
reconsider A as Subset of T by A2;
consider B being Subset of T such that
A3: A = Cl B and
A4: B in Int Cl F by A2,PCOMPS_1:def 2;
consider D being Subset of T such that
A5: B = Int D and
A6: D in Cl F by A4,Def1;
consider E being Subset of T such that
A7: D = Cl E and
A8: E in F by A6,PCOMPS_1:def 2;
ex P being set st x in P & P in Cl F
proof
take Cl E;
A c= Cl E by A3,A5,A7,TDLAT_1:3;
hence thesis by A1,A8,PCOMPS_1:def 2;
end;
hence x in union(Cl F) by TARSKI:def 4;
end;
theorem
meet(Cl Int Cl F) c= meet(Cl F)
proof
per cases;
suppose
A1: F = {};
then Cl F = {} by Th9;
hence thesis by A1,Th18;
end;
suppose
F <> {};
then
A2: Cl F <> {} by Th9;
let x be object;
assume
A3: x in meet(Cl Int Cl F);
for A being set st A in Cl F holds x in A
proof
let A be set;
assume
A4: A in Cl F;
then reconsider A as Subset of T;
consider B being Subset of T such that
A5: A = Cl B and
A6: B in F by A4,PCOMPS_1:def 2;
Cl B in Cl F by A6,PCOMPS_1:def 2;
then Int Cl B in Int Cl F by Def1;
then Cl Int Cl B in Cl Int Cl F by PCOMPS_1:def 2;
then
A7: x in Cl Int Cl B by A3,SETFAM_1:def 1;
Cl Int Cl B c= Cl B by TDLAT_1:3;
hence thesis by A5,A7;
end;
hence x in meet(Cl F) by A2,SETFAM_1:def 1;
end;
end;
theorem
union(Int F) c= union(Int Cl Int F)
proof
let x be object;
assume x in union(Int F);
then consider A being set such that
A1: x in A and
A2: A in Int F by TARSKI:def 4;
reconsider A as Subset of T by A2;
consider B being Subset of T such that
A3: A = Int B and
A4: B in F by A2,Def1;
ex P being set st x in P & P in Int Cl Int F
proof
take Int Cl Int B;
Int B in Int F by A4,Def1;
then
A5: Cl Int B in Cl Int F by PCOMPS_1:def 2;
A c= Int Cl Int B by A3,TDLAT_1:4;
hence thesis by A1,A5,Def1;
end;
hence x in union(Int Cl Int F) by TARSKI:def 4;
end;
theorem
meet(Int F) c= meet(Int Cl Int F)
proof
per cases;
suppose
A1: F = {};
then Int F = {} by Th18;
hence thesis by A1,Th9;
end;
suppose
F <> {};
then Int F <> {} by Th18;
then Cl Int F <> {} by Th9;
then
A2: Int Cl Int F <> {} by Th18;
let x be object;
assume
A3: x in meet(Int F);
for A being set st A in Int Cl Int F holds x in A
proof
let A be set;
assume
A4: A in Int Cl Int F;
then reconsider A as Subset of T;
consider E being Subset of T such that
A5: A = Int E and
A6: E in Cl Int F by A4,Def1;
consider B being Subset of T such that
A7: E = Cl B and
A8: B in Int F by A6,PCOMPS_1:def 2;
consider D being Subset of T such that
A9: B = Int D and
A10: D in F by A8,Def1;
Int D in Int F by A10,Def1;
then
A11: x in Int D by A3,SETFAM_1:def 1;
Int D c= Int Cl Int D by TDLAT_1:4;
hence thesis by A5,A7,A9,A11;
end;
hence x in meet(Int Cl Int F) by A2,SETFAM_1:def 1;
end;
end;
theorem Th48:
union(Cl Int F) c= Cl Int(union F)
proof
A1: Cl(union Int F) c= Cl Int(union F) by Th27,PRE_TOPC:19;
union(Cl Int F) c= Cl(union Int F) by Th15;
hence thesis by A1;
end;
theorem Th49:
Cl Int(meet F) c= meet(Cl Int F)
proof
A1: Cl (meet Int F) c= meet(Cl Int F) by Th14;
Cl Int(meet F) c= Cl meet(Int F) by Th28,PRE_TOPC:19;
hence thesis by A1;
end;
theorem Th50:
union(Int Cl F) c= Int Cl(union F)
proof
A1: Int(union Cl F) c= Int Cl(union F) by Th15,TOPS_1:19;
union(Int Cl F) c= Int(union Cl F) by Th27;
hence thesis by A1;
end;
theorem Th51:
Int Cl(meet F) c= meet(Int Cl F)
proof
A1: Int(meet Cl F) c= meet(Int Cl F) by Th28;
Int Cl(meet F) c= Int meet(Cl F) by Th14,TOPS_1:19;
hence thesis by A1;
end;
theorem
union(Cl Int Cl F) c= Cl Int Cl(union F)
proof
A1: Cl(union Int Cl F) c= Cl Int Cl(union F) by Th50,PRE_TOPC:19;
union(Cl Int Cl F) c= Cl(union Int Cl F) by Th15;
hence thesis by A1;
end;
theorem
Cl Int Cl(meet F) c= meet(Cl Int Cl F)
proof
A1: Cl Int Cl(meet F) c= Cl(meet Int Cl F) by Th51,PRE_TOPC:19;
Cl(meet Int Cl F) c= meet(Cl Int Cl F) by Th14;
hence thesis by A1;
end;
theorem
union(Int Cl Int F) c= Int Cl Int(union F)
proof
A1: Int(union Cl Int F) c= Int Cl Int(union F) by Th48,TOPS_1:19;
union(Int Cl Int F) c= Int(union Cl Int F) by Th27;
hence thesis by A1;
end;
theorem
Int Cl Int(meet F) c= meet(Int Cl Int F)
proof
A1: Int Cl Int(meet F) c= Int(meet Cl Int F) by Th49,TOPS_1:19;
Int(meet Cl Int F) c= meet(Int Cl Int F) by Th28;
hence thesis by A1;
end;
theorem Th56:
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)
proof
let F be Subset-Family of T;
A1: Cl Int Cl(union F) c= Cl Cl(union F) by PRE_TOPC:19,TOPS_1:16;
assume
A2: for A being Subset of T st A in F holds A c= Cl Int A;
A3: now
let A0 be set;
assume
A4: A0 in F;
then reconsider A = A0 as Subset of T;
Int A c= Int(union F) by A4,TOPS_1:19,ZFMISC_1:74;
then
A5: Cl Int A c= Cl Int(union F) by PRE_TOPC:19;
A c= Cl Int A by A2,A4;
hence A0 c= Cl Int(union F) by A5;
end;
hence union F c= Cl Int(union F) by ZFMISC_1:76;
Int(union F) c= Int Cl(union F) by PRE_TOPC:18,TOPS_1:19;
then
A6: Cl Int(union F) c= Cl Int Cl(union F) by PRE_TOPC:19;
union F c= Cl Int(union F) by A3,ZFMISC_1:76;
then Cl(union F) c= Cl Cl Int(union F) by PRE_TOPC:19;
then Cl(union F) c= Cl Int Cl(union F) by A6;
hence Cl(union F) = Cl Int Cl(union F) by A1,XBOOLE_0:def 10;
end;
theorem Th57:
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)
proof
let F be Subset-Family of T;
A1: Int Int (meet F) c= Int Cl Int(meet F) by PRE_TOPC:18,TOPS_1:19;
assume
A2: for A being Subset of T st A in F holds Int Cl A c= A;
thus Int Cl(meet F) c= meet F
proof
now
per cases;
suppose
A3: F = {};
Cl {}T = {}T by PRE_TOPC:22;
hence thesis by A3,SETFAM_1:1;
end;
suppose
A4: F <> {};
now
let A0 be set;
assume
A5: A0 in F;
then reconsider A = A0 as Subset of T;
Cl(meet F) c= Cl A by A5,PRE_TOPC:19,SETFAM_1:3;
then
A6: Int Cl(meet F) c= Int Cl A by TOPS_1:19;
Int Cl A c= A by A2,A5;
hence Int Cl(meet F) c= A0 by A6;
end;
hence thesis by A4,SETFAM_1:5;
end;
end;
hence thesis;
end;
then
A7: Int Int Cl(meet F) c= Int(meet F) by TOPS_1:19;
Cl Int(meet F) c= Cl(meet F) by PRE_TOPC:19,TOPS_1:16;
then Int Cl Int(meet F) c= Int Cl(meet F) by TOPS_1:19;
then Int Cl Int(meet F) c= Int(meet F) by A7;
hence Int Cl Int(meet F) = Int(meet F) by A1,XBOOLE_0:def 10;
end;
begin
:: 3. Selected Properties of Domains of a Topological Space.
reserve T for non empty TopSpace;
theorem Th58:
for A, B being Subset of T st B is condensed holds Int(Cl(A \/ B
)) \/ (A \/ B) = B iff A c= B
proof
let A, B be Subset of T;
assume
A1: B is condensed;
thus Int(Cl(A \/ B)) \/ (A \/ B) = B implies A c= B
proof
assume Int(Cl(A \/ B)) \/ (A \/ B) = B;
then
A2: A \/ B c= B by XBOOLE_1:7;
A c= A \/ B by XBOOLE_1:7;
hence thesis by A2;
end;
thus A c= B implies Int(Cl(A \/ B)) \/ (A \/ B) = B
proof
assume A c= B;
then
A3: A \/ B = B by XBOOLE_1:12;
then Int(Cl(A \/ B)) c= B by A1,TOPS_1:def 6;
hence thesis by A3,XBOOLE_1:12;
end;
end;
theorem
for A, B being Subset of T st A is condensed holds Cl(Int(A /\ B)) /\
(A /\ B) = A iff A c= B
proof
let A, B be Subset of T;
assume
A1: A is condensed;
thus Cl(Int(A /\ B)) /\ (A /\ B) = A implies A c= B
proof
assume Cl(Int(A /\ B)) /\ (A /\ B) = A;
then
A2: A c= A /\ B by XBOOLE_1:17;
A /\ B c= B by XBOOLE_1:17;
hence thesis by A2;
end;
thus A c= B implies Cl(Int(A /\ B)) /\ (A /\ B) = A
proof
assume A c= B;
then
A3: A /\ B = A by XBOOLE_1:28;
then A c= Cl(Int(A /\ B)) by A1,TOPS_1:def 6;
hence thesis by A3,XBOOLE_1:28;
end;
end;
theorem
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
proof
let A, B be Subset of T;
assume that
A1: A is closed_condensed and
A2: B is closed_condensed;
thus Int A c= Int B implies A c= B
proof
assume Int A c= Int B;
then
A3: Cl Int A c= Cl Int B by PRE_TOPC:19;
Cl Int A = A by A1,TOPS_1:def 7;
hence thesis by A2,A3,TOPS_1:def 7;
end;
thus thesis by TOPS_1:19;
end;
theorem
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
proof
let A, B be Subset of T;
assume that
A1: A is open_condensed and
A2: B is open_condensed;
thus Cl A c= Cl B implies A c= B
proof
assume Cl A c= Cl B;
then
A3: Int Cl A c= Int Cl B by TOPS_1:19;
Int Cl A = A by A1,TOPS_1:def 8;
hence thesis by A2,A3,TOPS_1:def 8;
end;
thus thesis by PRE_TOPC:19;
end;
theorem
for A, B being Subset of T st A is closed_condensed holds A c= B
implies Cl(Int(A /\ B)) = A
proof
let A, B be Subset of T;
assume
A1: A is closed_condensed;
assume A c= B;
then A /\ B = A by XBOOLE_1:28;
hence thesis by A1,TOPS_1:def 7;
end;
theorem Th63:
for A, B being Subset of T st B is open_condensed holds A c= B
implies Int(Cl(A \/ B)) = B
proof
let A, B be Subset of T;
assume
A1: B is open_condensed;
assume A c= B;
then A \/ B = B by XBOOLE_1:12;
hence thesis by A1,TOPS_1:def 8;
end;
definition
let T;
let IT be Subset-Family of T;
attr IT is domains-family means
for A being Subset of T holds A in IT implies A is condensed;
end;
theorem Th64:
for F being Subset-Family of T holds F c= Domains_of T iff F is
domains-family
proof
let F be Subset-Family of T;
thus F c= Domains_of T implies F is domains-family
proof
assume
A1: F c= Domains_of T;
now
let A be Subset of T;
assume A in F;
then A in Domains_of T by A1;
then A in {P where P is Subset of T : P is condensed} by TDLAT_1:def 1;
then ex Q being Subset of T st Q = A & Q is condensed;
hence A is condensed;
end;
hence thesis;
end;
thus F is domains-family implies F c= Domains_of T
proof
assume
A2: F is domains-family;
for X being object holds X in F implies X in Domains_of T
proof
let X be object;
assume
A3: X in F;
then reconsider X0 = X as Subset of T;
X0 is condensed by A2,A3;
then X0 in {P where P is Subset of T : P is condensed};
hence thesis by TDLAT_1:def 1;
end;
hence thesis;
end;
end;
theorem Th65:
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)
proof
let F be Subset-Family of T;
assume
A1: F is domains-family;
now
let A be Subset of T;
reconsider B = A as Subset of T;
assume A in F;
then B is condensed by A1;
hence A c= Cl Int A by TOPS_1:def 6;
end;
hence thesis by Th56;
end;
theorem Th66:
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)
proof
let F be Subset-Family of T;
assume
A1: F is domains-family;
now
let A be Subset of T;
reconsider B = A as Subset of T;
assume A in F;
then B is condensed by A1;
hence Int Cl A c= A by TOPS_1:def 6;
end;
hence thesis by Th57;
end;
theorem Th67:
for F being Subset-Family of T holds F is domains-family implies
(union F) \/ (Int Cl(union F)) is condensed
proof
let F be Subset-Family of T;
A1: Cl Int Cl(union F) c= Cl Cl(union F) by PRE_TOPC:19,TOPS_1:16;
assume F is domains-family;
then union F c= Cl Int(union F) by Th65;
then
A2: (union F) \/ (Int Cl(union F)) c= Cl Int((union F) \/ (Int Cl(union F))
) by Th5;
Int Cl((union F) \/ (Int Cl(union F))) = Int(Cl(union F) \/ Cl(Int Cl(
union F))) by PRE_TOPC:20
.= Int(Cl(union F)) by A1,XBOOLE_1:12;
then
Int Cl((union F) \/ (Int Cl(union F))) c= (union F) \/ (Int Cl(union F))
by XBOOLE_1:7;
hence thesis by A2,TOPS_1:def 6;
end;
theorem Th68:
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
proof
let F be Subset-Family of T;
thus for B being Subset of T st B in F holds B c= (union F) \/ (Int Cl(union
F))
proof
let B be Subset of T;
assume B in F;
then
A1: B c= union F by ZFMISC_1:74;
union F c= (union F) \/ (Int Cl(union F)) by XBOOLE_1:7;
hence thesis by A1;
end;
thus 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
proof
let A be Subset of T;
assume A is condensed;
then
A2: Int Cl A c= A by TOPS_1:def 6;
assume for B being Subset of T st B in F holds B c= A;
then for P be set st P in F holds P c= A;
then
A3: union F c= A by ZFMISC_1:76;
then Cl(union F) c= Cl A by PRE_TOPC:19;
then Int Cl(union F) c= Int Cl A by TOPS_1:19;
then Int Cl(union F) c= A by A2;
hence thesis by A3,XBOOLE_1:8;
end;
end;
theorem Th69:
for F being Subset-Family of T holds F is domains-family implies
(meet F) /\ (Cl Int(meet F)) is condensed
proof
let F be Subset-Family of T;
A1: Int Int (meet F) c= Int Cl Int(meet F) by PRE_TOPC:18,TOPS_1:19;
assume F is domains-family;
then Int Cl(meet F) c= meet F by Th66;
then
A2: Int Cl((meet F) /\ (Cl Int(meet F))) c= (meet F) /\ (Cl Int(meet F)) by Th6
;
Cl Int((meet F) /\ (Cl Int(meet F))) = Cl(Int(meet F) /\ Int(Cl Int(meet
F))) by TOPS_1:17
.= Cl(Int(meet F)) by A1,XBOOLE_1:28;
then
(meet F) /\ (Cl Int(meet F)) c= Cl Int((meet F) /\ (Cl Int(meet F))) by
XBOOLE_1:17;
hence thesis by A2,TOPS_1:def 6;
end;
theorem Th70:
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)))
proof
let F be Subset-Family of T;
thus for B being Subset of T st B in F holds (meet F) /\ (Cl Int(meet F)) c=
B
proof
let B be Subset of T;
assume B in F;
then
A1: meet F c= B by SETFAM_1:3;
(meet F) /\ (Cl Int(meet F)) c= meet F by XBOOLE_1:17;
hence thesis by A1;
end;
thus 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))
proof
assume
A2: F <> {};
let A be Subset of T;
assume A is condensed;
then
A3: A c= Cl Int A by TOPS_1:def 6;
assume for B being Subset of T st B in F holds A c= B;
then for P be set st P in F holds A c= P;
then
A4: A c= meet F by A2,SETFAM_1:5;
then Int A c= Int(meet F) by TOPS_1:19;
then Cl Int A c= Cl Int(meet F) by PRE_TOPC:19;
then A c= Cl Int(meet F) by A3;
hence thesis by A4,XBOOLE_1:19;
end;
end;
definition
let T;
let IT be Subset-Family of T;
attr IT is closed-domains-family means
for A being Subset of T holds A in IT implies A is closed_condensed;
end;
theorem Th71:
for F being Subset-Family of T holds F c= Closed_Domains_of T
iff F is closed-domains-family
proof
let F be Subset-Family of T;
thus F c= Closed_Domains_of T implies F is closed-domains-family
proof
assume
A1: F c= Closed_Domains_of T;
now
let A be Subset of T;
assume A in F;
then A in Closed_Domains_of T by A1;
then A in {P where P is Subset of T : P is closed_condensed} by
TDLAT_1:def 5;
then ex Q being Subset of T st Q = A & Q is closed_condensed;
hence A is closed_condensed;
end;
hence thesis;
end;
thus F is closed-domains-family implies F c= Closed_Domains_of T
proof
assume
A2: F is closed-domains-family;
for X being object holds X in F implies X in Closed_Domains_of T
proof
let X be object;
assume
A3: X in F;
then reconsider X0 = X as Subset of T;
X0 is closed_condensed by A2,A3;
then X0 in {P where P is Subset of T : P is closed_condensed};
hence thesis by TDLAT_1:def 5;
end;
hence thesis;
end;
end;
theorem Th72:
for F being Subset-Family of T holds F is closed-domains-family
implies F is domains-family
proof
let F be Subset-Family of T;
thus F is closed-domains-family implies F is domains-family
proof
assume F is closed-domains-family;
then
A1: F c= Closed_Domains_of T by Th71;
Closed_Domains_of T c= Domains_of T by TDLAT_1:31;
then F c= Domains_of T by A1;
hence thesis by Th64;
end;
end;
theorem Th73:
for F being Subset-Family of T holds F is closed-domains-family
implies F is closed
proof
let F be Subset-Family of T;
assume
A1: F is closed-domains-family;
for A being Subset of T holds A in F implies A is closed
proof
let A be Subset of T;
assume A in F;
then A is closed_condensed by A1;
hence thesis by TOPS_1:66;
end;
hence thesis by TOPS_2:def 2;
end;
theorem
for F being Subset-Family of T holds F is domains-family implies Cl F
is closed-domains-family
proof
let F be Subset-Family of T;
assume
A1: F is domains-family;
for A being Subset of T holds A in Cl F implies A is closed_condensed
proof
let A be Subset of T;
assume A in Cl F;
then consider P being Subset of T such that
A2: A = Cl P and
A3: P in F by PCOMPS_1:def 2;
reconsider P as Subset of T;
P is condensed by A1,A3;
hence thesis by A2,TDLAT_1:24;
end;
hence thesis;
end;
theorem Th75:
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
proof
let F be Subset-Family of T;
assume F is closed-domains-family;
then F is domains-family by Th72;
then Cl(union F) = Cl Int Cl(union F) by Th65;
hence Cl(union F) is closed_condensed by TOPS_1:def 7;
thus thesis by TDLAT_1:22;
end;
theorem Th76:
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
proof
let F be Subset-Family of T;
thus for B being Subset of T st B in F holds B c= Cl(union F)
proof
let B be Subset of T;
assume B in F;
then
A1: B c= union F by ZFMISC_1:74;
union F c= Cl(union F) by PRE_TOPC:18;
hence thesis by A1;
end;
thus 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
proof
let A be Subset of T;
reconsider A1 = A as Subset of T;
assume A is closed_condensed;
then
A2: A1 is closed by TOPS_1:66;
assume for B being Subset of T st B in F holds B c= A;
then for P be set st P in F holds P c= A;
then union F c= A by ZFMISC_1:76;
then Cl(union F) c= Cl A by PRE_TOPC:19;
hence thesis by A2,PRE_TOPC:22;
end;
end;
theorem Th77:
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))
proof
let F be Subset-Family of T;
thus F is closed implies for B being Subset of T st B in F holds Cl Int(meet
F) c= B
proof
assume F is closed;
then meet F is closed by TOPS_2:22;
then
A1: Cl meet F = meet F by PRE_TOPC:22;
let B be Subset of T;
A2: Cl Int(meet F) c= Cl meet F by PRE_TOPC:19,TOPS_1:16;
assume B in F;
then meet F c= B by SETFAM_1:3;
hence thesis by A2,A1;
end;
thus 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)
proof
assume
A3: F <> {};
let A be Subset of T;
assume
A4: A is closed_condensed;
assume for B being Subset of T st B in F holds A c= B;
then for P be set st P in F holds A c= P;
then A c= meet F by A3,SETFAM_1:5;
then
A5: Int A c= Int(meet F) by TOPS_1:19;
A = Cl Int A by A4,TOPS_1:def 7;
hence thesis by A5,PRE_TOPC:19;
end;
end;
definition
let T;
let IT be Subset-Family of T;
attr IT is open-domains-family means
for A being Subset of T holds A in IT implies A is open_condensed;
end;
theorem Th78:
for F being Subset-Family of T holds F c= Open_Domains_of T iff
F is open-domains-family
proof
let F be Subset-Family of T;
thus F c= Open_Domains_of T implies F is open-domains-family
proof
assume
A1: F c= Open_Domains_of T;
now
let A be Subset of T;
assume A in F;
then A in Open_Domains_of T by A1;
then A in {P where P is Subset of T : P is open_condensed} by
TDLAT_1:def 9;
then ex Q being Subset of T st Q = A & Q is open_condensed;
hence A is open_condensed;
end;
hence thesis;
end;
thus F is open-domains-family implies F c= Open_Domains_of T
proof
assume
A2: F is open-domains-family;
for X being object holds X in F implies X in Open_Domains_of T
proof
let X be object;
assume
A3: X in F;
then reconsider X0 = X as Subset of T;
X0 is open_condensed by A2,A3;
then X0 in {P where P is Subset of T : P is open_condensed};
hence thesis by TDLAT_1:def 9;
end;
hence thesis;
end;
end;
theorem Th79:
for F being Subset-Family of T holds F is open-domains-family
implies F is domains-family
proof
let F be Subset-Family of T;
thus F is open-domains-family implies F is domains-family
proof
assume F is open-domains-family;
then
A1: F c= Open_Domains_of T by Th78;
Open_Domains_of T c= Domains_of T by TDLAT_1:35;
then F c= Domains_of T by A1;
hence thesis by Th64;
end;
end;
theorem Th80:
for F being Subset-Family of T holds F is open-domains-family
implies F is open
proof
let F be Subset-Family of T;
assume
A1: F is open-domains-family;
for A being Subset of T holds A in F implies A is open
proof
let A be Subset of T;
assume A in F;
then A is open_condensed by A1;
hence thesis by TOPS_1:67;
end;
hence thesis by TOPS_2:def 1;
end;
theorem
for F being Subset-Family of T holds F is domains-family implies Int F
is open-domains-family
proof
let F be Subset-Family of T;
assume
A1: F is domains-family;
for A being Subset of T holds A in Int F implies A is open_condensed
proof
let A be Subset of T;
assume A in Int F;
then consider P being Subset of T such that
A2: A = Int P and
A3: P in F by Def1;
reconsider P as Subset of T;
P is condensed by A1,A3;
hence thesis by A2,TDLAT_1:25;
end;
hence thesis;
end;
theorem Th82:
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
proof
let F be Subset-Family of T;
assume F is open-domains-family;
then F is domains-family by Th79;
then Int Cl Int(meet F) = Int(meet F) by Th66;
hence Int(meet F) is open_condensed by TOPS_1:def 8;
thus thesis by TDLAT_1:23;
end;
theorem Th83:
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
proof
let F be Subset-Family of T;
thus F is open implies for B being Subset of T st B in F holds B c= Int Cl(
union F)
proof
assume F is open;
then union F is open by TOPS_2:19;
then
A1: Int(union F) = union F by TOPS_1:23;
let B be Subset of T;
A2: Int(union F) c= Int Cl(union F) by PRE_TOPC:18,TOPS_1:19;
assume B in F;
then B c= union F by ZFMISC_1:74;
hence thesis by A2,A1;
end;
thus 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
proof
let A be Subset of T;
assume A is open_condensed;
then
A3: A = Int Cl A by TOPS_1:def 8;
assume for B being Subset of T st B in F holds B c= A;
then for P be set st P in F holds P c= A;
then union F c= A by ZFMISC_1:76;
then Cl(union F) c= Cl A by PRE_TOPC:19;
hence thesis by A3,TOPS_1:19;
end;
end;
theorem Th84:
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))
proof
let F be Subset-Family of T;
thus for B being Subset of T st B in F holds Int(meet F) c= B
proof
let B be Subset of T;
assume B in F;
then
A1: meet F c= B by SETFAM_1:3;
Int(meet F) c= meet F by TOPS_1:16;
hence thesis by A1;
end;
thus 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)
proof
assume
A2: F <> {};
let A be Subset of T;
assume
A3: A is open_condensed;
assume for B being Subset of T st B in F holds A c= B;
then for P be set st P in F holds A c= P;
then
A4: A c= meet F by A2,SETFAM_1:5;
A is open by A3,TOPS_1:67;
then Int A = A by TOPS_1:23;
hence thesis by A4,TOPS_1:19;
end;
end;
begin
:: 4. Completeness of the Lattice of Domains.
reserve T for non empty TopSpace;
theorem Th85:
the carrier of Domains_Lattice T = Domains_of T
proof
Domains_Lattice T = LattStr(#Domains_of T,D-Union T,D-Meet T#) by
TDLAT_1:def 4;
hence thesis;
end;
theorem Th86:
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)
proof
let a, b be Element of Domains_Lattice T;
let A, B be Element of Domains_of T;
assume that
A1: a = A and
A2: b = B;
A3: Domains_Lattice T = LattStr(#Domains_of T,D-Union T,D-Meet T#) by
TDLAT_1:def 4;
hence a "\/" b = (D-Union T).(A,B) by A1,A2,LATTICES:def 1
.= Int(Cl(A \/ B)) \/ (A \/ B) by TDLAT_1:def 2;
thus a "/\" b = (D-Meet T).(A,B) by A3,A1,A2,LATTICES:def 2
.= Cl(Int(A /\ B)) /\ (A /\ B) by TDLAT_1:def 3;
end;
theorem
Bottom (Domains_Lattice T) = {}T & Top (Domains_Lattice T) = [#]T
proof
thus Bottom (Domains_Lattice T) = {}T
proof
{}T is condensed by TDLAT_1:14;
then
A1: {}T in {A where A is Subset of T : A is condensed};
then reconsider E = {}T as Element of Domains_of T by TDLAT_1:def 1;
{}T in Domains_of T by A1,TDLAT_1:def 1;
then reconsider e = {}T as Element of Domains_Lattice T by Th85;
for a being Element of Domains_Lattice T holds e "\/" a = a
proof
let a be Element of Domains_Lattice T;
reconsider A = a as Element of Domains_of T by Th85;
A in Domains_of T;
then A in {C where C is Subset of T : C is condensed} by TDLAT_1:def 1;
then ex D being Subset of T st D = A & D is condensed;
then
A2: Int(Cl A) c= A by TOPS_1:def 6;
thus e "\/" a = Int(Cl(E \/ A)) \/ (E \/ A) by Th86
.= a by A2,XBOOLE_1:12;
end;
hence thesis by LATTICE2:14;
end;
thus Top (Domains_Lattice T) = [#]T
proof
[#]T is condensed by TDLAT_1:15;
then
A3: [#]T in {A where A is Subset of T : A is condensed};
then reconsider E = [#]T as Element of Domains_of T by TDLAT_1:def 1;
[#]T in Domains_of T by A3,TDLAT_1:def 1;
then reconsider e = [#]T as Element of Domains_Lattice T by Th85;
for a being Element of Domains_Lattice T holds e "/\" a = a
proof
let a be Element of Domains_Lattice T;
reconsider A = a as Element of Domains_of T by Th85;
A in Domains_of T;
then A in {C where C is Subset of T : C is condensed} by TDLAT_1:def 1;
then ex D being Subset of T st D = A & D is condensed;
then
A4: A c= Cl(Int A) by TOPS_1:def 6;
thus e "/\" a = Cl(Int(E /\ A)) /\ (E /\ A) by Th86
.= Cl(Int(A)) /\ ([#]T /\ A) by XBOOLE_1:28
.= Cl(Int(A)) /\ A by XBOOLE_1:28
.= a by A4,XBOOLE_1:28;
end;
hence thesis by LATTICE2:16;
end;
end;
theorem Th88:
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
proof
let a, b be Element of Domains_Lattice T;
let A, B be Element of Domains_of T;
assume that
A1: a = A and
A2: b = B;
B in Domains_of T;
then B in {C where C is Subset of T : C is condensed} by TDLAT_1:def 1;
then
A3: ex Q being Subset of T st Q = B & Q is condensed;
thus a [= b implies A c= B
proof
assume a [= b;
then a "\/" b = b by LATTICES:def 3;
then Int(Cl(A \/ B)) \/ (A \/ B) = B by A1,A2,Th86;
hence thesis by A3,Th58;
end;
assume A c= B;
then Int(Cl(A \/ B)) \/ (A \/ B) = B by A3,Th58;
then a "\/" b = b by A1,A2,Th86;
hence thesis by LATTICES:def 3;
end;
theorem Th89:
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
proof
let X be Subset of Domains_Lattice T;
X c= the carrier of Domains_Lattice T;
then
A1: X c= Domains_of T by Th85;
then reconsider F = X as Subset-Family of T by TOPS_2:2;
set A = (union F) \/ (Int Cl(union F));
A2: F is domains-family by A1,Th64;
then A is condensed by Th67;
then A in {C where C is Subset of T : C is condensed};
then
A3: A in Domains_of T by TDLAT_1:def 1;
then reconsider a = A as Element of Domains_Lattice T by Th85;
A4: for b being Element of Domains_Lattice T st X is_less_than b holds a [= b
proof
let b be Element of Domains_Lattice T;
reconsider B = b as Element of Domains_of T by Th85;
assume
A5: X is_less_than b;
A6: for C being Subset of T st C in F holds C c= B
proof
let C be Subset of T;
reconsider C1 = C as Subset of T;
assume
A7: C in F;
then C1 is condensed by A2;
then C in {P where P is Subset of T : P is condensed};
then
A8: C in Domains_of T by TDLAT_1:def 1;
then reconsider c = C as Element of Domains_Lattice T by Th85;
c [= b by A5,A7;
hence thesis by A8,Th88;
end;
B in Domains_of T;
then B in {C where C is Subset of T : C is condensed} by TDLAT_1:def 1;
then ex C being Subset of T st C = B & C is condensed;
then A c= B by A6,Th68;
hence thesis by A3,Th88;
end;
take a;
X is_less_than a
proof
let b be Element of Domains_Lattice T;
reconsider B = b as Element of Domains_of T by Th85;
assume b in X;
then B c= A by Th68;
hence thesis by A3,Th88;
end;
hence thesis by A4;
end;
theorem Th90:
Domains_Lattice T is complete
proof
thus for X being set 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
proof
let X be set;
set Y = { c where c is Element of Domains_Lattice T : c in X};
A1: for d being Element of Domains_Lattice T holds Y is_less_than d
implies X is_less_than d
proof
let d be Element of Domains_Lattice T;
assume
A2: Y is_less_than d;
thus for e being Element of Domains_Lattice T st e in X holds e [= d
proof
let e be Element of Domains_Lattice T;
assume e in X;
then e in Y;
hence thesis by A2;
end;
end;
A3: for d being Element of Domains_Lattice T holds X is_less_than d
implies Y is_less_than d
proof
let d be Element of Domains_Lattice T;
assume
A4: X is_less_than d;
thus for e being Element of Domains_Lattice T st e in Y holds e [= d
proof
let e be Element of Domains_Lattice T;
assume e in Y;
then ex e0 being Element of Domains_Lattice T st e0 = e & e0 in X;
hence thesis by A4;
end;
end;
now
let x be object;
assume x in Y;
then ex y being Element of Domains_Lattice T st y = x & y in X;
hence x in the carrier of Domains_Lattice T;
end;
then reconsider Y as Subset of Domains_Lattice T by TARSKI:def 3;
consider a being Element of Domains_Lattice T such that
A5: Y is_less_than a and
A6: for b being Element of Domains_Lattice T st Y is_less_than b
holds a [= b by Th89;
take a;
for b being Element of Domains_Lattice T st X is_less_than b holds a
[= b by A3,A6;
hence thesis by A1,A5;
end;
end;
theorem Th91:
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))
proof
let F be Subset-Family of T;
assume
A1: F is domains-family;
let X be Subset of Domains_Lattice T;
assume
A2: X = F;
thus "\/"(X,Domains_Lattice T) = (union F) \/ (Int Cl(union F))
proof
set A = (union F) \/ (Int Cl(union F));
A is condensed by A1,Th67;
then A in {C where C is Subset of T : C is condensed};
then
A3: A in Domains_of T by TDLAT_1:def 1;
then reconsider a = A as Element of Domains_Lattice T by Th85;
A4: X is_less_than a
proof
let b be Element of Domains_Lattice T;
reconsider B = b as Element of Domains_of T by Th85;
assume b in X;
then B c= A by A2,Th68;
hence thesis by A3,Th88;
end;
A5: for b being Element of Domains_Lattice T st X is_less_than b holds a [= b
proof
let b be Element of Domains_Lattice T;
reconsider B = b as Element of Domains_of T by Th85;
assume
A6: X is_less_than b;
A7: for C being Subset of T st C in F holds C c= B
proof
let C be Subset of T;
reconsider C1 = C as Subset of T;
assume
A8: C in F;
then C1 is condensed by A1;
then C in {P where P is Subset of T : P is condensed};
then
A9: C in Domains_of T by TDLAT_1:def 1;
then reconsider c = C as Element of Domains_Lattice T by Th85;
c [= b by A2,A6,A8;
hence thesis by A9,Th88;
end;
B in Domains_of T;
then B in {C where C is Subset of T : C is condensed } by TDLAT_1:def 1;
then ex C being Subset of T st C = B & C is condensed;
then A c= B by A7,Th68;
hence thesis by A3,Th88;
end;
Domains_Lattice T is complete by Th90;
hence thesis by A4,A5,LATTICE3:def 21;
end;
end;
theorem Th92:
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)
proof
let F be Subset-Family of T;
assume
A1: F is domains-family;
let X be Subset of Domains_Lattice T;
assume
A2: X = F;
thus X <> {} implies "/\"(X,Domains_Lattice T) = (meet F) /\ (Cl Int(meet F)
)
proof
set A = (meet F) /\ (Cl Int(meet F));
A is condensed by A1,Th69;
then A in {C where C is Subset of T : C is condensed};
then
A3: A in Domains_of T by TDLAT_1:def 1;
then reconsider a = A as Element of Domains_Lattice T by Th85;
A4: a is_less_than X
proof
let b be Element of Domains_Lattice T;
reconsider B = b as Element of Domains_of T by Th85;
assume b in X;
then A c= B by A2,Th70;
hence thesis by A3,Th88;
end;
assume
A5: X <> {};
A6: for b being Element of Domains_Lattice T st b is_less_than X holds b [= a
proof
let b be Element of Domains_Lattice T;
reconsider B = b as Element of Domains_of T by Th85;
assume
A7: b is_less_than X;
A8: for C being Subset of T st C in F holds B c= C
proof
let C be Subset of T;
reconsider C1 = C as Subset of T;
assume
A9: C in F;
then C1 is condensed by A1;
then C in {P where P is Subset of T : P is condensed};
then
A10: C in Domains_of T by TDLAT_1:def 1;
then reconsider c = C as Element of Domains_Lattice T by Th85;
b [= c by A2,A7,A9;
hence thesis by A10,Th88;
end;
B in Domains_of T;
then B in {C where C is Subset of T : C is condensed} by TDLAT_1:def 1;
then ex C being Subset of T st C = B & C is condensed;
then B c= A by A2,A5,A8,Th70;
hence thesis by A3,Th88;
end;
Domains_Lattice T is complete by Th90;
hence thesis by A4,A6,LATTICE3:34;
end;
thus X = {} implies "/\"(X,Domains_Lattice T) = [#]T
proof
set A = [#]T;
A is condensed by TDLAT_1:15;
then A in {C where C is Subset of T : C is condensed};
then
A11: A in Domains_of T by TDLAT_1:def 1;
then reconsider a = A as Element of Domains_Lattice T by Th85;
A12: for b being Element of Domains_Lattice T st b is_less_than X holds b [= a
proof
let b be Element of Domains_Lattice T;
reconsider B = b as Element of Domains_of T by Th85;
assume b is_less_than X;
B c= A;
hence thesis by A11,Th88;
end;
assume
A13: X = {};
A14: a is_less_than X
by A13;
Domains_Lattice T is complete by Th90;
hence thesis by A14,A12,LATTICE3:34;
end;
end;
begin
:: 5. Completeness of the Lattices of Closed Domains and Open Domains.
reserve T for non empty TopSpace;
::The Lattice of Closed Domains.
theorem Th93:
the carrier of Closed_Domains_Lattice T = Closed_Domains_of T
proof
Closed_Domains_Lattice T = LattStr(#Closed_Domains_of T,CLD-Union T,
CLD-Meet T#) by TDLAT_1:def 8;
hence thesis;
end;
theorem Th94:
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))
proof
let a, b be Element of Closed_Domains_Lattice T;
let A, B be Element of Closed_Domains_of T;
assume that
A1: a = A and
A2: b = B;
A3: Closed_Domains_Lattice T = LattStr(#Closed_Domains_of T,CLD-Union T,
CLD-Meet T#) by TDLAT_1:def 8;
hence a "\/" b = (CLD-Union T).(A,B) by A1,A2,LATTICES:def 1
.= A \/ B by TDLAT_1:def 6;
thus a "/\" b = (CLD-Meet T).(A,B) by A3,A1,A2,LATTICES:def 2
.= Cl(Int(A /\ B)) by TDLAT_1:def 7;
end;
theorem
Bottom (Closed_Domains_Lattice T) = {}T & Top (Closed_Domains_Lattice
T) = [#]T
proof
thus Bottom (Closed_Domains_Lattice T) = {}T
proof
{}T is closed_condensed by TDLAT_1:18;
then
A1: {}T in {A where A is Subset of T : A is closed_condensed};
then reconsider E = {}T as Element of Closed_Domains_of T by TDLAT_1:def 5;
{}T in Closed_Domains_of T by A1,TDLAT_1:def 5;
then reconsider e = {}T as Element of Closed_Domains_Lattice T by Th93;
for a being Element of Closed_Domains_Lattice T holds e "\/" a = a
proof
let a be Element of Closed_Domains_Lattice T;
reconsider A = a as Element of Closed_Domains_of T by Th93;
thus e "\/" a = E \/ A by Th94
.= a;
end;
hence thesis by LATTICE2:14;
end;
thus Top (Closed_Domains_Lattice T) = [#]T
proof
[#]T is closed_condensed by TDLAT_1:19;
then
A2: [#]T in {A where A is Subset of T : A is closed_condensed};
then reconsider E = [#]T as Element of Closed_Domains_of T by TDLAT_1:def 5
;
[#]T in Closed_Domains_of T by A2,TDLAT_1:def 5;
then reconsider e = [#]T as Element of Closed_Domains_Lattice T by Th93;
for a being Element of Closed_Domains_Lattice T holds e "/\" a = a
proof
let a be Element of Closed_Domains_Lattice T;
reconsider A = a as Element of Closed_Domains_of T by Th93;
A in Closed_Domains_of T;
then A in {C where C is Subset of T : C is closed_condensed} by
TDLAT_1:def 5;
then
A3: ex D being Subset of T st D = A & D is closed_condensed;
thus e "/\" a = Cl(Int(E /\ A)) by Th94
.= Cl(Int(A)) by XBOOLE_1:28
.= a by A3,TOPS_1:def 7;
end;
hence thesis by LATTICE2:16;
end;
end;
theorem Th96:
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
proof
let a, b be Element of Closed_Domains_Lattice T;
let A, B be Element of Closed_Domains_of T;
assume that
A1: a = A and
A2: b = B;
thus a [= b implies A c= B
proof
assume a [= b;
then a "\/" b = b by LATTICES:def 3;
then A \/ B = B by A1,A2,Th94;
hence thesis by XBOOLE_1:7;
end;
thus A c= B implies a [= b
proof
assume A c= B;
then A \/ B = B by XBOOLE_1:12;
then a "\/" b = b by A1,A2,Th94;
hence thesis by LATTICES:def 3;
end;
end;
theorem Th97:
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
proof
let X be Subset of Closed_Domains_Lattice T;
X c= the carrier of Closed_Domains_Lattice T;
then
A1: X c= Closed_Domains_of T by Th93;
then reconsider F = X as Subset-Family of T by TOPS_2:2;
set A = Cl(union F);
A2: F is closed-domains-family by A1,Th71;
then A is closed_condensed by Th75;
then A in {C where C is Subset of T : C is closed_condensed};
then
A3: A in Closed_Domains_of T by TDLAT_1:def 5;
then reconsider a = A as Element of Closed_Domains_Lattice T by Th93;
A4: for b being Element of Closed_Domains_Lattice T st X is_less_than b
holds a [= b
proof
let b be Element of Closed_Domains_Lattice T;
reconsider B = b as Element of Closed_Domains_of T by Th93;
assume
A5: X is_less_than b;
A6: for C being Subset of T st C in F holds C c= B
proof
let C be Subset of T;
reconsider C1 = C as Subset of T;
assume
A7: C in F;
then C1 is closed_condensed by A2;
then C in {P where P is Subset of T : P is closed_condensed};
then
A8: C in Closed_Domains_of T by TDLAT_1:def 5;
then reconsider c = C as Element of Closed_Domains_Lattice T by Th93;
c [= b by A5,A7;
hence thesis by A8,Th96;
end;
B in Closed_Domains_of T;
then B in {C where C is Subset of T : C is closed_condensed} by
TDLAT_1:def 5;
then ex C being Subset of T st C = B & C is closed_condensed;
then A c= B by A6,Th76;
hence thesis by A3,Th96;
end;
take a;
X is_less_than a
proof
let b be Element of Closed_Domains_Lattice T;
reconsider B = b as Element of Closed_Domains_of T by Th93;
assume b in X;
then B c= A by Th76;
hence thesis by A3,Th96;
end;
hence thesis by A4;
end;
theorem Th98:
Closed_Domains_Lattice T is complete
proof
thus for X being set 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
proof
let X be set;
set Y = { c where c is Element of Closed_Domains_Lattice T : c in X};
A1: for d being Element of Closed_Domains_Lattice T holds Y is_less_than d
implies X is_less_than d
proof
let d be Element of Closed_Domains_Lattice T;
assume
A2: Y is_less_than d;
thus for e being Element of Closed_Domains_Lattice T st e in X holds e
[= d
proof
let e be Element of Closed_Domains_Lattice T;
assume e in X;
then e in Y;
hence thesis by A2;
end;
end;
A3: for d being Element of Closed_Domains_Lattice T holds X is_less_than d
implies Y is_less_than d
proof
let d be Element of Closed_Domains_Lattice T;
assume
A4: X is_less_than d;
thus for e being Element of Closed_Domains_Lattice T st e in Y holds e
[= d
proof
let e be Element of Closed_Domains_Lattice T;
assume e in Y;
then
ex e0 being Element of Closed_Domains_Lattice T st e0 = e & e0 in X;
hence thesis by A4;
end;
end;
now
let x be object;
assume x in Y;
then ex y being Element of Closed_Domains_Lattice T st y = x & y in X;
hence x in the carrier of Closed_Domains_Lattice T;
end;
then reconsider Y as Subset of Closed_Domains_Lattice T by TARSKI:def 3;
consider a being Element of Closed_Domains_Lattice T such that
A5: Y is_less_than a and
A6: for b being Element of Closed_Domains_Lattice T st Y is_less_than
b holds a [= b by Th97;
take a;
for b being Element of Closed_Domains_Lattice T st X is_less_than b
holds a [= b by A3,A6;
hence thesis by A1,A5;
end;
end;
theorem
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)
proof
let F be Subset-Family of T;
assume
A1: F is closed-domains-family;
let X be Subset of Closed_Domains_Lattice T;
assume
A2: X = F;
thus "\/"(X,Closed_Domains_Lattice T) = Cl(union F)
proof
set A = Cl(union F);
A is closed_condensed by A1,Th75;
then A in {C where C is Subset of T : C is closed_condensed};
then
A3: A in Closed_Domains_of T by TDLAT_1:def 5;
then reconsider a = A as Element of Closed_Domains_Lattice T by Th93;
A4: X is_less_than a
proof
let b be Element of Closed_Domains_Lattice T;
reconsider B = b as Element of Closed_Domains_of T by Th93;
assume b in X;
then B c= A by A2,Th76;
hence thesis by A3,Th96;
end;
A5: for b being Element of Closed_Domains_Lattice T st X is_less_than b
holds a [= b
proof
let b be Element of Closed_Domains_Lattice T;
reconsider B = b as Element of Closed_Domains_of T by Th93;
assume
A6: X is_less_than b;
A7: for C being Subset of T st C in F holds C c= B
proof
let C be Subset of T;
reconsider C1 = C as Subset of T;
assume
A8: C in F;
then C1 is closed_condensed by A1;
then C in {P where P is Subset of T : P is closed_condensed};
then
A9: C in Closed_Domains_of T by TDLAT_1:def 5;
then reconsider c = C as Element of Closed_Domains_Lattice T by Th93;
c [= b by A2,A6,A8;
hence thesis by A9,Th96;
end;
B in Closed_Domains_of T;
then B in {C where C is Subset of T : C is closed_condensed} by
TDLAT_1:def 5;
then ex C being Subset of T st C = B & C is closed_condensed;
then A c= B by A7,Th76;
hence thesis by A3,Th96;
end;
Closed_Domains_Lattice T is complete by Th98;
hence thesis by A4,A5,LATTICE3:def 21;
end;
end;
theorem
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)
proof
let F be Subset-Family of T;
assume
A1: F is closed-domains-family;
let X be Subset of Closed_Domains_Lattice T;
assume
A2: X = F;
thus X <> {} implies "/\"(X,Closed_Domains_Lattice T) = Cl Int(meet F)
proof
set A = Cl Int(meet F);
A is closed_condensed by A1,Th75;
then A in {C where C is Subset of T : C is closed_condensed};
then
A3: A in Closed_Domains_of T by TDLAT_1:def 5;
then reconsider a = A as Element of Closed_Domains_Lattice T by Th93;
A4: a is_less_than X
proof
let b be Element of Closed_Domains_Lattice T;
reconsider B = b as Element of Closed_Domains_of T by Th93;
assume b in X;
then A c= B by A1,A2,Th73,Th77;
hence thesis by A3,Th96;
end;
assume
A5: X <> {};
A6: for b being Element of Closed_Domains_Lattice T st b is_less_than X
holds b [= a
proof
let b be Element of Closed_Domains_Lattice T;
reconsider B = b as Element of Closed_Domains_of T by Th93;
assume
A7: b is_less_than X;
A8: for C being Subset of T st C in F holds B c= C
proof
let C be Subset of T;
reconsider C1 = C as Subset of T;
assume
A9: C in F;
then C1 is closed_condensed by A1;
then C in {P where P is Subset of T : P is closed_condensed};
then
A10: C in Closed_Domains_of T by TDLAT_1:def 5;
then reconsider c = C as Element of Closed_Domains_Lattice T by Th93;
b [= c by A2,A7,A9;
hence thesis by A10,Th96;
end;
B in Closed_Domains_of T;
then B in {C where C is Subset of T : C is closed_condensed} by
TDLAT_1:def 5;
then ex C being Subset of T st C = B & C is closed_condensed;
then B c= A by A2,A5,A8,Th77;
hence thesis by A3,Th96;
end;
Closed_Domains_Lattice T is complete by Th98;
hence thesis by A4,A6,LATTICE3:34;
end;
thus X = {} implies "/\"(X,Closed_Domains_Lattice T) = [#]T
proof
set A = [#]T;
A is closed_condensed by TDLAT_1:19;
then A in {C where C is Subset of T : C is closed_condensed};
then
A11: A in Closed_Domains_of T by TDLAT_1:def 5;
then reconsider a = A as Element of Closed_Domains_Lattice T by Th93;
A12: for b being Element of Closed_Domains_Lattice T st b is_less_than X
holds b [= a
proof
let b be Element of Closed_Domains_Lattice T;
reconsider B = b as Element of Closed_Domains_of T by Th93;
assume b is_less_than X;
B c= A;
hence thesis by A11,Th96;
end;
assume
A13: X = {};
A14: a is_less_than X
by A13;
Closed_Domains_Lattice T is complete by Th98;
hence thesis by A14,A12,LATTICE3:34;
end;
end;
theorem
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)
proof
let F be Subset-Family of T;
A1: Cl Int(meet F) c= Cl(meet F) by PRE_TOPC:19,TOPS_1:16;
assume
A2: F is closed-domains-family;
then
A3: F is domains-family by Th72;
let X be Subset of Domains_Lattice T;
assume
A4: X = F;
meet F is closed by A2,Th73,TOPS_2:22;
then Cl Int(meet F) c= meet F by A1,PRE_TOPC:22;
then (meet F) /\ (Cl Int(meet F)) = Cl Int(meet F) by XBOOLE_1:28;
hence X <> {} implies "/\"(X,Domains_Lattice T) = Cl Int(meet F) by A3,A4
,Th92;
thus thesis by A3,A4,Th92;
end;
::The Lattice of Open Domains.
theorem Th102:
the carrier of Open_Domains_Lattice T = Open_Domains_of T
proof
Open_Domains_Lattice T = LattStr(#Open_Domains_of T,OPD-Union T,OPD-Meet
T#) by TDLAT_1:def 12;
hence thesis;
end;
theorem Th103:
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
proof
let a, b be Element of Open_Domains_Lattice T;
let A, B be Element of Open_Domains_of T;
assume that
A1: a = A and
A2: b = B;
A3: Open_Domains_Lattice T = LattStr(#Open_Domains_of T,OPD-Union T,OPD-Meet
T#) by TDLAT_1:def 12;
hence a "\/" b = (OPD-Union T).(A,B) by A1,A2,LATTICES:def 1
.= Int(Cl(A \/ B)) by TDLAT_1:def 10;
thus a "/\" b = (OPD-Meet T).(A,B) by A3,A1,A2,LATTICES:def 2
.= A /\ B by TDLAT_1:def 11;
end;
theorem
Bottom (Open_Domains_Lattice T) = {}T & Top (Open_Domains_Lattice T) = [#] T
proof
thus Bottom (Open_Domains_Lattice T) = {}T
proof
{}T is open_condensed by TDLAT_1:20;
then
A1: {}T in {A where A is Subset of T : A is open_condensed};
then reconsider E = {}T as Element of Open_Domains_of T by TDLAT_1:def 9;
{}T in Open_Domains_of T by A1,TDLAT_1:def 9;
then reconsider e = {}T as Element of Open_Domains_Lattice T by Th102;
for a being Element of Open_Domains_Lattice T holds e "\/" a = a
proof
let a be Element of Open_Domains_Lattice T;
reconsider A = a as Element of Open_Domains_of T by Th102;
A in Open_Domains_of T;
then A in {C where C is Subset of T : C is open_condensed} by
TDLAT_1:def 9;
then
A2: ex D being Subset of T st D = A & D is open_condensed;
thus e "\/" a = Int(Cl(E \/ A)) by Th103
.= a by A2,TOPS_1:def 8;
end;
hence thesis by LATTICE2:14;
end;
thus Top (Open_Domains_Lattice T) = [#]T
proof
[#]T is open_condensed by TDLAT_1:21;
then
A3: [#]T in {A where A is Subset of T : A is open_condensed};
then reconsider E = [#]T as Element of Open_Domains_of T by TDLAT_1:def 9;
[#]T in Open_Domains_of T by A3,TDLAT_1:def 9;
then reconsider e = [#]T as Element of Open_Domains_Lattice T by Th102;
for a being Element of Open_Domains_Lattice T holds e "/\" a = a
proof
let a be Element of Open_Domains_Lattice T;
reconsider A = a as Element of Open_Domains_of T by Th102;
thus e "/\" a = E /\ A by Th103
.= a by XBOOLE_1:28;
end;
hence thesis by LATTICE2:16;
end;
end;
theorem Th105:
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
proof
let a, b be Element of Open_Domains_Lattice T;
let A, B be Element of Open_Domains_of T;
reconsider A1 = A as Subset of T;
assume that
A1: a = A and
A2: b = B;
A in Open_Domains_of T;
then A in {C where C is Subset of T : C is open_condensed} by TDLAT_1:def 9;
then ex Q being Subset of T st Q = A & Q is open_condensed;
then
A3: A1 is open by TOPS_1:67;
thus a [= b implies A c= B
proof
assume a [= b;
then a "\/" b = b by LATTICES:def 3;
then Int(Cl(A \/ B)) = B by A1,A2,Th103;
hence thesis by A3,Th4;
end;
B in Open_Domains_of T;
then B in {C where C is Subset of T : C is open_condensed} by TDLAT_1:def 9;
then
A4: ex P being Subset of T st P = B & P is open_condensed;
thus A c= B implies a [= b
proof
assume A c= B;
then Int(Cl(A \/ B)) = B by A4,Th63;
then a "\/" b = b by A1,A2,Th103;
hence thesis by LATTICES:def 3;
end;
end;
theorem Th106:
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
proof
let X be Subset of Open_Domains_Lattice T;
X c= the carrier of Open_Domains_Lattice T;
then
A1: X c= Open_Domains_of T by Th102;
then reconsider F = X as Subset-Family of T by TOPS_2:2;
set A = Int Cl(union F);
A2: F is open-domains-family by A1,Th78;
then A is open_condensed by Th82;
then A in {C where C is Subset of T : C is open_condensed};
then
A3: A in Open_Domains_of T by TDLAT_1:def 9;
then reconsider a = A as Element of Open_Domains_Lattice T by Th102;
A4: for b being Element of Open_Domains_Lattice T st X is_less_than b holds
a [= b
proof
let b be Element of Open_Domains_Lattice T;
reconsider B = b as Element of Open_Domains_of T by Th102;
assume
A5: X is_less_than b;
A6: for C being Subset of T st C in F holds C c= B
proof
let C be Subset of T;
reconsider C1 = C as Subset of T;
assume
A7: C in F;
then C1 is open_condensed by A2;
then C in {P where P is Subset of T : P is open_condensed};
then
A8: C in Open_Domains_of T by TDLAT_1:def 9;
then reconsider c = C as Element of Open_Domains_Lattice T by Th102;
c [= b by A5,A7;
hence thesis by A8,Th105;
end;
B in Open_Domains_of T;
then B in {C where C is Subset of T : C is open_condensed} by TDLAT_1:def 9
;
then ex C being Subset of T st C = B & C is open_condensed;
then A c= B by A6,Th83;
hence thesis by A3,Th105;
end;
take a;
X is_less_than a
proof
let b be Element of Open_Domains_Lattice T;
reconsider B = b as Element of Open_Domains_of T by Th102;
assume b in X;
then B c= A by A2,Th80,Th83;
hence thesis by A3,Th105;
end;
hence thesis by A4;
end;
theorem Th107:
Open_Domains_Lattice T is complete
proof
thus for X being set 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
proof
let X be set;
set Y = { c where c is Element of Open_Domains_Lattice T : c in X};
A1: for d being Element of Open_Domains_Lattice T holds Y is_less_than d
implies X is_less_than d
proof
let d be Element of Open_Domains_Lattice T;
assume
A2: Y is_less_than d;
thus for e being Element of Open_Domains_Lattice T st e in X holds e [= d
proof
let e be Element of Open_Domains_Lattice T;
assume e in X;
then e in Y;
hence thesis by A2;
end;
end;
A3: for d being Element of Open_Domains_Lattice T holds X is_less_than d
implies Y is_less_than d
proof
let d be Element of Open_Domains_Lattice T;
assume
A4: X is_less_than d;
thus for e being Element of Open_Domains_Lattice T st e in Y holds e [= d
proof
let e be Element of Open_Domains_Lattice T;
assume e in Y;
then
ex e0 being Element of Open_Domains_Lattice T st e0 = e & e0 in X;
hence thesis by A4;
end;
end;
now
let x be object;
assume x in Y;
then ex y being Element of Open_Domains_Lattice T st y = x & y in X;
hence x in the carrier of Open_Domains_Lattice T;
end;
then reconsider Y as Subset of Open_Domains_Lattice T by TARSKI:def 3;
consider a being Element of Open_Domains_Lattice T such that
A5: Y is_less_than a and
A6: for b being Element of Open_Domains_Lattice T st Y is_less_than b
holds a [= b by Th106;
take a;
for b being Element of Open_Domains_Lattice T st X is_less_than b
holds a [= b by A3,A6;
hence thesis by A1,A5;
end;
end;
theorem
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)
proof
let F be Subset-Family of T;
assume
A1: F is open-domains-family;
let X be Subset of Open_Domains_Lattice T;
assume
A2: X = F;
thus "\/"(X,Open_Domains_Lattice T) = Int Cl(union F)
proof
set A = Int Cl(union F);
A is open_condensed by A1,Th82;
then A in {C where C is Subset of T : C is open_condensed};
then
A3: A in Open_Domains_of T by TDLAT_1:def 9;
then reconsider a = A as Element of Open_Domains_Lattice T by Th102;
A4: X is_less_than a
proof
let b be Element of Open_Domains_Lattice T;
reconsider B = b as Element of Open_Domains_of T by Th102;
assume b in X;
then B c= A by A1,A2,Th80,Th83;
hence thesis by A3,Th105;
end;
A5: for b being Element of Open_Domains_Lattice T st X is_less_than b
holds a [= b
proof
let b be Element of Open_Domains_Lattice T;
reconsider B = b as Element of Open_Domains_of T by Th102;
assume
A6: X is_less_than b;
A7: for C being Subset of T st C in F holds C c= B
proof
let C be Subset of T;
reconsider C1 = C as Subset of T;
assume
A8: C in F;
then C1 is open_condensed by A1;
then C in {P where P is Subset of T : P is open_condensed};
then
A9: C in Open_Domains_of T by TDLAT_1:def 9;
then reconsider c = C as Element of Open_Domains_Lattice T by Th102;
c [= b by A2,A6,A8;
hence thesis by A9,Th105;
end;
B in Open_Domains_of T;
then B in {C where C is Subset of T : C is open_condensed} by
TDLAT_1:def 9;
then ex C being Subset of T st C = B & C is open_condensed;
then A c= B by A7,Th83;
hence thesis by A3,Th105;
end;
Open_Domains_Lattice T is complete by Th107;
hence thesis by A4,A5,LATTICE3:def 21;
end;
end;
theorem
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)
proof
let F be Subset-Family of T;
assume
A1: F is open-domains-family;
let X be Subset of Open_Domains_Lattice T;
assume
A2: X = F;
thus X <> {} implies "/\"(X,Open_Domains_Lattice T) = Int(meet F)
proof
set A = Int(meet F);
A is open_condensed by A1,Th82;
then A in {C where C is Subset of T : C is open_condensed};
then
A3: A in Open_Domains_of T by TDLAT_1:def 9;
then reconsider a = A as Element of Open_Domains_Lattice T by Th102;
A4: a is_less_than X
proof
let b be Element of Open_Domains_Lattice T;
reconsider B = b as Element of Open_Domains_of T by Th102;
assume b in X;
then A c= B by A2,Th84;
hence thesis by A3,Th105;
end;
assume
A5: X <> {};
A6: for b being Element of Open_Domains_Lattice T st b is_less_than X
holds b [= a
proof
let b be Element of Open_Domains_Lattice T;
reconsider B = b as Element of Open_Domains_of T by Th102;
assume
A7: b is_less_than X;
A8: for C being Subset of T st C in F holds B c= C
proof
let C be Subset of T;
reconsider C1 = C as Subset of T;
assume
A9: C in F;
then C1 is open_condensed by A1;
then C in {P where P is Subset of T : P is open_condensed};
then
A10: C in Open_Domains_of T by TDLAT_1:def 9;
then reconsider c = C as Element of Open_Domains_Lattice T by Th102;
b [= c by A2,A7,A9;
hence thesis by A10,Th105;
end;
B in Open_Domains_of T;
then B in {C where C is Subset of T : C is open_condensed} by
TDLAT_1:def 9;
then ex C being Subset of T st C = B & C is open_condensed;
then B c= A by A2,A5,A8,Th84;
hence thesis by A3,Th105;
end;
Open_Domains_Lattice T is complete by Th107;
hence thesis by A4,A6,LATTICE3:34;
end;
thus X = {} implies "/\"(X,Open_Domains_Lattice T) = [#]T
proof
set A = [#]T;
A is open_condensed by TDLAT_1:21;
then A in {C where C is Subset of T : C is open_condensed};
then
A11: A in Open_Domains_of T by TDLAT_1:def 9;
then reconsider a = A as Element of Open_Domains_Lattice T by Th102;
A12: for b being Element of Open_Domains_Lattice T st b is_less_than X
holds b [= a
proof
let b be Element of Open_Domains_Lattice T;
reconsider B = b as Element of Open_Domains_of T by Th102;
assume b is_less_than X;
B c= A;
hence thesis by A11,Th105;
end;
assume
A13: X = {};
A14: a is_less_than X
by A13;
Open_Domains_Lattice T is complete by Th107;
hence thesis by A14,A12,LATTICE3:34;
end;
end;
theorem
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)
proof
let F be Subset-Family of T;
A1: Int(union F) c= Int Cl(union F) by PRE_TOPC:18,TOPS_1:19;
assume
A2: F is open-domains-family;
then union F is open by Th80,TOPS_2:19;
then union F c= Int Cl(union F) by A1,TOPS_1:23;
then
A3: (union F) \/ Int Cl(union F) = Int Cl(union F) by XBOOLE_1:12;
let X be Subset of Domains_Lattice T;
assume X = F;
hence thesis by A2,A3,Th79,Th91;
end;