:: The Lattice of Domains of an Extremally Disconnected Space
:: by Zbigniew Karno
::
:: Received August 27, 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, XBOOLE_0, STRUCT_0, RCOMP_1, TARSKI,
NATTRA_1, ZFMISC_1, SETFAM_1, TDLAT_1, REALSET1, LATTICES, FUNCT_1,
EQREL_1, TDLAT_2, PBOOLE, TDLAT_3;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, STRUCT_0, REALSET1, PRE_TOPC,
TOPS_1, TOPS_2, BORSUK_1, TSEP_1, BINOP_1, LATTICES, LATTICE3, TDLAT_1,
TDLAT_2;
constructors SETFAM_1, REALSET1, TOPS_1, TOPS_2, BORSUK_1, LATTICE3, TDLAT_1,
TDLAT_2, TSEP_1, BINOP_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, LATTICES, PRE_TOPC,
TOPS_1, BORSUK_1, TSEP_1;
requirements BOOLE, SUBSET;
definitions TARSKI, XBOOLE_0;
equalities REALSET1, SUBSET_1, STRUCT_0, TDLAT_1;
expansions TARSKI, BORSUK_1, TSEP_1, XBOOLE_0;
theorems TARSKI, ZFMISC_1, PRE_TOPC, TOPS_1, TOPS_2, PCOMPS_1, BORSUK_1,
TSEP_1, LATTICES, TDLAT_1, TDLAT_2, SUBSET_1, XBOOLE_0, XBOOLE_1,
RELSET_1;
begin
:: 1. Selected Properties of Subsets of a Topological Space.
reserve X for TopSpace;
::Properties of the Closure and the Interior Operators.
reserve C for Subset of X;
theorem Th1:
Cl C = (Int C`)`
proof
thus Cl C = (Cl((C``)))`` .= (Int (C`))` by TOPS_1:def 1;
end;
theorem Th2:
Cl C` = (Int C)`
proof
thus Cl C` = (Int ( C``))` by Th1
.= (Int C)`;
end;
theorem Th3:
Int C` = (Cl C)`
proof
thus Int C` = (Cl ( C``))` by TOPS_1:def 1
.= (Cl C)`;
end;
reserve A, B for Subset of X;
theorem
A \/ B = the carrier of X implies (A is closed implies A \/ Int B =
the carrier of X)
proof
assume A \/ B = the carrier of X;
then (A \/ B)` = {}X by XBOOLE_1:37;
then ( A`) /\ B` = {} by XBOOLE_1:53;
then
A1: ( A`) misses B`;
assume A is closed;
then ( A`) misses Cl B` by A1,TSEP_1:36;
then ( A`) /\ (Cl B`)`` = {};
then ( A`) /\ ((Int B)`) = {} by TOPS_1:def 1;
then (A \/ Int B)` = {}X by XBOOLE_1:53;
then (A \/ Int B)`` = [#]X;
hence thesis;
end;
theorem Th5:
A is open closed iff Cl A = Int A
proof
thus A is open & A is closed implies Cl A = Int A
proof
assume that
A1: A is open and
A2: A is closed;
Int A = A by A1,TOPS_1:23;
hence thesis by A2,PRE_TOPC:22;
end;
A3: Int A c= A by TOPS_1:16;
A4: A c= Cl A by PRE_TOPC:18;
assume Cl A = Int A;
hence thesis by A3,A4,XBOOLE_0:def 10;
end;
theorem
A is open & A is closed implies Int Cl A = Cl Int A
proof
assume that
A1: A is open and
A2: A is closed;
A3: Cl A = A by A2,PRE_TOPC:22;
Int A = A by A1,TOPS_1:23;
hence thesis by A3;
end;
::Properties of Domains.
theorem Th7:
A is condensed & Cl Int A c= Int Cl A implies A is open_condensed
& A is closed_condensed
proof
assume
A1: A is condensed;
then
A2: Int Cl A c= A by TOPS_1:def 6;
A3: A c= Cl Int A by A1,TOPS_1:def 6;
assume
A4: Cl Int A c= Int Cl A;
then Cl Int A c= A by A2;
then
A5: A = Cl Int A by A3;
A c= Int Cl A by A3,A4;
then A = Int Cl A by A2;
hence thesis by A5,TOPS_1:def 7,def 8;
end;
theorem Th8:
A is condensed & Cl Int A c= Int Cl A implies A is open & A is closed
proof
assume that
A1: A is condensed and
A2: Cl Int A c= Int Cl A;
A3: A is closed_condensed by A1,A2,Th7;
A is open_condensed by A1,A2,Th7;
hence thesis by A3,TOPS_1:66,67;
end;
theorem Th9:
A is condensed implies Int Cl A = Int A & Cl A = Cl Int A
proof
A1: Cl Int A c= Cl A by PRE_TOPC:19,TOPS_1:16;
assume
A2: A is condensed;
then Int Cl A c= A by TOPS_1:def 6;
then
A3: Int Int Cl A c= Int A by TOPS_1:19;
A c= Cl Int A by A2,TOPS_1:def 6;
then
A4: Cl A c= Cl Cl Int A by PRE_TOPC:19;
Int A c= Int Cl A by PRE_TOPC:18,TOPS_1:19;
hence thesis by A3,A4,A1;
end;
begin
:: 2. Discrete Topological Structures.
definition
let IT be TopStruct;
attr IT is discrete means
:Def1:
the topology of IT = bool the carrier of IT;
attr IT is anti-discrete means
:Def2:
the topology of IT = {{}, the carrier of IT};
end;
theorem
for Y being TopStruct holds Y is discrete & Y is anti-discrete implies
bool the carrier of Y = {{}, the carrier of Y};
theorem Th11:
for Y being TopStruct st {} in the topology of Y & the carrier
of Y in the topology of Y holds bool the carrier of Y = {{}, the carrier of Y}
implies Y is discrete & Y is anti-discrete
proof
let Y be TopStruct;
assume that
A1: {} in the topology of Y and
A2: the carrier of Y in the topology of Y;
assume
A3: bool the carrier of Y = {{}, the carrier of Y};
{{}, the carrier of Y} c= the topology of Y by A1,A2,ZFMISC_1:32;
then the topology of Y = bool the carrier of Y by A3;
hence thesis by A3;
end;
registration
cluster discrete anti-discrete strict non empty for TopStruct;
existence
proof
set one = {{}};
reconsider tau = bool one as Subset-Family of one;
take Y = TopStruct (#one,tau#);
thus Y is discrete;
tau = {{},one} by ZFMISC_1:24;
hence Y is anti-discrete;
thus thesis;
end;
end;
theorem
for Y being discrete TopStruct, A being Subset of Y holds (the
carrier of Y) \ A in the topology of Y
proof
let Y be discrete TopStruct, A be Subset of Y;
the topology of Y = bool the carrier of Y by Def1;
hence thesis;
end;
theorem Th13:
for Y being anti-discrete TopStruct, A being Subset of Y st A in
the topology of Y holds (the carrier of Y) \ A in the topology of Y
proof
let Y be anti-discrete TopStruct, A be Subset of Y;
A1: the topology of Y = {{}, the carrier of Y} by Def2;
assume A in the topology of Y;
then A = {} or A = the carrier of Y by A1,TARSKI:def 2;
then
(the carrier of Y) \ A = the carrier of Y or (the carrier of Y) \ A = {}
by XBOOLE_1:37;
hence thesis by A1,TARSKI:def 2;
end;
registration
cluster discrete -> TopSpace-like for TopStruct;
coherence
proof
let Y be TopStruct;
assume Y is discrete;
then
A1: the topology of Y = bool the carrier of Y;
then
A2: for F being Subset-Family of Y st F c= the topology of Y holds union F
in the topology of Y;
A3: for A,B being Subset of Y st A in the topology of Y & B in the
topology of Y holds A /\ B in the topology of Y by A1;
the carrier of Y in the topology of Y by A1,ZFMISC_1:def 1;
hence thesis by A2,A3,PRE_TOPC:def 1;
end;
cluster anti-discrete -> TopSpace-like for TopStruct;
coherence
proof
let Y be TopStruct;
assume Y is anti-discrete;
then
A4: the topology of Y = {{}, the carrier of Y};
A5: for A,B being Subset of Y st A in the topology of Y & B in the
topology of Y holds A /\ B in the topology of Y
proof
let A,B be Subset of Y;
assume that
A6: A in the topology of Y and
A7: B in the topology of Y;
A8: B = {} or B = the carrier of Y by A4,A7,TARSKI:def 2;
A = {} or A = the carrier of Y by A4,A6,TARSKI:def 2;
hence thesis by A4,A8,TARSKI:def 2;
end;
A9: for F being Subset-Family of Y st F c= the topology of Y holds union F
in the topology of Y
proof
let F be Subset-Family of Y;
assume F c= the topology of Y;
then
F = {} or F = {{}} or F = {the carrier of Y} or F = {{},the carrier
of Y} by A4,ZFMISC_1:36;
then union F = {} or union F = the carrier of Y or union F = {} \/ (the
carrier of Y) by ZFMISC_1:2,25,75;
hence thesis by A4,TARSKI:def 2;
end;
the carrier of Y in the topology of Y by A4,TARSKI:def 2;
hence thesis by A9,A5,PRE_TOPC:def 1;
end;
end;
theorem
for Y being TopSpace-like TopStruct holds bool the carrier of Y = {{},
the carrier of Y} implies Y is discrete & Y is anti-discrete
proof
let Y be TopSpace-like TopStruct;
reconsider E = {} as Subset-Family of Y by XBOOLE_1:2;
reconsider E as Subset-Family of Y;
A1: the carrier of Y in the topology of Y by PRE_TOPC:def 1;
E c= the topology of Y;
then
A2: {} in the topology of Y by PRE_TOPC:def 1,ZFMISC_1:2;
assume bool the carrier of Y = {{}, the carrier of Y};
hence thesis by A2,A1,Th11;
end;
definition
let IT be TopStruct;
attr IT is almost_discrete means
for A being Subset of IT st A in the
topology of IT holds (the carrier of IT) \ A in the topology of IT;
end;
registration
cluster discrete -> almost_discrete for TopStruct;
coherence;
cluster anti-discrete -> almost_discrete for TopStruct;
coherence
by Th13;
end;
registration
cluster almost_discrete strict for TopStruct;
existence
proof
set Y = the discrete strict TopStruct;
take Y;
thus thesis;
end;
end;
begin
:: 3. Discrete Topological Spaces.
registration
cluster discrete anti-discrete strict non empty for TopSpace;
existence
proof
set X = the discrete anti-discrete strict non empty TopStruct;
reconsider X as TopSpace;
take X;
thus thesis;
end;
end;
theorem Th15:
X is discrete iff for A being Subset of X holds A is open
proof
thus X is discrete implies for A being Subset of X holds A is open
by PRE_TOPC:def 2;
assume for A being Subset of X holds A is open;
then for V being object
holds V in the topology of X iff V in bool the carrier of X
by PRE_TOPC:def 2;
then the topology of X = bool the carrier of X by TARSKI:2;
hence thesis;
end;
theorem Th16:
X is discrete iff for A being Subset of X holds A is closed
proof
thus X is discrete implies for A being Subset of X holds A is closed
proof
assume
A1: X is discrete;
let A be Subset of X;
A` is open by A1,Th15;
hence thesis by TOPS_1:3;
end;
assume
A2: for A being Subset of X holds A is closed;
now
let A be Subset of X;
A` is closed by A2;
hence A is open by TOPS_1:4;
end;
hence thesis by Th15;
end;
theorem Th17:
(for A being Subset of X, x being Point of X st A = {x} holds A
is open) implies X is discrete
proof
assume
A1: for A being Subset of X, x being Point of X st A = {x} holds A is open;
now
let A be Subset of X;
set F = {B where B is Subset of X : ex a being Point of X st a in A & B =
{a}};
A2: F c= bool A
proof
let x be object;
assume x in F;
then consider C being Subset of X such that
A3: x = C and
A4: ex a being Point of X st a in A & C = {a};
C c= A by A4,ZFMISC_1:31;
hence thesis by A3;
end;
bool A c= bool the carrier of X by ZFMISC_1:67;
then reconsider F as Subset-Family of X by A2,XBOOLE_1:1;
A5: union bool A = A by ZFMISC_1:81;
now
let x be set;
assume
A6: x in bool A;
then reconsider P = x as Subset of X by XBOOLE_1:1;
now
let y be object;
assume
A7: y in P;
then reconsider a = y as Point of X;
now
take B0 = {a};
B0 is Subset of X by A7,ZFMISC_1:31;
hence y in B0 & B0 in F by A6,A7,TARSKI:def 1;
end;
hence y in union F by TARSKI:def 4;
end;
hence x c= union F;
end;
then
A8: union bool A c= union F;
now
let B be Subset of X;
assume B in F;
then
ex C being Subset of X st C = B & ex a being Point of X st a in A &
C = {a};
hence B is open by A1;
end;
then
A9: F is open by TOPS_2:def 1;
union F c= union bool A by A2,ZFMISC_1:77;
then union F = A by A8,A5;
hence A is open by A9,TOPS_2:19;
end;
hence thesis by Th15;
end;
registration
let X be discrete non empty TopSpace;
cluster -> open closed discrete for SubSpace of X;
coherence
proof
let X0 be SubSpace of X;
thus X0 is open
by Th15;
thus X0 is closed
by Th16;
A1: the topology of X = bool the carrier of X by Def1;
now
let S be object;
assume S in bool the carrier of X0;
then reconsider A = S as Subset of X0;
the carrier of X0 c= the carrier of X by BORSUK_1:1;
then reconsider B = A as Subset of X by XBOOLE_1:1;
now
take B;
thus B in the topology of X & A = B /\ [#]X0 by A1,XBOOLE_1:28;
end;
hence S in the topology of X0 by PRE_TOPC:def 4;
end;
then bool the carrier of X0 c= the topology of X0;
hence the topology of X0 = bool the carrier of X0;
end;
end;
registration
let X be discrete non empty TopSpace;
cluster discrete strict for SubSpace of X;
existence
proof
set X0 = the strict SubSpace of X;
take X0;
thus thesis;
end;
end;
theorem Th18:
X is anti-discrete iff for A being Subset of X st A is open
holds A = {} or A = the carrier of X
proof
A1: the carrier of X in the topology of X by PRE_TOPC:def 1;
thus X is anti-discrete implies for A being Subset of X st A is open holds A
= {} or A = the carrier of X
proof
assume
A2: X is anti-discrete;
let A be Subset of X;
assume A is open;
then A in the topology of X by PRE_TOPC:def 2;
then A in {{}, the carrier of X} by A2;
hence thesis by TARSKI:def 2;
end;
assume
A3: for A being Subset of X st A is open holds A = {} or A = the carrier of X;
now
let P be object;
assume
A4: P in the topology of X;
then reconsider C = P as Subset of X;
C is open by A4,PRE_TOPC:def 2;
then C = {} or C = the carrier of X by A3;
hence P in {{}, the carrier of X} by TARSKI:def 2;
end;
then
A5: the topology of X c= {{}, the carrier of X};
{} in the topology of X by PRE_TOPC:1;
then {{}, the carrier of X} c= the topology of X by A1,ZFMISC_1:32;
then the topology of X = {{}, the carrier of X} by A5;
hence thesis;
end;
theorem Th19:
X is anti-discrete iff for A being Subset of X st A is closed
holds A = {} or A = the carrier of X
proof
thus X is anti-discrete implies for A being Subset of X st A is closed holds
A = {} or A = the carrier of X
proof
assume
A1: X is anti-discrete;
let A be Subset of X;
assume A is closed;
then A` = {} or A` = the carrier of X by A1,Th18;
then A`` = [#]X or A`` = {}X by XBOOLE_1:37;
hence thesis;
end;
assume
A2: for A being Subset of X st A is closed holds A = {} or A = the
carrier of X;
now
let B be Subset of X;
assume B is open;
then B` = {} or B` = the carrier of X by A2;
then B`` = [#]X or B`` = {}X by XBOOLE_1:37;
hence B = {} or B = the carrier of X;
end;
hence thesis by Th18;
end;
theorem
(for A being Subset of X, x being Point of X st A = {x} holds Cl A =
the carrier of X) implies X is anti-discrete
proof
assume
A1: for A being Subset of X, x being Point of X st A = {x} holds Cl A =
the carrier of X;
for B being Subset of X st B is closed holds B = {} or B = the carrier of X
proof
let B be Subset of X;
assume
A2: B is closed;
set z = the Element of B;
assume
A3: B <> {};
then reconsider x = z as Point of X by TARSKI:def 3;
A4: {x} c= B by A3,ZFMISC_1:31;
then reconsider A = {x} as Subset of X by XBOOLE_1:1;
Cl A = the carrier of X by A1;
then the carrier of X c= B by A2,A4,TOPS_1:5;
hence thesis;
end;
hence thesis by Th19;
end;
registration
let X be anti-discrete non empty TopSpace;
cluster -> anti-discrete for SubSpace of X;
coherence
proof
let X0 be SubSpace of X;
A1: the topology of X = {{}, the carrier of X} by Def2;
now
let S be object;
assume
A2: S in the topology of X0;
then reconsider A = S as Subset of X0;
consider B being Subset of X such that
A3: B in the topology of X and
A4: A = B /\ [#] X0 by A2,PRE_TOPC:def 4;
A5: B = the carrier of X implies A = the carrier of X0 by A4,BORSUK_1:1
,XBOOLE_1:28;
B = {} implies A = {} by A4;
hence S in {{}, the carrier of X0} by A1,A3,A5,TARSKI:def 2;
end;
then
A6: the topology of X0 c= {{}, the carrier of X0};
now
let S be object;
assume S in {{}, the carrier of X0};
then S = {} or S = the carrier of X0 by TARSKI:def 2;
hence S in the topology of X0 by PRE_TOPC:1,def 1;
end;
then {{}, the carrier of X0} c= the topology of X0;
then the topology of X0 = {{}, the carrier of X0} by A6;
hence thesis;
end;
end;
registration
let X be anti-discrete non empty TopSpace;
cluster anti-discrete for SubSpace of X;
existence
proof
set X0 = the SubSpace of X;
take X0;
thus thesis;
end;
end;
theorem Th21:
X is almost_discrete iff for A being Subset of X st A is open
holds A is closed
proof
thus X is almost_discrete implies for A being Subset of X st A is open holds
A is closed
proof
assume
A1: X is almost_discrete;
now
let A be Subset of X;
assume A is open;
then A in the topology of X by PRE_TOPC:def 2;
then (the carrier of X) \ A in the topology of X by A1;
then [#]X \ A is open by PRE_TOPC:def 2;
hence A is closed by PRE_TOPC:def 3;
end;
hence thesis;
end;
assume
A2: for A being Subset of X st A is open holds A is closed;
now
let A be Subset of X;
reconsider A9 = A as Subset of X;
assume A in the topology of X;
then A9 is open by PRE_TOPC:def 2;
then A9 is closed by A2;
then [#]X \ A9 is open by PRE_TOPC:def 3;
hence (the carrier of X) \ A in the topology of X by PRE_TOPC:def 2;
end;
hence thesis;
end;
theorem Th22:
X is almost_discrete iff for A being Subset of X st A is closed
holds A is open
proof
thus X is almost_discrete implies for A being Subset of X st A is closed
holds A is open
proof
assume
A1: X is almost_discrete;
let A be Subset of X;
assume A is closed;
then A` is closed by A1,Th21;
hence thesis by TOPS_1:4;
end;
assume
A2: for A being Subset of X st A is closed holds A is open;
now
let A be Subset of X;
assume A is open;
then A` is open by A2;
hence A is closed by TOPS_1:3;
end;
hence thesis by Th21;
end;
theorem
X is almost_discrete iff for A being Subset of X st A is open holds Cl A = A
proof
thus X is almost_discrete implies for A being Subset of X st A is open holds
Cl A = A
by Th21,PRE_TOPC:22;
assume
A1: for A being Subset of X st A is open holds Cl A = A;
now
let A be Subset of X;
assume A is open;
then Cl A = A by A1;
hence A is closed;
end;
hence thesis by Th21;
end;
theorem
X is almost_discrete iff for A being Subset of X st A is closed holds
Int A = A
proof
thus X is almost_discrete implies for A being Subset of X st A is closed
holds Int A = A
by Th22,TOPS_1:23;
assume
A1: for A being Subset of X st A is closed holds Int A = A;
now
let A be Subset of X;
assume A is closed;
then Int A = A by A1;
hence A is open;
end;
hence thesis by Th22;
end;
registration
cluster almost_discrete strict for TopSpace;
existence
proof
set X = the discrete strict TopSpace;
take X;
thus thesis;
end;
end;
theorem
(for A being Subset of X, x being Point of X st A = {x} holds Cl A is
open) implies X is almost_discrete
proof
assume
A1: for D being Subset of X, x being Point of X st D = {x} holds Cl D is open;
for A being Subset of X st A is closed holds A is open
proof
let A be Subset of X;
set F = {B where B is Subset of X : ex C being Subset of X, a being Point
of X st a in A & C = {a} & B = Cl C};
A2: union bool A = A by ZFMISC_1:81;
assume
A3: A is closed;
A4: for C being Subset of X, a being Point of X st a in A & C = {a} holds
Cl C c= A
proof
let C be Subset of X, a be Point of X;
assume that
A5: a in A and
A6: C = {a};
C c= A by A5,A6,ZFMISC_1:31;
then Cl C c= Cl A by PRE_TOPC:19;
hence thesis by A3,PRE_TOPC:22;
end;
A7: F c= bool A
proof
let x be object;
assume x in F;
then consider P being Subset of X such that
A8: x = P and
A9: ex C being Subset of X, a being Point of X st a in A & C = {a}
& P = Cl C;
P c= A by A4,A9;
hence thesis by A8;
end;
bool A c= bool the carrier of X by ZFMISC_1:67;
then reconsider F as Subset-Family of X by A7,XBOOLE_1:1;
now
let x be set;
assume
A10: x in bool A;
then reconsider P = x as Subset of X by XBOOLE_1:1;
now
let y be object;
assume
A11: y in P;
then reconsider a = y as Point of X;
now
reconsider P0 = {a} as Subset of X by A11,ZFMISC_1:31;
take B = Cl P0;
A12: P0 c= B by PRE_TOPC:18;
a in P0 by TARSKI:def 1;
hence y in B & B in F by A10,A11,A12;
end;
hence y in union F by TARSKI:def 4;
end;
hence x c= union F;
end;
then
A13: union bool A c= union F;
now
let D be Subset of X;
assume D in F;
then ex S being Subset of X st S = D & ex C being Subset of X, a being
Point of X st a in A & C = {a} & S = Cl C;
hence D is open by A1;
end;
then
A14: F is open by TOPS_2:def 1;
union F c= union bool A by A7,ZFMISC_1:77;
then union F = A by A13,A2;
hence thesis by A14,TOPS_2:19;
end;
hence thesis by Th22;
end;
theorem
X is discrete iff X is almost_discrete & for A being Subset of X, x
being Point of X st A = {x} holds A is closed
proof
thus X is discrete implies X is almost_discrete & for A being Subset of X, x
being Point of X st A = {x} holds A is closed by Th16;
assume
A1: X is almost_discrete;
assume
A2: for A being Subset of X, x being Point of X st A = {x} holds A is closed;
for A being Subset of X, x being Point of X st A = {x} holds A is open
by A2,A1,Th22;
hence thesis by Th17;
end;
registration
cluster discrete -> almost_discrete for TopSpace;
coherence;
cluster anti-discrete -> almost_discrete for TopSpace;
coherence;
end;
registration
let X be almost_discrete non empty TopSpace;
cluster -> almost_discrete for non empty SubSpace of X;
coherence
proof
let X0 be non empty SubSpace of X;
now
let A0 be Subset of X0;
assume A0 is open;
then consider A being Subset of X such that
A1: A is open and
A2: A0 = A /\ [#]X0 by TOPS_2:24;
A is closed by A1,Th21;
hence A0 is closed by A2,PRE_TOPC:13;
end;
hence thesis by Th21;
end;
end;
registration
let X be almost_discrete non empty TopSpace;
cluster open -> closed for SubSpace of X;
coherence
by Th21;
cluster closed -> open for SubSpace of X;
coherence
by Th22;
end;
registration
let X be almost_discrete non empty TopSpace;
cluster almost_discrete strict non empty for SubSpace of X;
existence
proof
set X0 = the strict non empty SubSpace of X;
take X0;
thus thesis;
end;
end;
begin
:: 4. Extremally Disconnected Topological Spaces.
definition
let IT be non empty TopSpace;
attr IT is extremally_disconnected means
:Def4:
for A being Subset of IT st A is open holds Cl A is open;
end;
registration
cluster extremally_disconnected strict for non empty TopSpace;
existence
proof
set X = the discrete strict non empty TopSpace;
take X;
for A being Subset of X st A is open
holds Cl A is open by PRE_TOPC:22,Th16;
hence thesis;
end;
end;
reserve X for non empty TopSpace;
theorem Th27:
X is extremally_disconnected iff for A being Subset of X st A is
closed holds Int A is closed
proof
thus X is extremally_disconnected implies for A being Subset of X st A is
closed holds Int A is closed
proof
assume
A1: X is extremally_disconnected;
let A be Subset of X;
assume A is closed;
then Cl A` is open by A1;
then (Cl A`)` is closed;
hence thesis by TOPS_1:def 1;
end;
assume
A2: for A being Subset of X st A is closed holds Int A is closed;
now
let A be Subset of X;
assume A is open;
then Int A` is closed by A2;
then (Int A`)` is open;
hence Cl A is open by Th1;
end;
hence thesis;
end;
theorem Th28:
X is extremally_disconnected iff for A, B being Subset of X st A
is open & B is open holds A misses B implies Cl A misses Cl B
proof
thus X is extremally_disconnected implies for A, B being Subset of X st A is
open & B is open holds A misses B implies Cl A misses Cl B
proof
assume
A1: X is extremally_disconnected;
let A, B be Subset of X;
assume that
A2: A is open and
A3: B is open;
assume A misses B;
then
A4: A misses Cl B by A2,TSEP_1:36;
Cl B is open by A1,A3;
hence thesis by A4,TSEP_1:36;
end;
assume
A5: for A, B being Subset of X st A is open & B is open holds A misses B
implies Cl A misses Cl B;
now
let A be Subset of X;
A c= Cl A by PRE_TOPC:18;
then
A6: A misses (Cl A)` by SUBSET_1:24;
assume A is open;
then (Cl A) misses Cl (Cl A)` by A5,A6;
then Cl A c= (Cl (Cl A)`)` by SUBSET_1:23;
then
A7: Cl A c= Int Cl A by TOPS_1:def 1;
Int Cl A c= Cl A by TOPS_1:16;
hence Cl A is open by A7,XBOOLE_0:def 10;
end;
hence thesis;
end;
theorem
X is extremally_disconnected iff for A, B being Subset of X st A is
closed & B is closed holds A \/ B = the carrier of X implies (Int A) \/ (Int B)
= the carrier of X
proof
thus X is extremally_disconnected implies for A, B being Subset of X st A is
closed & B is closed holds A \/ B = the carrier of X implies (Int A) \/ (Int B)
= the carrier of X
proof
assume
A1: X is extremally_disconnected;
let A, B be Subset of X;
assume that
A2: A is closed and
A3: B is closed;
assume A \/ B = the carrier of X;
then (A \/ B)` = {}X by XBOOLE_1:37;
then ( A`) /\ B` = {}X by XBOOLE_1:53;
then ( A`) misses B`;
then (Cl A`) misses (Cl B`) by A1,A2,A3,Th28;
then (Cl A`) /\ (Cl B`) = {}X;
then ((Cl A`) /\ (Cl B`))` = [#]X;
then ( Cl A`)` \/ ( Cl B`)` = [#]X by XBOOLE_1:54;
then ( Cl A`)` \/ (Int B) = [#]X by TOPS_1:def 1;
hence thesis by TOPS_1:def 1;
end;
assume
A4: for A, B being Subset of X st A is closed & B is closed holds A \/
B = the carrier of X implies (Int A) \/ (Int B) = the carrier of X;
now
let A, B be Subset of X;
assume that
A5: A is open and
A6: B is open;
assume A misses B;
then A /\ B = {}X;
then (A /\ B)` = [#]X;
then A` \/ B` = [#]X by XBOOLE_1:54;
then (Int A`) \/ (Int B`) = the carrier of X by A4,A5,A6;
then ((Int A`) \/ (Int B`))` = {}X by XBOOLE_1:37;
then (Int A`)` /\ (Int B`)` = {}X by XBOOLE_1:53;
then (Cl A) /\ (Int B`)` = {}X by Th1;
then (Cl A) misses (Int B`)`;
hence (Cl A) misses (Cl B) by Th1;
end;
hence thesis by Th28;
end;
theorem Th30:
X is extremally_disconnected iff for A being Subset of X st A is
open holds Cl A = Int Cl A
proof
thus X is extremally_disconnected implies for A being Subset of X st A is
open holds Cl A = Int Cl A
proof
assume
A1: X is extremally_disconnected;
let A be Subset of X;
A c= Cl A by PRE_TOPC:18;
then
A2: A misses (Cl A)` by SUBSET_1:24;
assume A is open;
then (Cl A) misses Cl (Cl A)` by A1,A2,Th28;
then Cl A c= (Cl (Cl A)`)` by SUBSET_1:23;
then
A3: Cl A c= Int Cl A by TOPS_1:def 1;
Int Cl A c= Cl A by TOPS_1:16;
hence thesis by A3;
end;
assume
A4: for A being Subset of X st A is open holds Cl A = Int Cl A;
now
let A be Subset of X;
assume A is open;
then Cl A = Int Cl A by A4;
hence Cl A is open;
end;
hence thesis;
end;
theorem
X is extremally_disconnected iff for A being Subset of X st A is
closed holds Int A = Cl Int A
proof
thus X is extremally_disconnected implies for A being Subset of X st A is
closed holds Int A = Cl Int A
proof
assume
A1: X is extremally_disconnected;
let A be Subset of X;
assume A is closed;
then Cl A` = Int Cl A` by A1,Th30;
then Int A = (Int ((Cl A`)``))` by TOPS_1:def 1;
then Int A = Cl ( Cl A`)` by Th1;
hence thesis;
end;
assume
A2: for A being Subset of X st A is closed holds Int A = Cl Int A;
now
let A be Subset of X;
assume A is closed;
then Int A = Cl Int A by A2;
hence Int A is closed;
end;
hence thesis by Th27;
end;
theorem Th32:
X is extremally_disconnected iff for A being Subset of X st A is
condensed holds A is closed & A is open
proof
thus X is extremally_disconnected implies for A being Subset of X st A is
condensed holds A is closed & A is open
proof
assume
A1: X is extremally_disconnected;
let A be Subset of X;
A2: Cl Int A is open by A1;
assume
A3: A is condensed;
then Cl A = Cl Int A by Th9;
then Int Cl A = Cl Int A by A2,TOPS_1:23;
hence thesis by A3,Th8;
end;
assume
A4: for A being Subset of X st A is condensed holds A is closed & A is open;
now
let A be Subset of X;
assume A is open;
then
A5: Int A = A by TOPS_1:23;
Cl Int A is closed_condensed by TDLAT_1:22;
then Cl A is condensed by A5,TOPS_1:66;
hence Cl A is open by A4;
end;
hence thesis;
end;
theorem Th33:
X is extremally_disconnected iff for A being Subset of X st A is
condensed holds A is closed_condensed & A is open_condensed
proof
thus X is extremally_disconnected implies for A being Subset of X st A is
condensed holds A is closed_condensed & A is open_condensed
by Th32,TOPS_1:66,TOPS_1:67;
assume
A1: for A being Subset of X st A is condensed holds A is
closed_condensed & A is open_condensed;
now
let A be Subset of X;
assume
A2: A is condensed;
then
A3: A is open_condensed by A1;
A is closed_condensed by A1,A2;
hence A is closed & A is open by A3,TOPS_1:66,67;
end;
hence thesis by Th32;
end;
theorem Th34:
X is extremally_disconnected iff for A being Subset of X st A is
condensed holds Int Cl A = Cl Int A
proof
thus X is extremally_disconnected implies for A being Subset of X st A is
condensed holds Int Cl A = Cl Int A
proof
assume
A1: X is extremally_disconnected;
let A be Subset of X;
assume A is condensed;
then
A2: Cl A = Cl Int A by Th9;
Cl Int A is open by A1;
hence thesis by A2,TOPS_1:23;
end;
assume
A3: for A being Subset of X st A is condensed holds Int Cl A = Cl Int A;
now
let A be Subset of X;
assume
A4: A is condensed;
then Int Cl A = Cl Int A by A3;
hence A is closed & A is open by A4,Th8;
end;
hence thesis by Th32;
end;
theorem
X is extremally_disconnected iff for A being Subset of X st A is
condensed holds Int A = Cl A
proof
thus X is extremally_disconnected implies for A being Subset of X st A is
condensed holds Int A = Cl A
proof
assume
A1: X is extremally_disconnected;
let A be Subset of X;
assume
A2: A is condensed;
then A is closed by A1,Th32;
then
A3: A = Cl A by PRE_TOPC:22;
A is open by A1,A2,Th32;
hence thesis by A3,TOPS_1:23;
end;
assume
A4: for A being Subset of X st A is condensed holds Int A = Cl A;
now
let A be Subset of X;
assume A is condensed;
then Int A = Cl A by A4;
hence A is closed & A is open by Th5;
end;
hence thesis by Th32;
end;
theorem Th36:
X is extremally_disconnected iff for A being Subset of X holds (
A is open_condensed implies A is closed_condensed) & (A is closed_condensed
implies A is open_condensed)
proof
thus X is extremally_disconnected implies for A being Subset of X holds (A
is open_condensed implies A is closed_condensed) & (A is closed_condensed
implies A is open_condensed)
proof
assume
A1: X is extremally_disconnected;
let A be Subset of X;
thus A is open_condensed implies A is closed_condensed
proof
assume A is open_condensed;
then A is condensed by TOPS_1:67;
hence thesis by A1,Th33;
end;
thus A is closed_condensed implies A is open_condensed
proof
assume A is closed_condensed;
then A is condensed by TOPS_1:66;
hence thesis by A1,Th33;
end;
end;
assume
A2: for A being Subset of X holds (A is open_condensed implies A is
closed_condensed) & (A is closed_condensed implies A is open_condensed);
for A being Subset of X st A is condensed holds Int Cl A = Cl Int A
proof
let A be Subset of X;
assume
A3: A is condensed;
then
A4: A c= Cl Int A by TOPS_1:def 6;
Cl Int A is closed_condensed by TDLAT_1:22;
then Cl Int A is open_condensed by A2;
then Cl Int A = Int Cl Cl Int A by TOPS_1:def 8;
then
A5: Cl Int A c= Int Cl A by TDLAT_2:1;
Int Cl A c= A by A3,TOPS_1:def 6;
then Int Cl A c= Cl Int A by A4;
hence thesis by A5;
end;
hence thesis by Th34;
end;
definition
let IT be non empty TopSpace;
attr IT is hereditarily_extremally_disconnected means
:Def5:
for X0 being non empty SubSpace of IT holds X0 is extremally_disconnected;
end;
registration
cluster hereditarily_extremally_disconnected strict for non empty TopSpace;
existence
proof
take X = the discrete strict non empty TopSpace;
for X0 be non empty SubSpace of X holds X0 is extremally_disconnected
by Th16,PRE_TOPC:22;
hence thesis;
end;
end;
registration
cluster hereditarily_extremally_disconnected -> extremally_disconnected for
non
empty TopSpace;
coherence
proof
let X be non empty TopSpace such that
A1: X is hereditarily_extremally_disconnected;
X is SubSpace of X by TSEP_1:2;
hence thesis by A1;
end;
cluster almost_discrete -> hereditarily_extremally_disconnected for
non empty
TopSpace;
coherence
proof
let X be non empty TopSpace;
assume X is almost_discrete;
then reconsider X as almost_discrete non empty TopSpace;
for X0 be non empty SubSpace of X holds X0 is extremally_disconnected
by Th21,PRE_TOPC:22;
hence thesis;
end;
end;
theorem Th37:
for X being extremally_disconnected non empty TopSpace, X0
being non empty SubSpace of X, A being Subset of X st A = the carrier of X0 & A
is dense holds X0 is extremally_disconnected
proof
let X be extremally_disconnected non empty TopSpace, X0 be non empty
SubSpace of X, A be Subset of X;
assume
A1: A = the carrier of X0;
assume
A2: A is dense;
for D0, B0 being Subset of X0 st D0 is open & B0 is open holds D0 misses
B0 implies (Cl D0) misses (Cl B0)
proof
let D0, B0 be Subset of X0;
assume that
A3: D0 is open and
A4: B0 is open;
consider D being Subset of X such that
A5: D is open and
A6: D /\ [#]X0 = D0 by A3,TOPS_2:24;
consider B being Subset of X such that
A7: B is open and
A8: B /\ [#]X0 = B0 by A4,TOPS_2:24;
assume
A9: D0 /\ B0 = {};
D misses B
proof
assume D /\ B <> {};
then (D /\ B) meets A by A2,A5,A7,TOPS_1:45;
then (D /\ B) /\ A <> {};
then D /\ (B /\ (A /\ A)) <> {} by XBOOLE_1:16;
then D /\ (A /\ (B /\ A)) <> {} by XBOOLE_1:16;
hence contradiction by A1,A6,A8,A9,XBOOLE_1:16;
end;
then (Cl D) misses (Cl B) by A5,A7,Th28;
then (Cl D) /\ (Cl B) = {};
then ((Cl D) /\ (Cl B)) /\ [#]X0 = {};
then (Cl D) /\ ((Cl B) /\ ([#]X0 /\ [#]X0)) = {} by XBOOLE_1:16;
then (Cl D) /\ ([#]X0 /\ ((Cl B) /\ [#]X0)) = {} by XBOOLE_1:16;
then
A10: ((Cl D) /\ [#]X0) /\ ((Cl B) /\ [#]X0) = {} by XBOOLE_1:16;
A11: Cl B0 c= (Cl B) /\ [#]X0
proof
B0 c= B by A8,XBOOLE_1:17;
then reconsider B1 = B0 as Subset of X by XBOOLE_1:1;
Cl B1 c= Cl B by A8,PRE_TOPC:19,XBOOLE_1:17;
then (Cl B1) /\ [#]X0 c= (Cl B) /\ [#]X0 by XBOOLE_1:26;
hence thesis by PRE_TOPC:17;
end;
Cl D0 c= (Cl D) /\ [#]X0
proof
D0 c= D by A6,XBOOLE_1:17;
then reconsider D1 = D0 as Subset of X by XBOOLE_1:1;
Cl D1 c= Cl D by A6,PRE_TOPC:19,XBOOLE_1:17;
then (Cl D1) /\ [#]X0 c= (Cl D) /\ [#]X0 by XBOOLE_1:26;
hence thesis by PRE_TOPC:17;
end;
then (Cl D0) /\ (Cl B0) c= ((Cl D) /\ [#]X0) /\ ((Cl B) /\ [#]X0) by A11,
XBOOLE_1:27;
then (Cl D0) /\ (Cl B0) = {} by A10;
hence thesis;
end;
hence thesis by Th28;
end;
registration
let X be extremally_disconnected non empty TopSpace;
cluster open -> extremally_disconnected for non empty SubSpace of X;
coherence
proof
let X0 be non empty SubSpace of X such that
A1: X0 is open;
reconsider B = the carrier of X0 as Subset of X by TSEP_1:1;
now
let A0 be Subset of X0;
A0 c= B;
then reconsider A = A0 as Subset of X by XBOOLE_1:1;
assume A0 is open;
then A is open by A1,TSEP_1:17;
then
A2: Cl A is open by Def4;
Cl A0 = (Cl A) /\ [#]X0 by PRE_TOPC:17;
hence Cl A0 is open by A2,TOPS_2:24;
end;
hence thesis;
end;
end;
registration
let X be extremally_disconnected non empty TopSpace;
cluster extremally_disconnected strict for non empty SubSpace of X;
existence
proof
set X0 = the strict open non empty SubSpace of X;
take X0;
thus thesis;
end;
end;
registration
let X be hereditarily_extremally_disconnected non empty TopSpace;
cluster -> hereditarily_extremally_disconnected for
non empty SubSpace of X;
coherence
proof
let X0 be non empty SubSpace of X;
for Y being non empty SubSpace of X0 holds Y is extremally_disconnected
proof
let Y be non empty SubSpace of X0;
Y is SubSpace of X by TSEP_1:7;
hence thesis by Def5;
end;
hence thesis;
end;
end;
registration
let X be hereditarily_extremally_disconnected non empty TopSpace;
cluster hereditarily_extremally_disconnected strict for
non empty SubSpace of X;
existence
proof
set X0 = the strict non empty SubSpace of X;
take X0;
thus thesis;
end;
end;
theorem
(for X0 being closed non empty SubSpace of X holds X0 is
extremally_disconnected) implies X is hereditarily_extremally_disconnected
proof
assume
A1: for Y being closed non empty SubSpace of X holds Y is
extremally_disconnected;
for X0 being non empty SubSpace of X holds X0 is extremally_disconnected
proof
let X0 be non empty SubSpace of X;
reconsider A0 = the carrier of X0 as Subset of X by TSEP_1:1;
set A = Cl A0;
A is non empty by PCOMPS_1:2;
then consider Y being strict closed non empty SubSpace of X such that
A2: A = the carrier of Y by TSEP_1:15;
A0 c= A by PRE_TOPC:18;
then reconsider Y0 = X0 as non empty SubSpace of Y by A2,TSEP_1:4;
reconsider B0 = the carrier of Y0 as Subset of Y by TSEP_1:1;
Cl B0 = A /\ [#]Y by PRE_TOPC:17;
then
A3: B0 is dense by A2,TOPS_1:def 3;
Y is extremally_disconnected by A1;
hence thesis by A3,Th37;
end;
hence thesis;
end;
begin
:: 5. The Lattice of Domains of Extremally Disconnected Spaces.
::Properties of the Lattice of Domains of an Extremally Disconnected Space.
reserve Y for extremally_disconnected non empty TopSpace;
theorem Th39:
Domains_of Y = Closed_Domains_of Y
proof
now
let S be object;
assume
A1: S in Domains_of Y;
then reconsider A = S as Subset of Y;
A in {D where D is Subset of Y : D is condensed} by A1;
then ex D being Subset of Y st D = A & D is condensed;
then A is closed_condensed by Th33;
then A in {E where E is Subset of Y : E is closed_condensed};
hence S in Closed_Domains_of Y;
end;
then
A2: Domains_of Y c= Closed_Domains_of Y;
Closed_Domains_of Y c= Domains_of Y by TDLAT_1:31;
hence thesis by A2;
end;
theorem Th40:
D-Union Y = CLD-Union Y & D-Meet Y = CLD-Meet Y
proof
A1: Domains_of Y = Closed_Domains_of Y by Th39;
hence D-Union Y = (D-Union Y)||Closed_Domains_of Y by RELSET_1:19
.= CLD-Union Y by TDLAT_1:39;
thus D-Meet Y = (D-Meet Y)||Closed_Domains_of Y by A1,RELSET_1:19
.= CLD-Meet Y by TDLAT_1:40;
end;
theorem Th41:
Domains_Lattice Y = Closed_Domains_Lattice Y
proof
A1: D-Union Y = CLD-Union Y by Th40;
A2: D-Meet Y = CLD-Meet Y by Th40;
Domains_of Y = Closed_Domains_of Y by Th39;
hence
Domains_Lattice Y = LattStr(#Closed_Domains_of Y,CLD-Union Y,CLD-Meet Y
#) by A1,A2
.= Closed_Domains_Lattice Y;
end;
theorem Th42:
Domains_of Y = Open_Domains_of Y
proof
now
let S be object;
assume
A1: S in Domains_of Y;
then reconsider A = S as Subset of Y;
A in {D where D is Subset of Y : D is condensed} by A1;
then ex D being Subset of Y st D = A & D is condensed;
then A is open_condensed by Th33;
then A in {E where E is Subset of Y : E is open_condensed};
hence S in Open_Domains_of Y;
end;
then
A2: Domains_of Y c= Open_Domains_of Y;
Open_Domains_of Y c= Domains_of Y by TDLAT_1:35;
hence thesis by A2;
end;
theorem Th43:
D-Union Y = OPD-Union Y & D-Meet Y = OPD-Meet Y
proof
A1: Domains_of Y = Open_Domains_of Y by Th42;
hence D-Union Y = (D-Union Y)||Open_Domains_of Y by RELSET_1:19
.= OPD-Union Y by TDLAT_1:42;
thus D-Meet Y = (D-Meet Y)||Open_Domains_of Y by A1,RELSET_1:19
.= OPD-Meet Y by TDLAT_1:43;
end;
theorem Th44:
Domains_Lattice Y = Open_Domains_Lattice Y
proof
A1: D-Union Y = OPD-Union Y by Th43;
A2: D-Meet Y = OPD-Meet Y by Th43;
Domains_of Y = Open_Domains_of Y by Th42;
hence Domains_Lattice Y =LattStr(#Open_Domains_of Y,OPD-Union Y,OPD-Meet Y#)
by A1,A2
.= Open_Domains_Lattice Y;
end;
theorem Th45:
for A, B being Element of Domains_of Y holds (D-Union Y).(A,B) =
A \/ B & (D-Meet Y).(A,B) = A /\ B
proof
let A, B be Element of Domains_of Y;
reconsider A0 = A, B0 = B as Element of Closed_Domains_of Y by Th39;
(D-Union Y).(A,B) = (CLD-Union Y).(A0,B0) by Th40;
hence (D-Union Y).(A,B) = A \/ B by TDLAT_1:def 6;
reconsider A0 = A, B0 = B as Element of Open_Domains_of Y by Th42;
(D-Meet Y).(A,B) = (OPD-Meet Y).(A0,B0) by Th43;
hence thesis by TDLAT_1:def 11;
end;
theorem
for a, b being Element of Domains_Lattice Y for A, B being Element of
Domains_of Y st a = A & b = B holds a "\/" b = A \/ B & a "/\" b = A /\ B
proof
let a, b be Element of Domains_Lattice Y;
let A, B be Element of Domains_of Y;
assume that
A1: a = A and
A2: b = B;
thus a "\/" b = (D-Union Y).(A,B) by A1,A2,LATTICES:def 1
.= A \/ B by Th45;
thus a "/\" b = (D-Meet Y).(A,B) by A1,A2,LATTICES:def 2
.= A /\ B by Th45;
end;
theorem
for F being Subset-Family of Y st F is domains-family for S being
Subset of Domains_Lattice Y st S = F holds "\/"(S,Domains_Lattice Y) = Cl(union
F)
proof
let F be Subset-Family of Y;
assume F is domains-family;
then F c= Domains_of Y by TDLAT_2:65;
then F c= Closed_Domains_of Y by Th39;
then
A1: F is closed-domains-family by TDLAT_2:72;
let S be Subset of Domains_Lattice Y;
reconsider P = S as Subset of Closed_Domains_Lattice Y by Th41;
assume
A2: S = F;
thus "\/"(S,Domains_Lattice Y) = "\/"(P,Closed_Domains_Lattice Y) by Th41
.= Cl(union F) by A1,A2,TDLAT_2:100;
end;
theorem
for F being Subset-Family of Y st F is domains-family for S being
Subset of Domains_Lattice Y st S = F holds (S <> {} implies "/\"(S,
Domains_Lattice Y) = Int(meet F)) & (S = {} implies "/\"(S,Domains_Lattice Y) =
[#]Y)
proof
let F be Subset-Family of Y;
assume
A1: F is domains-family;
then F c= Domains_of Y by TDLAT_2:65;
then F c= Open_Domains_of Y by Th42;
then
A2: F is open-domains-family by TDLAT_2:79;
let S be Subset of Domains_Lattice Y;
assume
A3: S = F;
Domains_Lattice Y = Open_Domains_Lattice Y by Th44;
hence S <> {} implies "/\"(S,Domains_Lattice Y) = Int(meet F) by A2,A3,
TDLAT_2:110;
assume S = {};
hence thesis by A1,A3,TDLAT_2:93;
end;
::Lattice-theoretic Characterizations of Extremally Disconnected Spaces.
reserve X for non empty TopSpace;
theorem Th49:
X is extremally_disconnected iff Domains_Lattice X is M_Lattice
proof
thus X is extremally_disconnected implies Domains_Lattice X is M_Lattice
proof
assume X is extremally_disconnected;
then Domains_Lattice X = Open_Domains_Lattice X by Th44;
hence thesis;
end;
assume
A1: Domains_Lattice X is M_Lattice;
assume not X is extremally_disconnected;
then consider D being Subset of X such that
A2: D is condensed and
A3: Int Cl D <> Cl Int D by Th34;
set A = Int Cl D, C = Cl Int D, B = C`;
A4: D c= C by A2,TOPS_1:def 6;
A c= D by A2,TOPS_1:def 6;
then
A5: A c= C by A4;
A6: A is open_condensed by TDLAT_1:23;
then
A7: A = Int Cl A by TOPS_1:def 8;
B misses C by XBOOLE_1:79;
then
A8: B /\ C = {}X;
A9: C is closed_condensed by TDLAT_1:22;
then
A10: C = Cl Int C by TOPS_1:def 7;
C is condensed by A9,TOPS_1:66;
then
A11: C in {E where E is Subset of X : E is condensed};
reconsider c = C as Element of Domains_Lattice X by A11;
A is condensed by A6,TOPS_1:67;
then
A in {E where E is Subset of X : E is condensed};
then reconsider a = A as Element of Domains_Lattice X;
A15: B = Int (Int D)` by Th3
.= Int Cl D` by Th2;
B` is closed_condensed by TDLAT_1:22;
then B is open_condensed by TOPS_1:61;
then B is condensed by TOPS_1:67;
then B in {E where E is Subset of X : E is condensed};
then reconsider b = B as Element of Domains_Lattice X;
A16: A \/ {}X = A;
Cl(A \/ B) = Cl A \/ Cl B by PRE_TOPC:20
.= Cl Int(Cl D \/ Cl D`) by A15,TDLAT_1:6
.= Cl Int Cl(D \/ D`) by PRE_TOPC:20
.= Cl Int Cl [#]X by PRE_TOPC:2
.= Cl Int [#]X by TOPS_1:2
.= Cl [#]X by TOPS_1:15
.= [#]X by TOPS_1:2;
then a "\/" b = Int([#]X) \/ (A \/ B) by TDLAT_2:87
.= [#]X \/ (A \/ B) by TOPS_1:15
.= [#]X by XBOOLE_1:12;
then
A17: (a "\/" b) "/\" c = Cl(Int([#]X /\ C)) /\ ([#]X /\ C) by TDLAT_2:87
.= Cl(Int C) /\ ([#]X /\ C) by XBOOLE_1:28
.= Cl(Int C) /\ C by XBOOLE_1:28
.= C by A10;
A18: a [= c by A5,TDLAT_2:89;
b "/\" c = Cl(Int(B /\ C)) /\ (B /\ C) by TDLAT_2:87
.= {}X by A8;
then a "\/" (b "/\" c) = Int(Cl A) \/ A by A16,TDLAT_2:87
.= A by A7;
hence contradiction by A1,A3,A18,A17,LATTICES:def 12;
end;
theorem
Domains_Lattice X = Closed_Domains_Lattice X implies
X is extremally_disconnected by Th49;
theorem
Domains_Lattice X = Open_Domains_Lattice X implies
X is extremally_disconnected by Th49;
theorem
Closed_Domains_Lattice X = Open_Domains_Lattice X implies
X is extremally_disconnected
proof
assume Closed_Domains_Lattice X = Open_Domains_Lattice X; then
A1: Closed_Domains_of X = Open_Domains_of X;
for A being Subset of X holds (A is open_condensed implies A is
closed_condensed) & (A is closed_condensed implies A is open_condensed)
proof
let A be Subset of X;
thus A is open_condensed implies A is closed_condensed
proof
assume A is open_condensed;
then A in {E where E is Subset of X : E is open_condensed}; then
A in Closed_Domains_of X by A1;
then A in {E where E is Subset of X : E is closed_condensed};
then ex D being Subset of X st D = A & D is closed_condensed;
hence thesis;
end;
assume A is closed_condensed;
then A in {E where E is Subset of X : E is closed_condensed}; then
A in Open_Domains_of X by A1;
then A in {E where E is Subset of X : E is open_condensed };
then ex D being Subset of X st D = A & D is open_condensed;
hence thesis;
end;
hence thesis by Th36;
end;
theorem
X is extremally_disconnected iff Domains_Lattice X is B_Lattice
proof
thus X is extremally_disconnected implies Domains_Lattice X is B_Lattice
proof
assume X is extremally_disconnected;
then Domains_Lattice X = Open_Domains_Lattice X by Th44;
hence thesis;
end;
assume Domains_Lattice X is B_Lattice;
hence thesis by Th49;
end;