:: On Nowhere and Everywhere Dense Subspaces of Topological Spaces
:: by Zbigniew Karno
::
:: Received November 9, 1993
:: Copyright (c) 1993-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 XBOOLE_0, PRE_TOPC, SUBSET_1, TSEP_2, STRUCT_0, TOPS_3, TOPS_1,
ZFMISC_1, RCOMP_1, TARSKI, SETFAM_1, NATTRA_1, TDLAT_3;
notations TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1,
TSEP_1, TSEP_2, TDLAT_3, TOPS_3, TEX_2;
constructors TOPS_1, BORSUK_1, TSEP_1, TDLAT_3, TOPS_3, TEX_2, TSEP_2;
registrations XBOOLE_0, STRUCT_0, PRE_TOPC, BORSUK_1, TDLAT_3, TEX_1, TEX_2,
TOPS_1;
requirements BOOLE, SUBSET;
definitions TSEP_2;
equalities STRUCT_0;
expansions TSEP_2;
theorems PRE_TOPC, TOPS_1, BORSUK_1, TSEP_1, TMAP_1, TSEP_2, TOPS_3, TEX_1,
TEX_2, XBOOLE_0, XBOOLE_1, SUBSET_1;
begin
:: 1. Some Properties of Subsets of a Topological Space.
reserve X for non empty TopSpace,
A,B for Subset of X;
theorem Th1:
A,B constitute_a_decomposition implies (A is non empty iff B is proper)
proof
assume
A1: A,B constitute_a_decomposition;
then
A2: B = A` by TSEP_2:3;
thus A is non empty implies B is proper
by A2,TOPS_3:1,SUBSET_1:def 6;
assume
A3: B is proper;
A = B` by A1,TSEP_2:3;
hence thesis by A3;
end;
Lm1: A is everywhere_dense & B is everywhere_dense implies A meets B
proof
assume A is everywhere_dense & B is everywhere_dense;
then A /\ B <> {} by TOPS_3:34,44;
hence thesis by XBOOLE_0:def 7;
end;
Lm2: A is everywhere_dense & B is dense or A is dense & B is everywhere_dense
implies A meets B
proof
assume
A is everywhere_dense & B is dense or A is dense & B is everywhere_dense;
then A /\ B <> {} by TOPS_3:17,45;
hence thesis by XBOOLE_0:def 7;
end;
theorem Th2:
A,B constitute_a_decomposition implies (A is dense iff B is boundary)
proof
assume
A1: A,B constitute_a_decomposition;
then B = A` by TSEP_2:3;
hence A is dense implies B is boundary by TOPS_3:18;
assume
A2: B is boundary;
A = B` by A1,TSEP_2:3;
hence thesis by A2,TOPS_1:def 4;
end;
theorem
A,B constitute_a_decomposition implies (A is boundary iff B is dense) by Th2;
theorem Th4:
A,B constitute_a_decomposition implies (A is everywhere_dense iff
B is nowhere_dense)
proof
assume
A1: A,B constitute_a_decomposition;
then B = A` by TSEP_2:3;
hence A is everywhere_dense implies B is nowhere_dense by TOPS_3:39;
assume
A2: B is nowhere_dense;
A = B` by A1,TSEP_2:3;
hence thesis by A2,TOPS_3:40;
end;
theorem
A,B constitute_a_decomposition implies (A is nowhere_dense iff B is
everywhere_dense) by Th4;
reserve Y1,Y2 for non empty SubSpace of X;
theorem Th6:
Y1,Y2 constitute_a_decomposition implies Y1 is proper & Y2 is proper
proof
reconsider A1 = the carrier of Y1, A2 = the carrier of Y2 as Subset of X by
TSEP_1:1;
assume Y1,Y2 constitute_a_decomposition;
then A1,A2 constitute_a_decomposition;
then A1 is proper & A2 is proper by Th1;
hence thesis by TEX_2:8;
end;
theorem
for X being non trivial TopSpace, D being non empty proper
Subset of X ex Y0 being proper strict non empty SubSpace of X st D = the
carrier of Y0
proof
let X be non trivial TopSpace, D be non empty proper Subset of X;
consider Y0 being strict non empty SubSpace of X such that
A1: D = the carrier of Y0 by TSEP_1:10;
reconsider Y0 as proper strict non empty SubSpace of X by A1,TEX_2:8;
take Y0;
thus thesis by A1;
end;
theorem Th8:
for X being non trivial TopSpace, Y1 being proper non
empty SubSpace of X ex Y2 being proper strict non empty SubSpace of X st Y1,Y2
constitute_a_decomposition
proof
let X be non trivial TopSpace, Y1 be proper non empty SubSpace
of X;
reconsider A1 = the carrier of Y1 as Subset of X by TSEP_1:1;
A1 is proper by TEX_2:8;
then consider Y2 being strict non empty SubSpace of X such that
A1: A1` = the carrier of Y2 by TSEP_1:10;
A2: for P, Q be Subset of X st P = the carrier of Y1 & Q = the carrier of Y2
holds P,Q constitute_a_decomposition by A1,TSEP_2:5;
then Y1,Y2 constitute_a_decomposition;
then reconsider Y2 as proper strict non empty SubSpace of X by Th6;
take Y2;
thus thesis by A2;
end;
begin
:: 2. Dense and Everywhere Dense Subspaces.
definition
let X be non empty TopSpace;
let IT be SubSpace of X;
attr IT is dense means
:Def1:
for A being Subset of X st A = the carrier of IT holds A is dense;
end;
theorem Th9:
for X0 being SubSpace of X, A being Subset of X st A = the
carrier of X0 holds X0 is dense iff A is dense;
registration
let X be non empty TopSpace;
cluster dense closed -> non proper for SubSpace of X;
coherence
proof
let X0 be SubSpace of X;
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
assume
A1: X0 is dense closed;
then A is closed by TSEP_1:11;
then
A2: Cl A = A by PRE_TOPC:22;
A is dense by A1;
then Cl A = the carrier of X by TOPS_3:def 2;
then A is non proper by A2,SUBSET_1:def 6;
hence thesis by TEX_2:8;
end;
cluster dense proper -> non closed for SubSpace of X;
coherence;
cluster proper closed -> non dense for SubSpace of X;
coherence;
end;
registration
let X be non empty TopSpace;
cluster dense strict non empty for SubSpace of X;
existence
proof
X is SubSpace of X by TSEP_1:2;
then reconsider A0 = the carrier of X as Subset of X by TSEP_1:1;
consider X0 being strict non empty SubSpace of X such that
A1: A0 = the carrier of X0 by TSEP_1:10;
take X0;
now
let A be Subset of X;
assume A = the carrier of X0;
then A = [#]X by A1;
hence A is dense;
end;
hence thesis;
end;
end;
::Properties of Dense Subspaces.
theorem Th10:
for A0 being non empty Subset of X st A0 is dense ex X0 being
dense strict non empty SubSpace of X st A0 = the carrier of X0
proof
let A0 be non empty Subset of X;
consider X0 being strict non empty SubSpace of X such that
A1: A0 = the carrier of X0 by TSEP_1:10;
assume A0 is dense;
then reconsider Y0 = X0 as dense strict non empty SubSpace of X by A1,Th9;
take Y0;
thus thesis by A1;
end;
theorem
for X0 being dense non empty SubSpace of X, A being Subset of X, B
being Subset of X0 st A = B holds B is dense iff A is dense
proof
let X0 be dense non empty SubSpace of X, A be Subset of X, B be Subset of X0;
assume
A1: A = B;
reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
C is dense by Th9;
hence thesis by A1,TOPS_3:60;
end;
theorem
for X1 being dense SubSpace of X, X2 being SubSpace of X holds X1 is
SubSpace of X2 implies X2 is dense
proof
let X1 be dense SubSpace of X, X2 be SubSpace of X;
reconsider C = the carrier of X1 as Subset of X by BORSUK_1:1;
assume X1 is SubSpace of X2;
then
A1: the carrier of X1 c= the carrier of X2 by TSEP_1:4;
C is dense by Def1;
then for A be Subset of X st A = the carrier of X2 holds A is dense by A1,
TOPS_1:44;
hence thesis;
end;
theorem
for X1 being dense non empty SubSpace of X, X2 being non empty
SubSpace of X holds X1 is SubSpace of X2 implies X1 is dense SubSpace of X2
proof
let X1 be dense non empty SubSpace of X, X2 be non empty SubSpace of X;
reconsider C = the carrier of X1 as Subset of X by BORSUK_1:1;
C is dense by Def1;
then
A1: for A be Subset of X2 st A = the carrier of X1 holds A is dense by
TOPS_3:59;
assume X1 is SubSpace of X2;
hence thesis by A1,Def1;
end;
theorem
for X1 being dense non empty SubSpace of X, X2 being dense non empty
SubSpace of X1 holds X2 is dense non empty SubSpace of X
proof
let X1 be dense non empty SubSpace of X, X2 be dense non empty SubSpace of
X1;
reconsider C = the carrier of X1 as Subset of X by BORSUK_1:1;
now
let A be Subset of X;
assume
A1: A = the carrier of X2;
then reconsider B = A as Subset of X1 by BORSUK_1:1;
A2: C is dense by Def1;
B is dense by A1,Def1;
hence A is dense by A2,TOPS_3:60;
end;
hence thesis by Def1,TSEP_1:7;
end;
theorem
for Y1, Y2 being non empty TopSpace st Y2 = the TopStruct of Y1 holds
Y1 is dense SubSpace of X iff Y2 is dense SubSpace of X
proof
let X1,X2 be non empty TopSpace;
assume
A1: X2 = the TopStruct of X1;
thus X1 is dense SubSpace of X implies X2 is dense SubSpace of X
proof
assume
A2: X1 is dense SubSpace of X;
then reconsider Y2 = X2 as SubSpace of X by A1,TMAP_1:7;
for A2 be Subset of X st A2 = the carrier of Y2 holds A2 is dense by A1,A2
,Def1;
hence thesis by Def1;
end;
assume
A3: X2 is dense SubSpace of X;
then reconsider Y1 = X1 as SubSpace of X by A1,TMAP_1:7;
for A1 be Subset of X st A1 = the carrier of Y1 holds A1 is dense by A1,A3
,Def1;
hence thesis by Def1;
end;
definition
let X be non empty TopSpace;
let IT be SubSpace of X;
attr IT is everywhere_dense means
:Def2:
for A being Subset of X st A = the carrier of IT holds A is everywhere_dense;
end;
theorem Th16:
for X0 being SubSpace of X, A being Subset of X st A = the
carrier of X0 holds X0 is everywhere_dense iff A is everywhere_dense;
registration
let X be non empty TopSpace;
cluster everywhere_dense -> dense for SubSpace of X;
coherence
by TOPS_3:33;
cluster non dense -> non everywhere_dense for SubSpace of X;
coherence;
cluster non proper -> everywhere_dense for SubSpace of X;
coherence
proof
let X0 be SubSpace of X;
assume
A1: X0 is non proper;
now
let A be Subset of X;
assume A = the carrier of X0;
then A is non proper by A1,TEX_2:8;
then A = [#]X by SUBSET_1:def 6;
hence A is everywhere_dense by TOPS_3:31;
end;
hence thesis;
end;
cluster non everywhere_dense -> proper for SubSpace of X;
coherence;
end;
registration
let X be non empty TopSpace;
cluster everywhere_dense strict non empty for SubSpace of X;
existence
proof
X is SubSpace of X by TSEP_1:2;
then reconsider A0 = the carrier of X as Subset of X by TSEP_1:1;
consider X0 being strict non empty SubSpace of X such that
A1: A0 = the carrier of X0 by TSEP_1:10;
take X0;
now
let A be Subset of X;
assume A = the carrier of X0;
then A = [#]X by A1;
hence A is everywhere_dense by TOPS_3:31;
end;
hence thesis;
end;
end;
::Properties of Everywhere Dense Subspaces.
theorem Th17:
for A0 being non empty Subset of X st A0 is everywhere_dense ex
X0 being everywhere_dense strict non empty SubSpace of X st A0 = the carrier of
X0
proof
let A0 be non empty Subset of X;
consider X0 being strict non empty SubSpace of X such that
A1: A0 = the carrier of X0 by TSEP_1:10;
assume A0 is everywhere_dense;
then reconsider
Y0 = X0 as everywhere_dense strict non empty SubSpace of X by A1,Th16;
take Y0;
thus thesis by A1;
end;
theorem
for X0 being everywhere_dense non empty SubSpace of X, A being Subset
of X, B being Subset of X0 st A = B holds B is everywhere_dense iff A is
everywhere_dense
proof
let X0 be everywhere_dense non empty SubSpace of X, A be Subset of X, B be
Subset of X0;
assume
A1: A = B;
reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
C is everywhere_dense by Th16;
hence thesis by A1,TOPS_3:64;
end;
theorem
for X1 being everywhere_dense SubSpace of X, X2 being SubSpace of X
holds X1 is SubSpace of X2 implies X2 is everywhere_dense
proof
let X1 be everywhere_dense SubSpace of X, X2 be SubSpace of X;
reconsider C = the carrier of X1 as Subset of X by BORSUK_1:1;
assume X1 is SubSpace of X2;
then
A1: the carrier of X1 c= the carrier of X2 by TSEP_1:4;
C is everywhere_dense by Def2;
then for A be Subset of X st A = the carrier of X2 holds A is
everywhere_dense by A1,TOPS_3:38;
hence thesis;
end;
theorem
for X1 being everywhere_dense non empty SubSpace of X, X2 being non
empty SubSpace of X holds X1 is SubSpace of X2 implies X1 is everywhere_dense
SubSpace of X2
proof
let X1 be everywhere_dense non empty SubSpace of X, X2 be non empty SubSpace
of X;
reconsider C = the carrier of X1 as Subset of X by BORSUK_1:1;
C is everywhere_dense by Def2;
then
A1: for A be Subset of X2 st A = the carrier of X1 holds A is
everywhere_dense by TOPS_3:61;
assume X1 is SubSpace of X2;
hence thesis by A1,Def2;
end;
theorem
for X1 being everywhere_dense non empty SubSpace of X, X2 being
everywhere_dense non empty SubSpace of X1 holds X2 is everywhere_dense SubSpace
of X
proof
let X1 be everywhere_dense non empty SubSpace of X, X2 be everywhere_dense
non empty SubSpace of X1;
reconsider C = the carrier of X1 as Subset of X by BORSUK_1:1;
now
let A be Subset of X;
assume
A1: A = the carrier of X2;
then reconsider B = A as Subset of X1 by BORSUK_1:1;
A2: C is everywhere_dense by Def2;
B is everywhere_dense by A1,Def2;
hence A is everywhere_dense by A2,TOPS_3:64;
end;
hence thesis by Def2,TSEP_1:7;
end;
theorem
for Y1, Y2 being non empty TopSpace st Y2 = the TopStruct of Y1 holds
Y1 is everywhere_dense SubSpace of X iff Y2 is everywhere_dense SubSpace of X
proof
let X1,X2 be non empty TopSpace;
assume
A1: X2 = the TopStruct of X1;
thus X1 is everywhere_dense SubSpace of X implies X2 is everywhere_dense
SubSpace of X
proof
assume
A2: X1 is everywhere_dense SubSpace of X;
then reconsider Y2 = X2 as SubSpace of X by A1,TMAP_1:7;
for A2 be Subset of X st A2 = the carrier of Y2 holds A2 is
everywhere_dense by A1,A2,Def2;
hence thesis by Def2;
end;
assume
A3: X2 is everywhere_dense SubSpace of X;
then reconsider Y1 = X1 as SubSpace of X by A1,TMAP_1:7;
for A1 be Subset of X st A1 = the carrier of Y1 holds A1 is
everywhere_dense by A1,A3,Def2;
hence thesis by Def2;
end;
registration
let X be non empty TopSpace;
cluster dense open -> everywhere_dense for SubSpace of X;
coherence
proof
let X0 be SubSpace of X;
assume
A1: X0 is dense open;
now
let A be Subset of X;
assume A = the carrier of X0;
then A is dense & A is open by A1,TSEP_1:16;
hence A is everywhere_dense by TOPS_3:36;
end;
hence thesis;
end;
cluster dense non everywhere_dense -> non open for SubSpace of X;
coherence;
cluster open non everywhere_dense -> non dense for SubSpace of X;
coherence;
end;
registration
let X be non empty TopSpace;
cluster dense open strict non empty for SubSpace of X;
existence
proof
X is SubSpace of X by TSEP_1:2;
then reconsider A0 = the carrier of X as Subset of X by TSEP_1:1;
A0 = [#]X;
then A0 is dense;
then consider X0 being dense strict non empty SubSpace of X such that
A1: A0 = the carrier of X0 by Th10;
take X0;
now
let A be Subset of X;
assume A = the carrier of X0;
then A = [#]X by A1;
hence A is open;
end;
hence thesis by TSEP_1:def 1;
end;
end;
::Properties of Dense Open Subspaces.
theorem Th23:
for A0 being non empty Subset of X st A0 is dense open ex X0
being dense open strict non empty SubSpace of X st A0 = the carrier of X0
proof
let A0 be non empty Subset of X;
consider X0 being strict non empty SubSpace of X such that
A1: A0 = the carrier of X0 by TSEP_1:10;
assume A0 is dense open;
then reconsider Y0 = X0 as dense open strict non empty SubSpace of X by A1
,Th9,TSEP_1:16;
take Y0;
thus thesis by A1;
end;
theorem
for X0 being SubSpace of X holds X0 is everywhere_dense iff ex X1
being dense open strict SubSpace of X st X1 is SubSpace of X0
proof
let X0 be SubSpace of X;
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
thus X0 is everywhere_dense implies ex X1 being dense open strict SubSpace
of X st X1 is SubSpace of X0
proof
assume X0 is everywhere_dense;
then A is everywhere_dense;
then consider C being Subset of X such that
A1: C c= A and
A2: C is open and
A3: C is dense by TOPS_3:41;
C is non empty by A3,TOPS_3:17;
then consider X1 being dense open strict non empty SubSpace of X such that
A4: C = the carrier of X1 by A2,A3,Th23;
take X1;
thus thesis by A1,A4,TSEP_1:4;
end;
given X1 being dense open strict SubSpace of X such that
A5: X1 is SubSpace of X0;
reconsider C = the carrier of X1 as Subset of X by TSEP_1:1;
now
take C;
thus C c= A & C is open & C is dense by A5,Def1,TSEP_1:4,16;
end;
then for A be Subset of X st A = the carrier of X0 holds A is
everywhere_dense by TOPS_3:41;
hence thesis;
end;
reserve X1, X2 for non empty SubSpace of X;
theorem
X1 is dense or X2 is dense implies X1 union X2 is dense SubSpace of X
proof
reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
reconsider A = the carrier of X1 union X2 as Subset of X by TSEP_1:1;
assume X1 is dense or X2 is dense;
then A1 is dense or A2 is dense;
then A1 \/ A2 is dense by TOPS_3:21;
then A is dense by TSEP_1:def 2;
hence thesis by Th9;
end;
theorem
X1 is everywhere_dense or X2 is everywhere_dense implies X1 union X2
is everywhere_dense SubSpace of X
proof
reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
reconsider A = the carrier of X1 union X2 as Subset of X by TSEP_1:1;
assume X1 is everywhere_dense or X2 is everywhere_dense;
then A1 is everywhere_dense or A2 is everywhere_dense;
then A1 \/ A2 is everywhere_dense by TOPS_3:43;
then A is everywhere_dense by TSEP_1:def 2;
hence thesis by Th16;
end;
theorem
X1 is everywhere_dense & X2 is everywhere_dense implies X1 meet X2 is
everywhere_dense SubSpace of X
proof
reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
reconsider A = the carrier of X1 meet X2 as Subset of X by TSEP_1:1;
assume X1 is everywhere_dense & X2 is everywhere_dense;
then
A1: A1 is everywhere_dense & A2 is everywhere_dense;
then A1 meets A2 by Lm1;
then
A2: X1 meets X2 by TSEP_1:def 3;
A1 /\ A2 is everywhere_dense by A1,TOPS_3:44;
then A is everywhere_dense by A2,TSEP_1:def 4;
hence thesis by Th16;
end;
theorem
X1 is everywhere_dense & X2 is dense or X1 is dense & X2 is
everywhere_dense implies X1 meet X2 is dense SubSpace of X
proof
reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
reconsider A = the carrier of X1 meet X2 as Subset of X by TSEP_1:1;
assume
X1 is everywhere_dense & X2 is dense or X1 is dense & X2 is everywhere_dense;
then
A1: A1 is everywhere_dense & A2 is dense or A1 is dense & A2 is
everywhere_dense;
then A1 meets A2 by Lm2;
then
A2: X1 meets X2 by TSEP_1:def 3;
A1 /\ A2 is dense by A1,TOPS_3:45;
then A is dense by A2,TSEP_1:def 4;
hence thesis by Th9;
end;
begin
:: 3. Boundary and Nowhere Dense Subspaces.
definition
let X be non empty TopSpace;
let IT be SubSpace of X;
attr IT is boundary means
:Def3:
for A being Subset of X st A = the carrier of IT holds A is boundary;
end;
theorem Th29:
for X0 being SubSpace of X, A being Subset of X st A = the
carrier of X0 holds X0 is boundary iff A is boundary;
registration
let X be non empty TopSpace;
cluster open -> non boundary for non empty SubSpace of X;
coherence
proof
let X0 be non empty SubSpace of X;
assume
A1: X0 is open;
now
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
assume X0 is boundary;
then A is boundary;
then
A2: Int A = {};
A is open by A1,TSEP_1:16;
hence contradiction by A2,TOPS_1:23;
end;
hence thesis;
end;
cluster boundary -> non open for non empty SubSpace of X;
coherence;
cluster everywhere_dense -> non boundary for SubSpace of X;
coherence
proof
let X0 be SubSpace of X;
assume
A3: X0 is everywhere_dense;
now
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
A is everywhere_dense by A3;
then
A4: A is not boundary by TOPS_3:37;
assume X0 is boundary;
hence contradiction by A4;
end;
hence thesis;
end;
cluster boundary -> non everywhere_dense for SubSpace of X;
coherence;
end;
::Properties of Boundary Subspaces.
theorem Th30:
for A0 being non empty Subset of X st A0 is boundary ex X0 being
strict SubSpace of X st X0 is boundary & A0 = the carrier of X0
proof
let A0 be non empty Subset of X;
assume
A1: A0 is boundary;
consider X0 being strict non empty SubSpace of X such that
A2: A0 = the carrier of X0 by TSEP_1:10;
take X0;
thus thesis by A1,A2;
end;
theorem Th31:
for X1,X2 being SubSpace of X st X1,X2
constitute_a_decomposition holds X1 is dense iff X2 is boundary
proof
let X1,X2 be SubSpace of X;
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by
TSEP_1:1;
assume
A1: for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the
carrier of X2 holds A1,A2 constitute_a_decomposition;
thus X1 is dense implies X2 is boundary
proof
assume
A2: for A1 being Subset of X st A1 = the carrier of X1 holds A1 is dense;
now
let A2 be Subset of X;
assume A2 = the carrier of X2;
then
A3: A1,A2 constitute_a_decomposition by A1;
A1 is dense by A2;
hence A2 is boundary by A3,Th2;
end;
hence thesis;
end;
assume
A4: for A2 being Subset of X st A2 = the carrier of X2 holds A2 is boundary;
now
let A1 be Subset of X;
assume A1 = the carrier of X1;
then
A5: A1,A2 constitute_a_decomposition by A1;
A2 is boundary by A4;
hence A1 is dense by A5,Th2;
end;
hence thesis;
end;
theorem
for X1,X2 being non empty SubSpace of X st X1,X2
constitute_a_decomposition holds X1 is boundary iff X2 is dense by Th31;
theorem Th33:
for X0 being SubSpace of X st X0 is boundary for A being Subset
of X st A c= the carrier of X0 holds A is boundary
proof
let X0 be SubSpace of X;
reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
assume X0 is boundary;
then
A1: C is boundary;
let A be Subset of X;
assume A c= the carrier of X0;
hence thesis by A1,TOPS_3:11;
end;
theorem Th34:
for X1,X2 being SubSpace of X st X1 is boundary holds X2 is
SubSpace of X1 implies X2 is boundary
by TSEP_1:4,Th33;
definition
let X be non empty TopSpace;
let IT be SubSpace of X;
attr IT is nowhere_dense means
:Def4:
for A being Subset of X st A = the carrier of IT holds A is nowhere_dense;
end;
theorem Th35:
for X0 being SubSpace of X, A being Subset of X st A = the
carrier of X0 holds X0 is nowhere_dense iff A is nowhere_dense;
registration
let X be non empty TopSpace;
cluster nowhere_dense -> boundary for SubSpace of X;
coherence
proof
let X0 be SubSpace of X;
assume
A1: X0 is nowhere_dense;
now
let A be Subset of X;
assume A = the carrier of X0;
then A is nowhere_dense by A1;
hence A is boundary;
end;
hence thesis;
end;
cluster non boundary -> non nowhere_dense for SubSpace of X;
coherence;
cluster nowhere_dense -> non dense for SubSpace of X;
coherence
proof
let X0 be SubSpace of X;
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
assume X0 is nowhere_dense;
then A is nowhere_dense;
then
A2: A is not dense by TOPS_3:25;
assume X0 is dense;
hence contradiction by A2;
end;
cluster dense -> non nowhere_dense for SubSpace of X;
coherence;
end;
reserve X for non empty TopSpace;
::Properties of Nowhere Dense Subspaces.
theorem
for A0 being non empty Subset of X st A0 is nowhere_dense ex X0 being
strict SubSpace of X st X0 is nowhere_dense & A0 = the carrier of X0
proof
let A0 be non empty Subset of X;
assume
A1: A0 is nowhere_dense;
consider X0 being strict non empty SubSpace of X such that
A2: A0 = the carrier of X0 by TSEP_1:10;
take X0;
thus thesis by A1,A2;
end;
theorem Th37:
for X1,X2 being SubSpace of X st X1,X2
constitute_a_decomposition holds X1 is everywhere_dense iff X2 is nowhere_dense
proof
let X1,X2 be SubSpace of X;
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by
TSEP_1:1;
assume
A1: for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the
carrier of X2 holds A1,A2 constitute_a_decomposition;
thus X1 is everywhere_dense implies X2 is nowhere_dense
proof
assume
A2: for A1 being Subset of X st A1 = the carrier of X1 holds A1 is
everywhere_dense;
now
let A2 be Subset of X;
assume A2 = the carrier of X2;
then
A3: A1,A2 constitute_a_decomposition by A1;
A1 is everywhere_dense by A2;
hence A2 is nowhere_dense by A3,Th4;
end;
hence thesis;
end;
assume
A4: for A2 being Subset of X st A2 = the carrier of X2 holds A2 is
nowhere_dense;
now
let A1 be Subset of X;
assume A1 = the carrier of X1;
then
A5: A1,A2 constitute_a_decomposition by A1;
A2 is nowhere_dense by A4;
hence A1 is everywhere_dense by A5,Th4;
end;
hence thesis;
end;
theorem
for X1,X2 being non empty SubSpace of X st X1,X2
constitute_a_decomposition holds X1 is nowhere_dense iff X2 is everywhere_dense
by Th37;
theorem Th39:
for X0 being SubSpace of X st X0 is nowhere_dense for A being
Subset of X st A c= the carrier of X0 holds A is nowhere_dense
proof
let X0 be SubSpace of X;
reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
assume X0 is nowhere_dense;
then
A1: C is nowhere_dense;
let A be Subset of X;
assume A c= the carrier of X0;
hence thesis by A1,TOPS_3:26;
end;
theorem Th40:
for X1,X2 being SubSpace of X st X1 is nowhere_dense holds X2 is
SubSpace of X1 implies X2 is nowhere_dense
by TSEP_1:4,Th39;
registration
let X be non empty TopSpace;
cluster boundary closed -> nowhere_dense for SubSpace of X;
coherence
proof
let X0 be SubSpace of X;
assume
A1: X0 is boundary closed;
now
let A be Subset of X;
assume A = the carrier of X0;
then A is boundary & A is closed by A1,TSEP_1:11;
hence A is nowhere_dense;
end;
hence thesis;
end;
cluster boundary non nowhere_dense -> non closed for SubSpace of X;
coherence;
cluster closed non nowhere_dense -> non boundary for SubSpace of X;
coherence;
end;
::Properties of Boundary Closed Subspaces.
theorem Th41:
for A0 being non empty Subset of X st A0 is boundary closed ex
X0 being closed strict non empty SubSpace of X st X0 is boundary & A0 = the
carrier of X0
proof
let A0 be non empty Subset of X;
consider X0 being strict non empty SubSpace of X such that
A1: A0 = the carrier of X0 by TSEP_1:10;
assume
A2: A0 is boundary closed;
then reconsider Y0 = X0 as closed strict non empty SubSpace of X by A1,
TSEP_1:11;
take Y0;
thus thesis by A2,A1;
end;
theorem
for X0 being non empty SubSpace of X holds X0 is nowhere_dense iff ex
X1 being closed strict non empty SubSpace of X st X1 is boundary & X0 is
SubSpace of X1
proof
let X0 be non empty SubSpace of X;
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
thus X0 is nowhere_dense implies ex X1 being closed strict non empty
SubSpace of X st X1 is boundary & X0 is SubSpace of X1
proof
assume X0 is nowhere_dense;
then A is nowhere_dense;
then consider C being Subset of X such that
A1: A c= C and
A2: C is closed & C is boundary by TOPS_3:27;
C is non empty by A1,XBOOLE_1:3;
then consider X1 being closed strict non empty SubSpace of X such that
A3: X1 is boundary & C = the carrier of X1 by A2,Th41;
take X1;
thus thesis by A1,A3,TSEP_1:4;
end;
given X1 being closed strict non empty SubSpace of X such that
A4: X1 is boundary & X0 is SubSpace of X1;
reconsider C = the carrier of X1 as Subset of X by TSEP_1:1;
now
take C;
thus A c= C & C is boundary & C is closed by A4,TSEP_1:4,11;
end;
then for A be Subset of X st A = the carrier of X0 holds A is nowhere_dense
by TOPS_3:27;
hence thesis;
end;
reserve X1, X2 for non empty SubSpace of X;
theorem
(X1 is boundary or X2 is boundary) & X1 meets X2 implies X1 meet X2 is
boundary
proof
assume
A1: X1 is boundary or X2 is boundary;
assume
A2: X1 meets X2;
hereby
per cases by A1;
suppose
A3: X1 is boundary;
X1 meet X2 is SubSpace of X1 by A2,TSEP_1:27;
hence thesis by A3,Th34;
end;
suppose
A4: X2 is boundary;
X1 meet X2 is SubSpace of X2 by A2,TSEP_1:27;
hence thesis by A4,Th34;
end;
end;
end;
theorem
X1 is nowhere_dense & X2 is nowhere_dense implies X1 union X2 is
nowhere_dense
proof
reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
assume X1 is nowhere_dense & X2 is nowhere_dense;
then A1 is nowhere_dense & A2 is nowhere_dense;
then A1 \/ A2 is nowhere_dense by TOPS_1:53;
then for A be Subset of X st A = the carrier of X1 union X2 holds A is
nowhere_dense by TSEP_1:def 2;
hence thesis;
end;
theorem
X1 is nowhere_dense & X2 is boundary or X1 is boundary & X2 is
nowhere_dense implies X1 union X2 is boundary
proof
reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
assume
X1 is nowhere_dense & X2 is boundary or X1 is boundary & X2 is nowhere_dense;
then A1 is nowhere_dense & A2 is boundary or A1 is boundary & A2 is
nowhere_dense;
then A1 \/ A2 is boundary by TOPS_3:30;
then for A be Subset of X st A = the carrier of X1 union X2 holds A is
boundary by TSEP_1:def 2;
hence thesis;
end;
theorem
(X1 is nowhere_dense or X2 is nowhere_dense) & X1 meets X2 implies X1
meet X2 is nowhere_dense
proof
assume
A1: X1 is nowhere_dense or X2 is nowhere_dense;
assume
A2: X1 meets X2;
hereby
per cases by A1;
suppose
A3: X1 is nowhere_dense;
X1 meet X2 is SubSpace of X1 by A2,TSEP_1:27;
hence thesis by A3,Th40;
end;
suppose
A4: X2 is nowhere_dense;
X1 meet X2 is SubSpace of X2 by A2,TSEP_1:27;
hence thesis by A4,Th40;
end;
end;
end;
begin
:: 4. Dense and Boundary Subspaces of non Discrete Spaces.
theorem
for X being non empty TopSpace holds (for X0 being SubSpace of X holds
X0 is non boundary) implies X is discrete
proof
let X be non empty TopSpace;
assume
A1: for X0 being SubSpace of X holds X0 is non boundary;
now
let A be non empty Subset of X;
consider X0 being strict non empty SubSpace of X such that
A2: A = the carrier of X0 by TSEP_1:10;
X0 is non boundary by A1;
hence A is not boundary by A2;
end;
hence thesis by TEX_1:def 5;
end;
theorem
for X being non trivial TopSpace holds (for X0 being
proper SubSpace of X holds X0 is non dense) implies X is discrete
proof
let X be non trivial TopSpace;
assume
A1: for X0 being proper SubSpace of X holds X0 is non dense;
now
let A be Subset of X;
assume
A2: A <> the carrier of X;
now
per cases;
suppose
A is empty;
hence A is not dense by TOPS_3:17;
end;
suppose
A is non empty;
then consider X0 being strict non empty SubSpace of X such that
A3: A = the carrier of X0 by TSEP_1:10;
A is proper by A2,SUBSET_1:def 6;
then reconsider X0 as proper strict SubSpace of X by A3,TEX_2:8;
X0 is non dense by A1;
hence A is not dense by A3;
end;
end;
hence A is not dense;
end;
hence thesis by TEX_1:31;
end;
registration
let X be discrete non empty TopSpace;
cluster -> non boundary for non empty SubSpace of X;
coherence;
cluster proper -> non dense for SubSpace of X;
coherence;
cluster dense -> non proper for SubSpace of X;
coherence;
end;
registration
let X be discrete non empty TopSpace;
cluster non boundary strict non empty for SubSpace of X;
existence
proof
set X0 = the strict non empty SubSpace of X;
take X0;
thus thesis;
end;
end;
registration
let X be discrete non trivial TopSpace;
cluster non dense strict for SubSpace of X;
existence
proof
set X0 = the proper strict SubSpace of X;
take X0;
thus thesis;
end;
end;
theorem
for X being non empty TopSpace holds (ex X0 being non empty SubSpace
of X st X0 is boundary) implies X is non discrete;
theorem
for X being non empty TopSpace holds (ex X0 being non empty SubSpace
of X st X0 is dense proper) implies X is non discrete;
registration
let X be non discrete non empty TopSpace;
cluster boundary strict non empty for SubSpace of X;
existence
proof
consider A0 being non empty Subset of X such that
A1: A0 is boundary by TEX_1:def 5;
consider X0 being strict non empty SubSpace of X such that
A2: A0 = the carrier of X0 by TSEP_1:10;
take X0;
for A be Subset of X st A = the carrier of X0 holds A is boundary by A1,A2;
hence thesis;
end;
cluster dense proper strict non empty for SubSpace of X;
existence
proof
consider A0 being Subset of X such that
A3: A0 <> the carrier of X and
A4: A0 is dense by TEX_1:31;
A0 is non empty by A4,TOPS_3:17;
then consider X0 being dense strict non empty SubSpace of X such that
A5: A0 = the carrier of X0 by A4,Th10;
take X0;
A0 is proper by A3,SUBSET_1:def 6;
hence thesis by A5,TEX_2:8;
end;
end;
reserve X for non discrete non empty TopSpace;
theorem
for A0 being non empty Subset of X st A0 is boundary ex X0 being
boundary strict SubSpace of X st A0 = the carrier of X0
proof
let A0 be non empty Subset of X;
assume A0 is boundary;
then
ex X0 being strict SubSpace of X st X0 is boundary & A0 = the carrier of
X0 by Th30;
hence thesis;
end;
theorem
for A0 being non empty proper Subset of X st A0 is dense ex X0 being
dense proper strict SubSpace of X st A0 = the carrier of X0
proof
let A0 be non empty proper Subset of X;
consider X0 being strict non empty SubSpace of X such that
A1: A0 = the carrier of X0 by TSEP_1:10;
assume A0 is dense;
then reconsider X0 as dense proper strict SubSpace of X by A1,Th9,TEX_2:8;
take X0;
thus thesis by A1;
end;
theorem
for X1 being boundary non empty SubSpace of X ex X2 being dense proper
strict non empty SubSpace of X st X1,X2 constitute_a_decomposition
proof
let X1 be boundary non empty SubSpace of X;
consider X2 being proper strict non empty SubSpace of X such that
A1: X1,X2 constitute_a_decomposition by Th8;
reconsider X2 as dense proper strict non empty SubSpace of X by A1,Th31;
take X2;
thus thesis by A1;
end;
theorem
for X1 being dense proper non empty SubSpace of X ex X2 being boundary
strict non empty SubSpace of X st X1,X2 constitute_a_decomposition
proof
let X1 be dense proper non empty SubSpace of X;
consider X2 being proper strict non empty SubSpace of X such that
A1: X1,X2 constitute_a_decomposition by Th8;
reconsider X2 as boundary strict non empty SubSpace of X by A1,Th31;
take X2;
thus thesis by A1;
end;
theorem
for Y1, Y2 being non empty TopSpace st Y2 = the TopStruct of Y1 holds
Y1 is boundary SubSpace of X iff Y2 is boundary SubSpace of X
proof
let X1,X2 be non empty TopSpace;
assume
A1: X2 = the TopStruct of X1;
thus X1 is boundary SubSpace of X implies X2 is boundary SubSpace of X
proof
assume
A2: X1 is boundary SubSpace of X;
then reconsider Y2 = X2 as SubSpace of X by A1,TMAP_1:7;
for A2 be Subset of X st A2 = the carrier of Y2 holds A2 is boundary
by A1,A2,Def3;
hence thesis by Def3;
end;
assume
A3: X2 is boundary SubSpace of X;
then reconsider Y1 = X1 as SubSpace of X by A1,TMAP_1:7;
for A1 be Subset of X st A1 = the carrier of Y1 holds A1 is boundary by A1,A3
,Def3;
hence thesis by Def3;
end;
begin
:: 5. Everywhere and Nowhere Dense Subspaces of non Almost Discrete Spaces.
theorem
for X being non empty TopSpace holds (for X0 being SubSpace of X holds
X0 is non nowhere_dense) implies X is almost_discrete
proof
let X be non empty TopSpace;
assume
A1: for X0 being SubSpace of X holds X0 is non nowhere_dense;
now
let A be non empty Subset of X;
consider X0 being strict non empty SubSpace of X such that
A2: A = the carrier of X0 by TSEP_1:10;
X0 is non nowhere_dense by A1;
hence A is not nowhere_dense by A2;
end;
hence thesis by TEX_1:def 6;
end;
theorem
for X being non trivial TopSpace holds (for X0 being
proper SubSpace of X holds X0 is non everywhere_dense) implies X is
almost_discrete
proof
let X be non trivial TopSpace;
assume
A1: for X0 being proper SubSpace of X holds X0 is non everywhere_dense;
now
let A be Subset of X;
assume
A2: A <> the carrier of X;
now
per cases;
suppose
A is empty;
hence A is not everywhere_dense by TOPS_3:34;
end;
suppose
A is non empty;
then consider X0 being strict non empty SubSpace of X such that
A3: A = the carrier of X0 by TSEP_1:10;
A is proper by A2,SUBSET_1:def 6;
then reconsider X0 as proper strict SubSpace of X by A3,TEX_2:8;
X0 is non everywhere_dense by A1;
hence A is not everywhere_dense by A3;
end;
end;
hence A is not everywhere_dense;
end;
hence thesis by TEX_1:32;
end;
registration
let X be almost_discrete non empty TopSpace;
cluster -> non nowhere_dense for non empty SubSpace of X;
coherence
proof
let X0 be non empty SubSpace of X;
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
A is not nowhere_dense by TEX_1:def 6;
hence thesis;
end;
cluster proper -> non everywhere_dense for SubSpace of X;
coherence
proof
let X0 be SubSpace of X;
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
assume X0 is proper;
then A is proper by TEX_2:8;
then A <> the carrier of X by SUBSET_1:def 6;
then A is not everywhere_dense by TEX_1:32;
hence thesis;
end;
cluster everywhere_dense -> non proper for SubSpace of X;
coherence;
cluster boundary -> non closed for non empty SubSpace of X;
coherence;
cluster closed -> non boundary for non empty SubSpace of X;
coherence;
cluster dense proper -> non open for SubSpace of X;
coherence;
cluster dense open -> non proper for SubSpace of X;
coherence;
cluster open proper -> non dense for SubSpace of X;
coherence;
end;
registration
let X be almost_discrete non empty TopSpace;
cluster non nowhere_dense strict non empty for SubSpace of X;
existence
proof
set X0 = the strict non empty SubSpace of X;
take X0;
thus thesis;
end;
end;
registration
let X be almost_discrete non trivial TopSpace;
cluster non everywhere_dense strict for SubSpace of X;
existence
proof
set X0 = the proper strict SubSpace of X;
take X0;
thus thesis;
end;
end;
theorem
for X being non empty TopSpace holds (ex X0 being non empty SubSpace
of X st X0 is nowhere_dense) implies X is non almost_discrete;
theorem
for X being non empty TopSpace holds (ex X0 being non empty SubSpace
of X st X0 is boundary closed) implies X is non almost_discrete;
theorem
for X being non empty TopSpace holds (ex X0 being non empty SubSpace
of X st X0 is everywhere_dense proper) implies X is non almost_discrete;
theorem
for X being non empty TopSpace holds (ex X0 being non empty SubSpace
of X st X0 is dense open proper) implies X is non almost_discrete;
registration
let X be non almost_discrete non empty TopSpace;
cluster nowhere_dense strict non empty for SubSpace of X;
existence
proof
consider A0 being non empty Subset of X such that
A1: A0 is nowhere_dense by TEX_1:def 6;
consider X0 being strict non empty SubSpace of X such that
A2: A0 = the carrier of X0 by TSEP_1:10;
take X0;
for A be Subset of X st A = the carrier of X0 holds A is nowhere_dense
by A1,A2;
hence thesis;
end;
cluster everywhere_dense proper strict non empty for SubSpace of X;
existence
proof
consider A0 being Subset of X such that
A3: A0 <> the carrier of X and
A4: A0 is everywhere_dense by TEX_1:32;
A0 is non empty by A4,TOPS_3:34;
then consider
X0 being everywhere_dense strict non empty SubSpace of X such
that
A5: A0 = the carrier of X0 by A4,Th17;
take X0;
A0 is proper by A3,SUBSET_1:def 6;
hence thesis by A5,TEX_2:8;
end;
end;
reserve X for non almost_discrete non empty TopSpace;
theorem Th62:
for A0 being non empty Subset of X st A0 is nowhere_dense ex X0
being nowhere_dense strict non empty SubSpace of X st A0 = the carrier of X0
proof
let A0 be non empty Subset of X;
consider X0 being strict non empty SubSpace of X such that
A1: A0 = the carrier of X0 by TSEP_1:10;
assume A0 is nowhere_dense;
then reconsider Y0 = X0 as nowhere_dense strict non empty SubSpace of X by A1
,Th35;
take Y0;
thus thesis by A1;
end;
theorem
for A0 being non empty proper Subset of X st A0 is everywhere_dense ex
X0 being everywhere_dense proper strict SubSpace of X st A0 = the carrier of X0
proof
let A0 be non empty proper Subset of X;
assume A0 is everywhere_dense;
then consider
X0 being everywhere_dense strict non empty SubSpace of X such that
A1: A0 = the carrier of X0 by Th17;
reconsider X0 as everywhere_dense proper strict SubSpace of X by A1,TEX_2:8;
take X0;
thus thesis by A1;
end;
theorem
for X1 being nowhere_dense non empty SubSpace of X ex X2 being
everywhere_dense proper strict non empty SubSpace of X st X1,X2
constitute_a_decomposition
proof
let X1 be nowhere_dense non empty SubSpace of X;
consider X2 being proper strict non empty SubSpace of X such that
A1: X1,X2 constitute_a_decomposition by Th8;
reconsider X2 as everywhere_dense proper strict non empty SubSpace of X by A1
,Th37;
take X2;
thus thesis by A1;
end;
theorem
for X1 being everywhere_dense proper non empty SubSpace of X ex X2
being nowhere_dense strict non empty SubSpace of X st X1,X2
constitute_a_decomposition
proof
let X1 be everywhere_dense proper non empty SubSpace of X;
consider X2 being proper strict non empty SubSpace of X such that
A1: X1,X2 constitute_a_decomposition by Th8;
reconsider X2 as nowhere_dense strict non empty SubSpace of X by A1,Th37;
take X2;
thus thesis by A1;
end;
theorem
for Y1, Y2 being non empty TopSpace st Y2 = the TopStruct of Y1 holds
Y1 is nowhere_dense SubSpace of X iff Y2 is nowhere_dense SubSpace of X
proof
let X1,X2 be non empty TopSpace;
assume
A1: X2 = the TopStruct of X1;
thus X1 is nowhere_dense SubSpace of X implies X2 is nowhere_dense SubSpace
of X
proof
assume
A2: X1 is nowhere_dense SubSpace of X;
then reconsider Y2 = X2 as SubSpace of X by A1,TMAP_1:7;
for A2 be Subset of X st A2 = the carrier of Y2 holds A2 is
nowhere_dense by A1,A2,Def4;
hence thesis by Def4;
end;
assume
A3: X2 is nowhere_dense SubSpace of X;
then reconsider Y1 = X1 as SubSpace of X by A1,TMAP_1:7;
for A1 be Subset of X st A1 = the carrier of Y1 holds A1 is
nowhere_dense by A1,A3,Def4;
hence thesis by Def4;
end;
registration
let X be non almost_discrete non empty TopSpace;
cluster boundary closed strict non empty for SubSpace of X;
existence
proof
consider A being non empty Subset of X such that
A1: A is nowhere_dense by TEX_1:def 6;
consider C being Subset of X such that
A2: A c= C and
A3: C is closed & C is boundary by A1,TOPS_3:27;
C is non empty by A2,XBOOLE_1:3;
then consider X0 being strict non empty SubSpace of X such that
A4: C = the carrier of X0 by TSEP_1:10;
take X0;
( for C be Subset of X st C = the carrier of X0 holds C is boundary)&
for C be Subset of X st C = the carrier of X0 holds C is closed by A3,A4;
hence thesis by BORSUK_1:def 11;
end;
cluster dense open proper strict non empty for SubSpace of X;
existence
proof
consider A0 being Subset of X such that
A5: A0 <> the carrier of X and
A6: A0 is dense open by TEX_1:34;
A0 is non empty by A6,TOPS_3:17;
then consider X0 being dense open strict non empty SubSpace of X such that
A7: A0 = the carrier of X0 by A6,Th23;
take X0;
A0 is proper by A5,SUBSET_1:def 6;
hence thesis by A7,TEX_2:8;
end;
end;
theorem Th67:
for A0 being non empty Subset of X st A0 is boundary closed ex
X0 being boundary closed strict non empty SubSpace of X st A0 = the carrier of
X0
proof
let A0 be non empty Subset of X;
consider X0 being strict non empty SubSpace of X such that
A1: A0 = the carrier of X0 by TSEP_1:10;
assume A0 is boundary closed;
then reconsider
Y0 = X0 as boundary closed strict non empty SubSpace of X by A1,Th29,
TSEP_1:11;
take Y0;
thus thesis by A1;
end;
theorem
for A0 being non empty proper Subset of X st A0 is dense open ex X0
being dense open proper strict SubSpace of X st A0 = the carrier of X0
proof
let A0 be non empty proper Subset of X;
assume A0 is dense open;
then consider X0 being dense open strict non empty SubSpace of X such that
A1: A0 = the carrier of X0 by Th23;
reconsider X0 as dense open proper strict SubSpace of X by A1,TEX_2:8;
take X0;
thus thesis by A1;
end;
theorem
for X1 being boundary closed non empty SubSpace of X ex X2 being dense
open proper strict non empty SubSpace of X st X1,X2 constitute_a_decomposition
proof
let X1 be boundary closed non empty SubSpace of X;
consider X2 being proper strict non empty SubSpace of X such that
A1: X1,X2 constitute_a_decomposition by Th8;
reconsider X2 as dense open proper strict non empty SubSpace of X by A1,Th31,
TSEP_2:34;
take X2;
thus thesis by A1;
end;
theorem
for X1 being dense open proper non empty SubSpace of X ex X2 being
boundary closed strict non empty SubSpace of X st X1,X2
constitute_a_decomposition
proof
let X1 be dense open proper non empty SubSpace of X;
consider X2 being proper strict non empty SubSpace of X such that
A1: X1,X2 constitute_a_decomposition by Th8;
reconsider X2 as boundary closed strict non empty SubSpace of X by A1,Th31,
TSEP_2:33;
take X2;
thus thesis by A1;
end;
theorem
for X0 being non empty SubSpace of X holds X0 is nowhere_dense iff ex
X1 being boundary closed strict non empty SubSpace of X st X0 is SubSpace of X1
proof
let X0 be non empty SubSpace of X;
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
thus X0 is nowhere_dense implies ex X1 being boundary closed strict non
empty SubSpace of X st X0 is SubSpace of X1
proof
assume X0 is nowhere_dense;
then A is nowhere_dense;
then consider C being Subset of X such that
A1: A c= C and
A2: C is closed & C is boundary by TOPS_3:27;
C is non empty by A1,XBOOLE_1:3;
then consider
X1 being boundary closed strict non empty SubSpace of X such that
A3: C = the carrier of X1 by A2,Th67;
take X1;
thus thesis by A1,A3,TSEP_1:4;
end;
given X1 being boundary closed strict non empty SubSpace of X such that
A4: X0 is SubSpace of X1;
reconsider C = the carrier of X1 as Subset of X by TSEP_1:1;
now
take C;
thus A c= C & C is boundary & C is closed by A4,Def3,TSEP_1:4,11;
end;
then for A be Subset of X st A = the carrier of X0 holds A is nowhere_dense
by TOPS_3:27;
hence thesis;
end;
theorem
for X0 being nowhere_dense non empty SubSpace of X holds X0 is
boundary closed or ex X1 being everywhere_dense proper strict non empty
SubSpace of X, X2 being boundary closed strict non empty SubSpace of X st X1
meet X2 = the TopStruct of X0 & X1 union X2 = the TopStruct of X
proof
let X0 be nowhere_dense non empty SubSpace of X;
reconsider D = the carrier of X0 as non empty Subset of X by TSEP_1:1;
A1: X is SubSpace of X by TSEP_1:2;
D is nowhere_dense by Th35;
then consider C, B being Subset of X such that
A2: C is closed boundary and
A3: B is everywhere_dense and
A4: C /\ B = D and
A5: C \/ B = the carrier of X by TOPS_3:51;
B <> {} by A4;
then consider
X1 being everywhere_dense strict non empty SubSpace of X such that
A6: B = the carrier of X1 by A3,Th17;
assume
A7: X0 is non boundary or X0 is non closed;
now
assume B is non proper;
then B = the carrier of X by SUBSET_1:def 6;
then D = C by A4,XBOOLE_1:28;
hence contradiction by A7,A2,TSEP_1:11;
end;
then reconsider
X1 as everywhere_dense proper strict non empty SubSpace of X by A6,TEX_2:8;
C <> {} by A4;
then consider
X2 being boundary closed strict non empty SubSpace of X such that
A8: C = the carrier of X2 by A2,Th67;
take X1, X2;
C meets B by A4,XBOOLE_0:def 7;
then X1 meets X2 by A8,A6,TSEP_1:def 3;
then the carrier of X1 meet X2 = D by A4,A8,A6,TSEP_1:def 4;
hence X1 meet X2 = the TopStruct of X0 by TSEP_1:5;
the carrier of X1 union X2 = the carrier of X by A5,A8,A6,TSEP_1:def 2;
hence thesis by A1,TSEP_1:5;
end;
theorem
for X0 being everywhere_dense non empty SubSpace of X holds X0 is
dense open or ex X1 being dense open proper strict non empty SubSpace of X, X2
being nowhere_dense strict non empty SubSpace of X st X1 misses X2 & X1 union
X2 = the TopStruct of X0
proof
let X0 be everywhere_dense non empty SubSpace of X;
reconsider D = the carrier of X0 as non empty Subset of X by TSEP_1:1;
D is everywhere_dense by Th16;
then consider C, B being Subset of X such that
A1: C is open dense and
A2: B is nowhere_dense and
A3: C \/ B = D and
A4: C misses B by TOPS_3:49;
C <> {} by A1,TOPS_3:17;
then consider X1 being dense open strict non empty SubSpace of X such that
A5: C = the carrier of X1 by A1,Th23;
assume
A6: X0 is non dense or X0 is non open;
now
assume C is non proper;
then
A7: C = the carrier of X by SUBSET_1:def 6;
C c= D by A3,XBOOLE_1:7;
then D = [#]X by A7,XBOOLE_0:def 10;
then D is dense open;
hence contradiction by A6,TSEP_1:16;
end;
then reconsider
X1 as dense open proper strict non empty SubSpace of X by A5,TEX_2:8;
now
per cases by A6;
suppose
A8: X0 is non dense;
assume B = {};
thus contradiction by A8;
end;
suppose
A9: X0 is non open;
assume B = {};
hence contradiction by A1,A3,A9,TSEP_1:16;
end;
end;
then consider
X2 being nowhere_dense strict non empty SubSpace of X such that
A10: B = the carrier of X2 by A2,Th62;
take X1, X2;
thus X1 misses X2 by A4,A5,A10,TSEP_1:def 3;
the carrier of X1 union X2 = the carrier of X0 by A3,A5,A10,TSEP_1:def 2;
hence thesis by TSEP_1:5;
end;
theorem
for X0 being nowhere_dense non empty SubSpace of X ex X1 being dense
open proper strict non empty SubSpace of X, X2 being boundary closed strict non
empty SubSpace of X st X1,X2 constitute_a_decomposition & X0 is SubSpace of X2
proof
let X0 be nowhere_dense non empty SubSpace of X;
reconsider D = the carrier of X0 as non empty Subset of X by TSEP_1:1;
D is nowhere_dense by Th35;
then consider C, B being Subset of X such that
A1: C is closed boundary and
A2: B is open dense and
A3: C /\ (D \/ B) = D and
A4: C misses B and
A5: C \/ B = the carrier of X by TOPS_3:52;
B <> {} by A2,TOPS_3:17;
then consider X1 being dense open strict non empty SubSpace of X such that
A6: B = the carrier of X1 by A2,Th23;
A7: C <> {} by A3;
then consider
X2 being boundary closed strict non empty SubSpace of X such that
A8: C = the carrier of X2 by A1,Th67;
A9: C /\ B = {} by A4,XBOOLE_0:def 7;
now
assume B is non proper;
then B = the carrier of X by SUBSET_1:def 6;
hence contradiction by A7,A9,XBOOLE_1:28;
end;
then reconsider
X1 as dense open proper strict non empty SubSpace of X by A6,TEX_2:8;
take X1, X2;
for P,Q be Subset of X st P = the carrier of X1 & Q = the carrier of X2
holds P,Q constitute_a_decomposition by A4,A5,A6,A8;
hence X1,X2 constitute_a_decomposition;
D c= C by A3,XBOOLE_1:17;
hence thesis by A8,TSEP_1:4;
end;
theorem
for X0 being everywhere_dense proper SubSpace of X ex X1 being dense
open proper strict SubSpace of X, X2 being boundary closed strict SubSpace of X
st X1,X2 constitute_a_decomposition & X1 is SubSpace of X0
proof
let X0 be everywhere_dense proper SubSpace of X;
reconsider D = the carrier of X0 as Subset of X by TSEP_1:1;
D is everywhere_dense by Th16;
then consider C, B being Subset of X such that
A1: C is open dense and
A2: B is closed boundary and
A3: C \/ (D /\ B) = D and
A4: C misses B and
A5: C \/ B = the carrier of X by TOPS_3:50;
C <> {} by A1,TOPS_3:17;
then consider X1 being dense open strict non empty SubSpace of X such that
A6: C = the carrier of X1 by A1,Th23;
A7: now
assume C is non proper;
then C = the carrier of X by SUBSET_1:def 6;
then the carrier of X c= D by A3,XBOOLE_1:7;
then D = the carrier of X by XBOOLE_0:def 10;
then D is non proper by SUBSET_1:def 6;
hence contradiction by TEX_2:8;
end;
then B is non empty by A5,SUBSET_1:def 6;
then consider
X2 being boundary closed strict non empty SubSpace of X such that
A8: B = the carrier of X2 by A2,Th67;
reconsider X1 as dense open proper strict SubSpace of X by A6,A7,TEX_2:8;
take X1, X2;
for P,Q be Subset of X st P = the carrier of X1 & Q = the carrier of X2
holds P,Q constitute_a_decomposition by A4,A5,A6,A8;
hence X1,X2 constitute_a_decomposition;
C c= D by A3,XBOOLE_1:7;
hence thesis by A6,TSEP_1:4;
end;